parfdocker/parf repository overview

⁠Description of the Parf docker image for experiments reproduction

Parf is a lightweight and fully automated parameter tuning tool for the abstract interpretation-based static analyzer Frama-C/Eva. 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: Adaptive Parameter Tuning for Abstract Interpretation" submitted to ASE 2024.

Here is a demo for an overview:

⁠Set up

1. Install Docker as per https://docs.docker.com/engine/install/⁠.

2. Pull Parf from dockerhub:

   docker pull parfdocker/parf:v2.0
   

   Copy

   To check whether you have successfully pulled the correct docker image: run docker images and see if parfdocker/parf exists.

3. Run the Docker container:

   docker run -it --platform linux/amd64 --entrypoint /bin/bash -u vscode parfdocker/parf:v2.0
   cd /home/vscode
   

   Copy

   You should be in a terminal environment as a user.

4. Synchronize the environment with the current opam switch in the container:

   eval $(opam env)
   

   Copy

5. Check whether Frama-C and Mopsa are available in the container:

   frama-c --version
   

   Copy

   and

   mopsa-c -v
   

   Copy

⁠Usage

frama-c <sourcefiles> -parf [OPTION]

The external options of Parf are:

• -parf-budget: time budget (seconds) of whole parf analysis; default value is 300.
• -parf-process: number of processes in parallel computing; set 0 (default value) for sequential computing.
• -parf-sample-num: samples of each refinement iteration; default value is 4.
• -parf-refine-num: number of refinement iterations; default value is 7.
• -parf-alpha: value of hyper-parameter $\alpha$; default is 0.1.
• -parf-beta: value of hyper-parameter $\beta$; default is 2.0.

As discussed in the rebuttal response, no significant sensitivity of Parf to the hyper-parameters ($num_{\text{sample}}, num_{\text{refine}}, \alpha,\beta$) is observed, and setting -parf-sample-num 6 and -parf-refine-num 5 may obtain a slight performance improvement compared to experimental settings in the paper. Moreover, the most important options are -parf-budget and -parf-process. Here are some examples of using Parf:

• Use the sequential version of Parf to analyze oscs-benchmarks/2048/2048.c within 300 seconds:

  frama-c oscs-benchmarks/2048/2048.c -parf -parf-budget 300
  

  Copy
• Use the 4-process parallel version of Parf to analyze oscs-benchmarks/2048/2048.c within 300 seconds:

  frama-c oscs-benchmarks/2048/2048.c -parf -parf-budget 300 -parf-process 4
  

  Copy

⁠Reproduction of Experiments in the Paper

⁠RQ1: Parf vs. Other Strategies

To check the experimental results:

1. Run cd ~/reproduction-and-summaries/.

2. Check the summaries of experimental results of the Parf tool and the other three baselines:

   • Parf: cat final-summary-of-parf-parallel.txt. (Or check the results of experiments repeatedly conducted with Parf via cat log_parf_parallel_expr1-summary.txt and cat log_parf_parallel_expr2-summary.txt)
   • Default: 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>, Parameters: <final_parameters>
   

   Copy

   where <program>, num_of_alarms, and final_parameters are respectively the name of the benchmark program, the number of alarms of the most accurate analysis, and the parameter setting of the most accurate analysis.

3. Check the analysis log, say benchmark with the name <program>, of Parf tool and other three baselines:

   • Parf: cat ../oscs-benchmarks/<program>/.frama-c/log_parf_parallel_expr1 and cat ../oscs-benchmarks/<program>/.frama-c/log_parf_parallel_expr2. For example, cat ../oscs-benchmarks/2048/.frama-c/log_parf_parallel_expr1 for benchmark 2048.
   • Default: cat ../oscs-benchmarks/<program>/.frama-c/log_eva_default
   • Official: cat ../oscs-benchmarks/<program>/.frama-c/log_eva_official
   • Expert: cat ../oscs-benchmarks/<program>/.frama-c/log_eva_expert Note that many analysis logs of expert 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.

   Note that some benchmarks, e.g. jsmn, kgflags, miniz, and qlz, contain all analysis targets and programs in one project, and their logs files are included in one file and

   real	xxmxx.xxxs
   user	xxmxx.xxxs
   sys     xxmxx.xxxs
   

   Copy

To reproduce the experimental results (make sure the current directory is reproduction-and-summaries):

• Default: Execute the following commands to reproduce results under the default parameter configuration:

  ./run_oscs_eva_default.sh log_eva_default_1
  

  Copy

  The output file is log_eva_default_1-summary.txt.

• Official: Execute the following commands to reproduce results under the official parameter configuration:

  ./run_oscs_eva_official.sh log_eva_official_1
  

  Copy

  The output file is log_eva_official_1-summary.txt.

• Expert: Execute the following commands to reproduce results under the -eva-precision incremental strategy (it is expected to take more than 15 hours.):

  ./run_oscs_eva_expert.sh log_eva_expert_1
  

  Copy

  The output file is log_eva_expert_1-summary.txt.

• Parf: Execute the following commands to reproduce results under the 4-process parallel Parf strategy (it is expected to take more than 10 hours.):

  ./run_oscs_parf_parallel_core4.sh log_parf_parallel_1
  

  Copy

  The output file is log_parf_parallel_1-summary.txt.

  Remark: Given the stochastic nature of Parf, we conducted two experiments using the Parf strategy during our tests, each using half of the allocated time budget (30 minutes for each project). The results of these experiments are recorded in log_parf_parallel_expr1-summary.txt and log_parf_parallel_expr2-summary.txt respectively. You can utilize compare_summaries.py to compare the results of these experiments and identify the optimal outcome:

  python3 compare_summaries.py <summary_name_1> <summary_name_2> <final_summary>
  

  Copy

  For instance,

  python3 compare_summaries.py log_parf_parallel_expr1-summary.txt log_parf_parallel_expr2-summary.txt final-summary-of-parf-parallel.txt
  

  Copy

⁠RQ2: Effect of Hyper-Parameters

To check the experimental results: (make sure the current directory is reproduction-and-summaries):

1. Check the summaries of experimenal results with different hyper-parameters:

   Hyper-Parameter	Command
   $(\alpha,\beta)=(0.067,1.33)$	cat log_a_067_b_133-summary.txt
   $(\alpha,\beta)=(0.067,2)$	cat log_a_067_b_200-summary.txt
   $(\alpha,\beta)=(0.067,3)$	cat log_a_067_b_300-summary.txt
   $(\alpha,\beta)=(0.1,1.33)$	cat log_a_010_b_133-summary.txt
   $(\alpha,\beta)=(0.1,2)$	cat log_a_010_b_200-summary.txt
   $(\alpha,\beta)=(0.1,3)$	cat log_a_010_b_300-summary.txt
   $(\alpha,\beta)=(0.15,1.33)$	cat log_a_015_b_133-summary.txt
   $(\alpha,\beta)=(0.15,2)$	cat log_a_015_b_200-summary.txt
   $(\alpha,\beta)=(0.15,3)$	cat log_a_015_b_300-summary.txt
   $num_{\text{sample}=2}$	cat log_sample_num_2-summary.txt
   $num_{\text{sample}=4}$	cat log_sample_num_4-summary.txt
   $num_{\text{sample}=6}$	cat log_sample_num_6-summary.txt
   $num_{\text{sample}=8}$	cat log_sample_num_8-summary.txt
   $num_{\text{sample}=10}$	cat log_sample_num_10-summary.txt
   $num_{\text{refine}=3}$	cat log_refine_num_3-summary.txt
   $num_{\text{refine}=4}$	cat log_refine_num_4-summary.txt
   $num_{\text{refine}=5}$	cat log_refine_num_5-summary.txt
   $num_{\text{refine}=6}$	cat log_refine_num_6-summary.txt
   $num_{\text{refine}=7}$	cat log_refine_num_7-summary.txt
   $num_{\text{refine}=8}$	cat log_refine_num_8-summary.txt

   Remark:

   • The experiments of RQ2 are conducted over 18/37 OSCS benchmarks which has -eva-precision >= 9. Note that benchmarks qlz-ex1, qlz-ex2, and qlz-ex4 are included but qlz-ex3 is excluded under this criteria.
   • log_refine_num_4-summary.txt and log_a_010_b_200-summary.txt is same as log_refine_num_3-summary.txt because these three experiments share identical hyper-parameters setting. We do not repeatedly conduct the experiments but just reuse the results.
   • The content of log_refine_num_7-summary.txt is a subset of final-summary-of-parf-parallel.txt since these two experiments share identical hyper-parameters setting. We do not repeatedly conduct the experiment but just reuse the results.

2. Check the analysis log, say benchmark with the name <program>, with hyper-parameter $num_{\text{sample}=6}$:

   cat ../partial-oscs-benchmarks/<program>/.frama-c/log_refine_num_6_1.

To reproduce the experimental results (make sure the current directory is reproduction-and-summaries):

1. Execute ./analysis_hyper_parameters_alpha_beta.sh to reproduce experimental results of different hyper-parameters $\alpha$ and $\beta$.
2. Execute ./analysis_hyper_parameters_num_sample.sh to reproduce experimental results of different hyper-parameters $num_{\text{sample}}$.
3. Execute ./analysis_hyper_parameters_num_refine.sh to reproduce experimental results of different hyper-parameters $num_{\text{refine}}$.

⁠RQ3: Generality of Parf

Check Experiment Results

We provide experiment results of Mopsa in the form of analysis logs and a summary table. We store different experiment results in different git tags. first, cd mopsa-oscs-benchmarks and then:

git tag -l

This will produce

result-8.17
result-8.19-10min
result-8.20-30min
result-8.21-30min-2
results-8.18-17-44

which are different experiment results of our Parf on Mopsa.

Note that we include only result-*-30min(-2) in our ASE'24 paper. If you want to check these experiment results manually, run

git checkout <experiment-tag>

and then the experiment logs of benchmark <benchmark-name> are in the mopsa-oscs-benchmarks/oscs-benchmarks/<benchmark-name>/.frama-c/ directory.

To check the summary table of the experiment results, see the mopsa-oscs-benchmarks/mopsa-results.csv file. Note that although Mopsa with Parf gives an analysis result of monocypher in the log/table, its consumed time exceeds 30 min and is marked "TO" in our paper.

Reproduction of Experiment Results

To reproduce our experiments, run

cd mopsa-oscs-benchmarks/scripts
./run_oscs-mopsa_parf.sh

then new experiment logs will be produced in the .frama-c directories of different benchmarks. Note that new logs will overwrite old ones; this means if you need the old logs, remember to git commmit and use git tag -a to store them in the repository.

⁠RQ4: Improving Frama-C in SV-COMP

To check the experimental results:

1. Run cd ~/frama-c-sv/.

2. Summarize the results:

   python3 evaluate_results.py <inputdir>
   

   Copy

   where <inputdir> can be all subcategories of sv-benchmarks/NoOverflows-BitVectors and sv-benchmarks/NoOverflows-Other, which contains verification tasks of NoOverflows category where Frama-C participated in the SV-COMP 2022 [3,4]. Here is a complete list of inputdir:

   • sv-benchmarks/NoOverflows-BitVectors/signedintegeroverflow-regression
   • sv-benchmarks/NoOverflows-BitVectors/termination-crafted
   • sv-benchmarks/NoOverflows-BitVectors/termination-crafted-lit
   • sv-benchmarks/NoOverflows-BitVectors/termination-numeric
   • sv-benchmarks/NoOverflows-Other/bitvector
   • sv-benchmarks/NoOverflows-Other/goblint-regression
   • sv-benchmarks/NoOverflows-Other/loop-zilu
   • sv-benchmarks/NoOverflows-Other/psyco
   • sv-benchmarks/NoOverflows-Other/recursive
   • sv-benchmarks/NoOverflows-Other/recursive-simple

   Remark: The datasets and experimental results are stored in the frama-c-sv/sv-benchmarks directory. This directory contains two categories of verification tasks: NoOverflows-BitVectors and NoOverflows-Other, each containing several subclasses of verification tasks. For a specific subclass of verification tasks, such as NoOverflows-BitVectors/signedintegeroverflow-regression, the relevant data is as follows:

   • NoOverflows-BitVectors/signedintegeroverflow-regression: This directory contains all the source files (.i or .c) and property files (.yml) for the verification programs.
   • NoOverflows-BitVectors/signedintegeroverflow-regression-output: This directory stores the verification results for all programs under the -eva-precision 11 parameter setting, consistent with the competition strategy.
   • NoOverflows-BitVectors/signedintegeroverflow-regression-config: This directory contains the parameter settings generated by Parf for all programs.
   • NoOverflows-BitVectors/signedintegeroverflow-regression-parf: This directory stores the verification results under the parameter settings generated by Parf.

To reproduce the experimental data (make sure the current directory is ~/frama-c-sv/):

./run_frama-c-sv.sh
./get-sv-benchmarks-parf-parameters.sh
./run_parf.sh

It is expected to take more than 10 hours. Please refer to the last part about how to check the results.