ConfigTuneX: Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning

This repository contains implementation results for the ConfigTuneX as described in the following paper:

Paper: Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning

Table of Contents

• ConfigTuneX: Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning
• Table of Contents
• ConfigTuneX
• Prerequisites
• Usage
  • 1. Path Setting For Verfication Tools
    • JayHorn
    • CBMC
    • JBMC
    • Symbiotic
  • 2. FOLD-SE Rule Generation
  • 3. Run ConfigTuneX
  • 4. Results

ConfigTuneX

ConfigTuneX, a novel rule-based machine learning approach that optimizes configuration settings in static program verification tools through composite FOLD-SE rules. Artifacts for the results can be downloaded from here

Prerequisites

This application is written for Python=3.11.10. All requirements are listed in requirements.txt, and they are installed by pip with the following command.

pip install -r requirements.txt

Next, you will have to download the artifacts (configtunex_artifact.tgz) from here and decompress it with the following command.

tar -xvzf configtunex_artifact.tgz

Usage

1. Path Setting For Verfication Tools

JayHorn

1. Go to the directory {PROJ_DIR}/src/python/tools/jayhorn
2. Open jayhorn bash file
3. At line 20, replace /home/jason/projects/satune with {PROJ_DIR}/

CBMC

1. Go to the directory {PROJ_DIR}/src/python/tools/cbmc
2. Open cbmc bash file
3. At lines 3, 14, 20, replace /home/jason/projects/satune with {PROJ_DIR}/

JBMC

1. Go to the directory {PROJ_DIR}/src/python/tools/cbmc
2. Open cbmc bash file
3. At line 178, replace /home/jason/projects/satune with {PROJ_DIR}/

Symbiotic

No need to change path for executing it.

2. FOLD-SE Rule Generation

This step is to generate FOLD-SE composite rules. The rules are generated with the following command:

cd configtunex_artifact
python -m src.python.main \
       --run foldse_sota_composite \
       --asp_method foldse

Output after running the command are in the result directories of {PROJ_DIR}/_results/satune/foldse_sota_ver_composite/rf/{TOOL_NAME}.

For each verification tool and its result directory, the following files are generated:

_results/
|- satune/foldse_sota_ver_composite/rf/{TOOL_NAME}/
|  |- foldse_fp_fn_model_raw_2labels_{FOLD_NUM}.txt
|  |- foldse_fp_fn_rules_raw_2labels_{FOLD_NUM}.json
|  |- foldse_unk_model_raw_2labels_{FOLD_NUM}.txt
|  |- foldse_unk_rules_raw_2labels_{FOLD_NUM}.json

Where {TOOL_NAME} and {FOLD_NUM} represent name of verification tool and an index of fold of test data, respectively.

• The foldse_fp_fn_model_raw_2labels_{FOLD_NUM}.txt contains features of the FOLD-SE rules for incorrect-outcome result.

• The foldse_fp_fn_rules_raw_2labels_{FOLD_NUM}.json contains FOLD-SE rules for incorrect-outcome result in json format.

• The foldse_unk_model_raw_2labels_{FOLD_NUM}.txt contains features of the FOLD-SE rules for unresolved result.

• The foldse_unk_rules_raw_2labels_{FOLD_NUM}.json contains FOLD-SE rules for unresolved result in json format.

3. Run ConfigTuneX

This step is to run ConfigTuneX. Over verification tools (JayHorn, CBMC, JBMC and Symbiotic) You can run it by executing the following command:

cd configtunex_artifact
python -m src.python.main \
       --run configtunex_composite_rules_{TOOL_NAME} \
       --asp_method foldse

Output files in the result directories (the result directories of {PROJ_DIR}/_results/configtunex/rf/compositerules are the following:

_results/
|- configtunex/rf/compositerules/
|  |- foldse_{TOOL_NAME}_2labels_{FOLD_NUM}/
|  |  |- execution_log_{FOLD_NUM}.txt
|  |  |- execution_results_{FOLD_NUM}.csv
|  |  |- rf_label_encoders.pkl
|  |  |- rf_model_summray.json
|  |  |- rf_model.pkl
|  |  |- rf_test_accuracy.txt
|  |  |- scasp_output/
|  |  |  |- scasp_output_{CKSUM}.txt
|  |  |- scasp_script
|  |  |  |- scasp_{CKSUM}.pl

Where {TOOL_NAME}, {FOLD_NUM} and {CKSUM} represent name of verification tool, an index of fold of test data and the checksum value of a input program in test data, respectively.

• The execution_log_{FOLD_NUM}.txt contains log of running ConfigTuneX.
• The execution_results_{FOLD_NUM}.csv contains execution results of verification tool using ConfigTuneX.
• The rf_model.pkl is random forest model used to evaluate counterfactual configurations generated by the composite FOLD-SE rules.
• The rf_model_summray.json contains performance summary of the random forest model.
• The rf_label_encoders.pkl is encoder model for the random forest model.
• The rf_test_accuracy.txt contains test accuracy of the random forest model.
• The scasp_output/scasp_output_{CKSUM}.txt contains execution results of s(CASP) code for a specific input program.
• The scasp_script/scasp_{CKSUM}.pl is s(CASP) code for a specific input program to generate counterfactual configurations.

4. Results

The results of running verification tool using ConfigTuneX are at the directory {PROJ_DIR}/_results/configtunex/rf/compositerules/foldse_{TOOL_NAME}_2labels_{FOLD_NUM}/