Optimise the output to reduce token consumption

[mihaistate]

Created two functions in the esbmc_util file that use regex patterns to reduce the generated output of ESBMC-AI and another one that removes patterns by using the nltk library.
Added tests for the patterns that use specific ESBMC-AI phrases as input strings.
Changed the content of a system instruction in the config.json file to tell the LLM to avoid providing some informations that are not useful for debbuging and development puroposes, such as time measurements, assertions, assumptions or warnings. This approach leads to a more consistent and efficient output reduction alongside the three functions that use specific patterns.
Added new scenarious in the config.json file for some bugs.
The implementation has been tested on various SV-Benchmarks multiple times and they lead to consistent token consumption reductions.

[Yiannis128]

Why did you comment this out? It says clearly, "Do not remove import."

[Yiannis128]

This downloads a library to your system without explicit user approval. This is bad design, there should be an option in the config to configure where it downloads this. We don't want to be downloading files to the user's systems without them knowing ;)

[Yiannis128]

Consider the following sample:

#include <string.h>
#include <assert.h>

int main() {
	char* value = "branches";
	assert(strcmp("branches", value) == 0);
	return 0;
}

Would produce the following ESBMC output:

ESBMC version 7.5.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing sample.c
Converting
Generating GOTO Program
GOTO program creation time: 0.097s
GOTO program processing time: 0.002s
Starting Bounded Model Checking
Unwinding loop 8 iteration 1   file string.c line 96 column 12 function strcmp
Unwinding loop 8 iteration 2   file string.c line 96 column 12 function strcmp
Unwinding loop 8 iteration 3   file string.c line 96 column 12 function strcmp
Unwinding loop 8 iteration 4   file string.c line 96 column 12 function strcmp
Unwinding loop 8 iteration 5   file string.c line 96 column 12 function strcmp
Unwinding loop 8 iteration 6   file string.c line 96 column 12 function strcmp
Unwinding loop 8 iteration 7   file string.c line 96 column 12 function strcmp
Unwinding loop 8 iteration 8   file string.c line 96 column 12 function strcmp
Symex completed in: 0.002s (92 assignments)
Slicing time: 0.000s (removed 90 assignments)
Generated 19 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
Solving with solver Boolector 3.2.3
Runtime decision procedure: 0.000s
Building error trace

[Counterexample]


State 1 file sample.c line 6 column 2 function main thread 0
----------------------------------------------------
Violated property:
  file sample.c line 6 column 2 function main
  assertion strcmp("branches", value) == 0
  return_value$_strcmp$1 == 0


VERIFICATION FAILED

Putting that through a regex viewer removes from the Violated property: section the line assertion strcmp("branches", value) == 0.

There are many more regex that are too generic to be included. You filter out ESBMC output that is useful.

[Yiannis128]

What does this even do? Why was it included? You included it without a commit message explaining why it should be included in the project. Arguably, this could just be included as a generic script on the system.

[Yiannis128]

So this is quite a messy pull request, the pull request has some big issues both on a technical level and an experimental level.

Technical Issues

1. You have deleted .env.example which is used as a template for people setting up ESBMC-AI before we make a better config solution.
2. Why is there a myenv folder with random and unexplained scripts inside? Also why is there a folder path/to/your/virtualenv also committed? The message committing them does not even explain what they're for.
3. The commit has a lot of empty tab spaces. Please make sure to format the code before committing it as it appears in the diff and makes it harder to read.
4. The source code files are not formatted.
5. In your regex, you have used flags=re.MULTILINE for operations that occur only on one line. There is no need for this and it would slow down the operations... You use flags=re.MULTILINE only when you want to apply the regex to each line.
6. Some regex operations could be done without regex. For example, filtering strings out would be faster without regex.
7. With this amount of regex, how can you guarantee it won't remove anything unintentionally? You said that you wrote tests, but please see this comment I've left. There are many more like this. If the current PR is merged, we will have random parts of the ESBMC output removed.
8. The tests you included have the data inside. Would be better to have the data outside the test code and load it in using fixtures.
9. You should add an option in the config to enable/disable this feature.

You shouldn't include everything in a commit that you work on. Only things that you would like included in the project.

Practical Issue

Do you have any figures that show any improvement in speed/accuracy of successful repairs? If the accuracy of repairs improves, we should know by how much. If it becomes worse, we need to know why, also it cannot be accepted. Also, how slow does this become due to all the regex?

Also, there's already a merge that happened that can reduce the ESBMC output to a few tokens as it uses only the violated property section only, please look at: #117 Maybe this PR can be added as another mode of that?

[mihaistate]

"1.Some regex operations could be done without regex. For example, filtering strings out would be faster without regex.
"
The regex pattern may prove to be more efficient than any other string method, we need abstract patterns that are able to remove sentences that will be phrased differentlty, but refer to the same idea, that is why I would suggest to stick to regex patterns. I agree that the string methods are faster, but they can't match all the phrases that point to the same idea

[Yiannis128]

"1.Some regex operations could be done without regex. For example, filtering strings out would be faster without regex. " The regex pattern may prove to be more efficient than any other string method, we need abstract patterns that are able to remove sentences that will be phrased differentlty, but refer to the same idea, that is why I would suggest to stick to regex patterns. I agree that the string methods are faster, but they can't match all the phrases that point to the same idea

The problem I have been trying to explain is that REGEX patterns used carelessly, like in this case where you are nuking lines with the word “branches” is not good design. I showed you an example where the useful output was altered.

Also, REGEX is extremely slow. Direct string manipulation is more rigid but also miles faster. So I don't know what you mean by: "The regex pattern may prove to be more efficient", efficient in terms of what?