Parf is a toolkit for adaptively tuning abstraction strategies of static program analyzers in a fully automated manner. This repository contains a Docker image of Parf (as a plugin to Frama-C) used to replicate the experimental results reported in the paper titled "Parf: An Adaptive Abstraction-Strategy Tuner for Static Analysis" submitted to JCST.
Install Docker as per https://docs.docker.com/engine/install/.
Pull Parf from dockerhub:
docker pull parfdocker/parf-jcst:v2.0
To check whether you have successfully pulled the correct docker image: run docker images and see if parfdocker/parf-jcst exists.
Run the Docker container:
docker run -it parfdocker/parf-jcst:v2.0
You should be in a terminal environment as the root. Then
root@300735229ca6:~# ls
Parf-Benchmark
Synchronize the environment with the current opam switch in the container:
eval $(opam env)
Check whether Frama-C and Parf is available in the container:
frama-c --version
and
frama-c -parf-h
frama-c <sourcefiles> -parf [OPTION]
Below are the most commonly used external options for Parf, along with their default values:
-parf-budget: Specifies the total time budget (in seconds) for the entire Parf analysis. Default value: 300.-parf-process: Determines the number of processes used for parallel computation. Set to 0 for sequential computation (default value).-parf-sample-num: Defines the number of samples per refinement iteration. Default value: 4.We recommend setting the value of -parf-sample-num to be 1–2 times the value of -parf-process for optimal performance. Here are some examples of using Parf:
Analyze oscs-benchmarks/2048/2048.c using the sequential version of Parf with a 300-second time budget:
frama-c oscs-benchmarks/2048/2048.c -parf -parf-budget 300
Analyze oscs-benchmarks/2048/2048.c using the parallel version of Parf with 4 processes and a 300-second time budget, generating 8 samples in each iteration:
frama-c oscs-benchmarks/2048/2048.c -parf -parf-budget 300 -parf-process 4 -parf-sample-num 8
Run cd ~/Parf-Benchmark/scripts
Check the summaries of experimental results of the Parf tool and the other four baselines:
Parf_Opt: cat log_parf-optimum.txtParf_Avg: cat log_parf-server1-summary.txt log_parf-server2-summary.txt log_parf-server3-summary.txt (The Parf_Avg in RQ1 lists the average #alarms of three independent experiments' results)-eva-precision 0: cat log_eva_precision0-summary.txtDefault: cat log_eva_default-summary.txt.Official: cat log_eva_official-summary.txt.Expert: cat log_eva_expert-summary.txt.The results of each benchmark are in the form of:
<program>, Alarms: <num_of_alarms>, Time: <time>, Parameters: <final_parameters>
where <program>, num_of_alarms, time, and final_parameters are respectively the name of the benchmark, the number of alarms reported by the final analysis, the analysis time, and the parameter setting of the final analysis (for log_parf-server1-summary.txt, log_parf-server2-summary.txt, log_parf-server3-summary.txt, and log_eva_precision0-summary.txt).
Check the detailed log of each analysis for a certain benchmark (e.g., <program>), of Parf and other four baselines:
Parf: cat ../oscs-benchmarks/<program>/.frama-c/log_parf-server1, cat ../oscs-benchmarks/<program>/.frama-c/log_parf-server2, and cat ../oscs-benchmarks/<program>/.frama-c/log_parf-server3. For example, cat ../oscs-benchmarks/2048/.frama-c/log_parf-server1 for benchmark 2048.-eva-precision 0: cat ../oscs-benchmarks/<program>/.frama-c/log_eva_precision0Default: cat ../oscs-benchmarks/<program>/.frama-c/log_eva_default-serverOfficial: cat ../oscs-benchmarks/<program>/.frama-c/log_eva_official-serverExpert: cat ../oscs-benchmarks/<program>/.frama-c/log_eva_expert-server
Note that many analysis logs ofExpert baseline do not end with a Frama-C/Eva summary, i.e. the final analysis interrupts due to the time limit, so you may have to manually search the last completed analysis.Run cd ~/Parf-Benchmark/scripts.
Reproduce the results.
-eva-precision 0:
./run_oscs_eva_precision0.sh --logfile=log_eva_precision0-reproduce
python3 summarize.py log_eva_precision0-reproduce ../oscs-benchmarks
The generated summary file is log_eva_precision0-reproduce-summary.txt.
Default:
./run_oscs_eva_default.sh --logfile=log_eva_default-reproduce
python3 summarize.py log_eva_default-reproduce ../oscs-benchmarks
The generated summary file is log_eva_default-reproduce-summary.txt.
Expert: (it is expected to take more than 20 hours)
./run_oscs_eva_expert.sh --logfile=log_eva_expert-reproduce
python3 summarize.py log_eva_expert-reproduce ../oscs-benchmarks
The generated summary file is log_eva_expert-reproduce-summary.txt.
Official:
./run_oscs_eva_official.sh log_eva_official-reproduce
python3 summarize.py log_eva_official-reproduce ../oscs-benchmarks
The generated summary file is log_eva_official-reproduce-summary.txt.
Parf:
Given the inherent randomness of Parf, we conduct 3-repeated experiments under the same hyper-parameter configurations with ASE '24 (it is expected to take more than 20 hours for each experiment):
./run_oscs_parf.sh --timeBudget=3600 --processCore=4 --sampleNum=4 --refineNum=7 --logFile=log_parf-reproduce1 --output=.parf_log-reproduce1
python3 summarize.py log_parf-reproduce1 ../oscs-benchmarks
./run_oscs_parf.sh --timeBudget=3600 --processCore=4 --sampleNum=4 --refineNum=7 --logFile=log_parf-reproduce2 --output=.parf_log-reproduce2
python3 summarize.py log_parf-reproduce2 ../oscs-benchmarks
./run_oscs_parf.sh --timeBudget=3600 --processCore=4 --sampleNum=4 --refineNum=7 --logFile=log_parf-reproduce3 --output=.parf_log-reproduce3
python3 summarize.py log_parf-reproduce3 ../oscs-benchmarks
The generated summary files for each experiments are log_parf-reproduce1-summary.txt, log_parf-reproduce2-summary.txt, and log_parf-reproduce3-summary.txt.
Then identify the optimal outcome (output as log_parf-optimum-reproduce.txt) by:
python3 collect_best_analysis.py log_parf-reproduce1-summary.txt log_parf-reproduce2-summary.txt log_parf-reproduce3-summary.txt --output_file=log_parf-optimum-reproduce.txt
Run cd ~/Parf-Benchmark/scripts.
Run cat dominant_params/summary_table_precision0.csv
The format is as follows:
Project,Analysis,Alarms,Time
monocypher,selected-10.log,606,3:03.01
monocypher,remaining-8.log,574,16:16.82
monocypher,selected-12.log,606,3:02.45
monocypher,selected-1.log,601,4:08.90
...
Each row represents the result of a controlled experiment.
Notably, a controlled experiment somehow does not terminate in the 30-minute time budget, for example:
kilo,selected-5.log,N/A,30:00.04
Then we treat this experiment by setting its reported alarms same as the -eva-precision 0 baseline.
Partition the parameter settings for 13 pairs of controlled experiments for each benchmark:
python3 partition_parameters.py log_parf-optimum-reproduce.txt dominant_params-reproduce
Note: if you replace the log_parf-optimum-reproduce.txt with log_parf-optimum.txt, you will reproduce the exactly same results displayed in the submitted paper.
Conduct the controlled experiments (it is expected to take more than 10 hours):
python3 conduct_dominant_experiments.py --parameters_dir dominant_params-reproduce --projects_dir ../oscs-benchmarks
Collect the results of all controlled experiments:
python3 summarize_dominant.py ../oscs-benchmarks dominant_params-reproduce
Then check the results: cat dominant_params-reproduce/summary_table_precision0.csv.
The source program of RQ3 is the 2018_06_parser/parser_full.c of the benchmark tutorials: cat ~/Parf-Benchmark/oscs-benchmarks/tutorials/2018_06_parser/parser_full.c.
Run cd ~/Parf-Benchmark/oscs-benchmarks/tutorials/2018_06_parser/.
To reproduce the analysis result of Expert:
frama-c parser_full.c -eva -eva-precision 11
, which is same as
frama-c parser_full.c -eva -eva-widening-delay 6 -eva-subdivide-non-linear 220 -eva-split-return auto -eva-slevel 5000 -eva-remove-redundant-alarms -eva-plevel 2000 -eva-partition-history 2 -eva-octagon-through-calls -eva-min-loop-unroll 4 -eva-ilevel 256 -eva-equality-through-calls formals -eva-domains cvalue,equality,gauges,octagon,symbolic-locations -eva-auto-loop-unroll 1024
The result summary is
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
5 functions analyzed (out of 7): 71% coverage.
In these functions, 89 statements reached (out of 89): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
1 alarm generated by the analysis:
1 access out of bounds index
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 3 valid 2 unknown 0 invalid 5 total
Preconditions 7 valid 1 unknown 0 invalid 8 total
76% of the logical properties reached have been proven.
----------------------------------------------------------------------------
If you replace the -eva-partition-history 2 in the above parameter setting with -eva-partition-history 0 used by Expert, the false alarm will be eliminated:
frama-c parser_full.c -eva -eva-widening-delay 6 -eva-subdivide-non-linear 220 -eva-split-return auto -eva-slevel 5000 -eva-remove-redundant-alarms -eva-plevel 2000 -eva-partition-history 0 -eva-octagon-through-calls -eva-min-loop-unroll 4 -eva-ilevel 256 -eva-equality-through-calls formals -eva-domains cvalue,equality,gauges,octagon,symbolic-locations -eva-auto-loop-unroll 1024
To reproduce the analysis result of Parf:
frama-c parser_full.c -eva -eva-widening-delay 21 -eva-subdivide-non-linear 391 -eva-split-return auto -eva-slevel 5866 -eva-remove-redundant-alarms -eva-plevel 4001 -eva-partition-history 0 -eva-octagon-through-calls -eva-min-loop-unroll 0 -eva-ilevel 513 -eva-equality-through-calls formals -eva-domains cvalue,equality,gauges,octagon,symbolic-locations -eva-auto-loop-unroll 1651
The result summary is
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
5 functions analyzed (out of 7): 71% coverage.
In these functions, 89 statements reached (out of 89): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
0 alarms generated by the analysis.
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 3 valid 2 unknown 0 invalid 5 total
Preconditions 8 valid 0 unknown 0 invalid 8 total
84% of the logical properties reached have been proven.
----------------------------------------------------------------------------
If you replace the -eva-partition-history 0 in the above parameter setting used by Parf with -eva-partition-history 2, the false alarm will be reported:
frama-c parser_full.c -eva -eva-widening-delay 21 -eva-subdivide-non-linear 391 -eva-split-return auto -eva-slevel 5866 -eva-remove-redundant-alarms -eva-plevel 4001 -eva-partition-history 2 -eva-octagon-through-calls -eva-min-loop-unroll 0 -eva-ilevel 513 -eva-equality-through-calls formals -eva-domains cvalue,equality,gauges,octagon,symbolic-locations -eva-auto-loop-unroll 1651
Content type
Image
Digest
sha256:6dcf2c325…
Size
1.6 GB
Last updated
over 1 year ago
docker pull parfdocker/parf-jcst:v2.0