Skip to content

Commit 88591de

Browse files
ChronosymbolicChronosymbolic
committed
add codebase
1 parent e5dedef commit 88591de

215 files changed

Lines changed: 75670 additions & 3 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.gitignore‎

Lines changed: 151 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,151 @@
1+
# Project
2+
*.pk
3+
*.txt
4+
*.xlsx
5+
*.csv
6+
*.m
7+
*.list
8+
*.z3-trace
9+
.DS_Store
10+
FromCmd*
11+
*temp
12+
.idea/
13+
# *.intervals
14+
# *.names
15+
# *.implications
16+
# *.data
17+
# *.attr
18+
19+
# Byte-compiled / optimized / DLL files
20+
__pycache__/
21+
*.py[cod]
22+
*$py.class
23+
24+
# C extensions
25+
*.so
26+
27+
# Distribution / packaging
28+
.Python
29+
tmp/
30+
build/
31+
develop-eggs/
32+
dist/
33+
downloads/
34+
eggs/
35+
.eggs/
36+
lib/
37+
lib64/
38+
parts/
39+
sdist/
40+
var/
41+
tests/
42+
wheels/
43+
pip-wheel-metadata/
44+
share/python-wheels/
45+
*.egg-info/
46+
.installed.cfg
47+
*.egg
48+
MANIFEST
49+
50+
# PyInstaller
51+
# Usually these files are written by a python script from a template
52+
# before PyInstaller builds the exe, so as to inject date/other infos into it.
53+
*.manifest
54+
*.spec
55+
56+
# Installer logs
57+
pip-log.txt
58+
pip-delete-this-directory.txt
59+
60+
# Unit test / coverage reports
61+
htmlcov/
62+
.tox/
63+
.nox/
64+
.coverage
65+
.coverage.*
66+
.cache
67+
nosetests.xml
68+
coverage.xml
69+
*.cover
70+
*.py,cover
71+
.hypothesis/
72+
.pytest_cache/
73+
.vscode/
74+
75+
# Translations
76+
*.mo
77+
*.pot
78+
79+
# Django stuff:
80+
*.log
81+
local_settings.py
82+
db.sqlite3
83+
db.sqlite3-journal
84+
85+
# Flask stuff:
86+
instance/
87+
.webassets-cache
88+
89+
# Scrapy stuff:
90+
.scrapy
91+
92+
# Sphinx documentation
93+
docs/_build/
94+
95+
# PyBuilder
96+
target/
97+
98+
# Jupyter Notebook
99+
.ipynb_checkpoints
100+
101+
# IPython
102+
profile_default/
103+
ipython_config.py
104+
105+
# pyenv
106+
.python-version
107+
108+
# pipenv
109+
# According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
110+
# However, in case of collaboration, if having platform-specific dependencies or dependencies
111+
# having no cross-platform support, pipenv may install dependencies that don't work, or not
112+
# install all needed dependencies.
113+
#Pipfile.lock
114+
115+
# PEP 582; used by e.g. github.com/David-OConnor/pyflow
116+
__pypackages__/
117+
118+
# Celery stuff
119+
celerybeat-schedule
120+
celerybeat.pid
121+
122+
# SageMath parsed files
123+
*.sage.py
124+
125+
# Environments
126+
.env
127+
.venv
128+
env/
129+
venv/
130+
ENV/
131+
env.bak/
132+
venv.bak/
133+
134+
# Spyder project settings
135+
.spyderproject
136+
.spyproject
137+
138+
# Rope project settings
139+
.ropeproject
140+
141+
# mkdocs documentation
142+
/site
143+
144+
# mypy
145+
.mypy_cache/
146+
.dmypy.json
147+
dmypy.json
148+
149+
# Pyre type checker
150+
.pyre/
151+
result/rel_num

‎README.md‎

Lines changed: 108 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,108 @@
1-
# Chronosymbolic-Learning
2-
Artifact for paper "Chronosymbolic: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning"
3-
- code will be open-source soon
1+
# Chronosymbolic Learning
2+
Artifact for paper "Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning"
3+
4+
- See `./experiment` for some important results and configurations
5+
6+
- See `./examples` for examples on how our tool works
7+
8+
## Requirement
9+
Install packages in `requirements.txt`:
10+
11+
```
12+
pip install -r requirements.txt
13+
```
14+
15+
May have to manually set up `PYTHONPATH` and `PATH` properly, `PYTHONPATH=$Z3_BIN/python`, `PATH=$PATH:$Z3_BIN`
16+
17+
Then, prepare the dataset following the instruction in `data/` folder.
18+
19+
## Chronosymbolic Learning
20+
- Support SMT-LIB2 format (check-sat) and Datalog format (rule-query)
21+
22+
- Have executable binaries of decision tree and SVM for Linux and MacOS, and can automatically adapt to the OS
23+
24+
- Control flow implemented in `learner/run_agent.py` `run_Agent` function
25+
26+
- Hyperparameters in `config.yml`
27+
28+
- Temp files generated when calling decision tree and SVM are in `tmp/`
29+
30+
- Implemented some optimization for SMTLIB files generated by [Seahorn](https://seahorn.github.io/)
31+
32+
- Run: `python test.py` with the parameters below:
33+
34+
- Specify file name using `-f FILE_NAME`
35+
36+
- Specify log file (which records how the tool solves the CHC system) using `-l FILE_NAME`
37+
38+
- Specify directory name using `-r -f DIR_NAME` (logs are automatically generated in log/DIR_NAME)
39+
- e.g. `python test.py -f tests/safe/ -a -r -v -t 360 -o result/result.log`
40+
41+
- Or specify a file list using `-b -f FILELIST` (run files specified in the filelist, whose format is the same as `tests/filtered`)
42+
- e.g. `python test.py -a -v -b -f tests/filtered -a -t 360 -o result/result.log`
43+
44+
- Increase log file verbosity using `-v` (not effective in output on screen)
45+
46+
- Adjust timeout using `-t TIMEOUT`, only effective in directory mode
47+
48+
- Specify result file using `-o FILE_NAME`, export a result csv (with success and timing statistics) with the same file name using `-a`
49+
50+
- Start testing from the file index k in the folder `-s k` (index start from zero)
51+
52+
- If you want to run multiple instances, make sure using different `FILE_NAME`-s in the config file to avoid clash (`config.yaml` in default)
53+
54+
- More options see `--help`
55+
56+
# To reproduce Chronosymbolic-single
57+
- `python test.py -f tests/safe -a -r -v -t 360 -o result/result_safe.log`
58+
59+
- `python test.py -f tests/unsafe -a -r -v -t 360 -o result/result_unsafe.log`
60+
61+
- `python test.py -f tests/multiple_pred -a -r -v -t 360 -o result/result_multi.log`
62+
63+
64+
# To run the baselines
65+
## Spacer and GSpacer
66+
- Configure [z3-gspacer-branch](https://github.com/hgvk94/z3/tree/ggbranch)
67+
68+
- Specify the path of z3 (with GSpacer) binary in `utils/run_spacer.py` and `utils/run_spacer_filtered.py`
69+
70+
- Specify a folder name and run `utils/run_spacer.py` or specify a filelist name and run `utils/run_spacer_filtered.py`
71+
72+
- Enable GSpacer: `enable_global_guidance = 1`
73+
74+
## LinearArbitrary and Freqhorn
75+
Refer to [LinearArbitrary](https://github.com/GaloisInc/LinearArbitrary-SeaHorn/tree/master/test) and [Freqhorn](https://github.com/freqhorn/freqhorn)
76+
For LinearArbitrary, you can also try our optimized data-driven learner implementation (set `ClassAgent = Chronosymbolic` to `ClassAgent = DataDrivenLearner` in `test.py` and run it in the same way as Chronosymbolic does)
77+
78+
## Manually "guess" an inductive invariant
79+
In `test.py` `guess_manually` function:
80+
- Modify `s = 'v_0 == v_1'` to indicate the inductive invariant
81+
82+
- Modify `db = load_horn_db_from_file("/home/ssr/chc-tools/chctools/NL/nl-1-chc.smt2", z3.main_ctx())` to indicate SMTLIB2 file name
83+
84+
## Enumeration
85+
- A simple implementation of enumeration-based invariant synthesizer
86+
87+
- Run `learner/enumerate.py` that enumerates through a context-free grammar
88+
89+
## Benchmarks
90+
[CHC-COMP](https://github.com/chc-comp)
91+
92+
[Freqhorn](https://github.com/freqhorn/freqhorn)
93+
94+
[LinearArbitrary](https://github.com/GaloisInc/LinearArbitrary-SeaHorn/tree/master/test)
95+
96+
97+
## Reference
98+
[chc-tools](https://github.com/chc-comp/chc-tools/tree/master/chctools)
99+
100+
[libsvm](http://www.csie.ntu.edu.tw/~cjlin/libsvm)
101+
102+
[ICE-C5](https://github.com/Chenguang-Zhu/ICE-C5)
103+
104+
[LinearArbitrary](https://github.com/GaloisInc/LinearArbitrary-SeaHorn)
105+
106+
[z3](https://github.com/Z3Prover/z3)
107+
108+
[Seahorn](https://seahorn.github.io/)

‎config.yml‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
# FILE_NAME: '/mnt/ramdisk/FromCmd'
2+
# FILE_NAME: '/dev/shm/FromCmd'
3+
FILE_NAME: 'tmp/FromCmd'
4+
LOGGING: on
5+
6+
SVM:
7+
EnableSVM: true
8+
SVMCParameter: 1
9+
SVMCoeffBound: 5
10+
SVMAHyperplane: 0
11+
SVMFreqPos: 0
12+
SVMFreqNeg: 30
13+
14+
DT: # only works for sklearn DT
15+
RNDSeed: 1
16+
Criterion: 'entropy' # entropy or gini
17+
Splitter: 'best' # best or random
18+
19+
OCT: on
20+
MODFind: on # enable automatically find mod patterns
21+
DIVFind: off # enable automatically find div patterns (beta)
22+
MOD: []
23+
DIV: [] # (beta)
24+
# a list of mod and div k features
25+
26+
ValIterMode: false # false: policy iter mode (update a rule until passed)
27+
ClearBodyAppsDP: false
28+
RuleSampleLen: 2
29+
RuleSampleWidth: 1
30+
RuleSampleLenNeg: 1
31+
RuleSampleWidthNeg: 1
32+
33+
FactSampleMaxRound: 10
34+
QuerySampleMaxRound: 2
35+
# prevent from sampling too much monotonic dps, must >= 2
36+
37+
LC: 0
38+
OverflowLimit: 214748364900
39+
Z3_Solver_Timeout: 360000
40+
Z3_Global_Timeout: 10000
41+
42+
EnableMatchFact: true
43+
# may accelerate pos dp collection, but may also trigger more z3 calls
44+
# could enable it when pos dps are sparse. Only for v1 and v2, Chronosymbolic uses is_in_zone()
45+
46+
Dataset:
47+
QueueModePos: off
48+
QueueModeNeg: off
49+
# if enable this, pos/neg dataset is a fixed-length queue
50+
QueueLenPos: 50
51+
QueueLenNeg: 50
52+
QueueTentNegProp: 0.5
53+
QueueRealNegProp: 0.5
54+
55+
56+
RelationUpperBound: 500
57+
# constrain chc relation number
58+
59+
SampleBatchSize: 0
60+
61+
InitPhase: on
62+
UseSafeZone: true
63+
UseUnsafeZone: true
64+
# expansion related
65+
Expansion:
66+
UseExpansion: true
67+
ForceExp: false
68+
BodyCstrExpUB: 700
69+
NewZoneExpUB: 1500
70+
InitExpMinIter: 3
71+
InitExpMaxIter: 7
72+
FreeVarUB: 500
73+
74+
Verbosity:
75+
PrintCstr: off
76+
PrintNewCandFreq: 50
77+
PrintCex: 5
78+
# PrintNewCandFreq: 1
79+
# PrintCex: 1
80+
81+
Strategy:
82+
# SafeZoneUsage: '(self.total_iter // 200) % 2 == 0' # if you want fix UseSafeZone = True, set 'True'
83+
# UnsafeZoneUsage: '(self.total_iter // 100) % 2 == 0'
84+
SafeZoneUsage: 'True'
85+
UnsafeZoneUsage: 'True'

‎horndb/__init__.py‎

Whitespace-only changes.

0 commit comments

Comments
 (0)