AutoCL

This is the reproduction package for AutoCL, which contains the AutoCL Docker image and experiment results.evalaution.xlsx: all evaluation results.Benchmark: Benchmark suite/category (Simulink, SV-COMP, LeetCode, Embedded).Program: Program/task identifier within the suite.st: Primary state variable used.LoC: Lines of code of the target C program analyzed.# Nest: Whether the target program contains nested loops (O = has loop, X = no loop).Dom(st): Size of the domain of st (number of possible values).# Vars: Total number of observable variables.Bool: Number of Boolean variables.Enum: Number of enumerated variables.Num: Number of numeric variables (integer or float).states: Number of states in the last learned model (by AutoCL).transitions: Number of transitions in the last learned model (by AutoCL).iter: Total number of active learning iterations executed.pred (s): Total time spent in transition predicate synthesis (seconds).model (s): Total time spent in model construction (seconds).teach (s): Total time spent in teaching (seconds).total (s): End-to-end runtime in seconds (timeouts are recorded as >3h).# invalid: Total number of infeasible observations during teaching.violation: Number of specification violations when checking the final model (N/A means no usable count was produced).# specs: Number of specifications generated/checked for the final model.model abs (s): Time spent on model abstraction performed by the dynamic mapper (seconds).trace abs (s): Time spent on trace abstraction (seconds).refine (s): Time spent on BV refinement (seconds).refine (#): Number of BV refinements performed.obs. usage: Average observation-usage ratio only for BV refinement, reported as a percentage (N/A if unavailable).# BV (learn): Average number of Boolean variables used for learning (N/A if unavailable).# BV (teach): Average number of Boolean variables used for teaching (N/A if unavailable).trace conflict: (Static-Mapper only) Whether trace conflicts occurred (O = conflict detected, X = none).#BV: (Static-Mapper only) Total number of Boolean variables used by the static mapper. Results info (the 'test' directory): For each benchmark suite, there are experiment results for autocl (AutoCL), autocl_coarse (AutoCL-Coarse), autocl_fine (AutoCL-Fine), autocl_static_mapper (Static Mapper), and baseline. Inside each directory, you can find the results of each approach on individual benchmarks.input.txt: The input file required to run AutoCL.result.txt: The text outputs produced during the execution of AutoCL.code/ : Contains code mainly used during the teaching phase. code_proof.c: completeness checking code; code.c: feasibility checking code; model.c: instrumented target program for trace collection; spec_check.c: code for checking the generated specifications; learn_bv.txt and learn_bv_events.txt: conflict group for BV refinement and synthesized predicates from the group; and pred.txt and pred.audit.txt: the list of extracted predicates used only for the static mapper and the log specifying how each predicate is extracted.models/ : Contains PNG images of the learned SFAs and text files of the guard predicates for each learning iteration.traces/ : trace[N].txt: trace groups used for synthesizing guard predicates; and trace[N]_events.txt: symbolic lifting used for SFA construction.How to reproduce (It works on Ubuntu 20 or 22):Download all files and unpack them ("tar -xzf test.tar.gz" and "docker load -i autocl.tar.gz").For a given benchmark set, remove the directory of the approach you want to reproduce (autocl, autocl_coarse, autocl_fine, autocl_static_mapper, or baseline). (e.g., "cd test/Embedded ; rm -rf autocl")Run the corresponding shell script with the same name as the deleted directory. (e.g., "sh autocl.sh")After all runs have completed, execute `python3 stat/results.py`. Then, run `python3 stat/graph.py` to generate `stat/barchart_solved.png` (Fig. 8). Also, run `python3 stat/table.py` to generate `stat/table.tex` (Tables 1--4).