Extract the zip (Evaluation/Supplementary.zip) for Supplementary material.
$ cd datagen/scripts
...
$ ./extract_run.sh
$ ./plot.sh
# Must generate the tables, plots and data summary file.
$ docker pull acharver1/achar
$ docker run --name achar --cpus=6 --memory=20g -it -v $PWD:/current acharver1/achar:latest
The -v flag is used to mount a volume into the docker container. In this case, the pwd is mounted by the name current inside the docker container.
It can be accessed by cd /current.
The following flag values can be tweaked based on the system where this docker image is to be run.
cpu (Restrict the number of CPU cores to be used)memory (Restrict the primary memory/RAM usage).v <dir1> : <dir2> Change the mount directory and the mounted (inside docker) directory by specifying correct paths. _ _
/ \ ___| |__ __ _ _ __
/ _ \ / __| '_ \ / _` | '__|
/ ___ \ (__| | | | (_| | |
/_/ \_\___|_| |_|\__,_|_|
==== Achar : Verifying REAL Loop Invariants. ====
Usage : ./runexample.sh (-h) [INDEX] [SPEC_TYPE] (Optional .. K-Induction Factor)
parameters :
INDEX Benchmark Example Number or Index to process.
SPEC_TYPE Specifiy the grammar and checker/solver pair for the run.
Check the specs folder for more information
To run a Hybrid Benchmark {1..10} Example, spec : fuzz_hybrid
To run Open-Program Benchmark {1..12, 14, 15} Examples, spec : fuzz_open
To run the NN MNIST Example, spec : fuzz_nn, INDEX : 150
To run a Fuzz Example with HonggFuzz, spec : fuzz_spec, INDEX : [1-133]
To run with Z3, spec : c_nl_all_spec, INDEX : [1-133]
To run a Colassus Example, spec : colossus_spec [need Colossus Docker Running]
Examples : Use the Example Number as INDEX.
Hybrid Example 1 : multiply()
Hybrid Example 2 : mod2check()
Open-Program Benchmark Example 2 : isprime() // Paper Example [isprime()]
Open-Program Benchmark Example 1 : sum() // Sum of squares
Open-Program Benchmark Example 8 : multiply() // Multiply Example
-h Print this Help.
Example :
$ cd current # if mounted by /current path
$ ./runbench.sh 11 fuzz_spec
Specify the index or example number followed by fuzz_open (Achar) or fuzz_hybrid (Achar Hybrid)
./runbench.sh 1 fuzz_hybrid
./runbench.sh 8 fuzz_open
The fuzz_spec option is to run Achar, c_nl_spec is to run Code2Inv.
./runbench.sh 33 fuzz_spec
./runbench.sh 33 c_nl_spec
Content type
Image
Digest
Size
2.7 GB
Last updated
over 4 years ago
docker pull acharver1/achar