search

ftsrg / theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
http://theta.inf.mit.bme.hu/
Apache License 2.0
49 stars 43 forks source link

Added CHC algorithm to Xsts #289

Closed leventeBajczi closed 3 months ago

leventeBajczi commented 3 months ago

This PR adds support for the Horn solving backend for Xstss.

Right now we don't support proof/CeX transformation, but that should be trivial, if it turns out this feature is useful.

I've added some tests, and it seems like there are no mistakes on the simple examples, but a more thorough testing would definitely be necessary.

Also, if it turns out this is useful, we could also think about useful ways of representing correctness proofs, because the horn solvers give us invariants for both the "env" and "trans" steps.

leventeBajczi commented 3 months ago

Unfortunately, horn solvers tend not to support custom datatypes and sorts, so I replaced every enumType with an int.

sonarcloud[bot] commented 3 months ago

Quality Gate Passed Quality Gate passed

Issues
26 New issues
0 Accepted issues

Measures
0 Security Hotspots
63.9% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarCloud

github-actions[bot] commented 3 months ago

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

task set BOUNDED CEGAR HORN
ConcurrencySafety-Main :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (19 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ConcurrencySafety-MemSafety :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (43 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ConcurrencySafety-NoOverflows :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (39 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
NoDataRace-Main :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (24 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Arrays :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (1 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-BitVectors :white_check_mark: (14 / 0 / 46) HTML/CSV :white_check_mark: (14 / 0 / 46) HTML/CSV :white_check_mark: (12 / 0 / 46) HTML/CSV
ReachSafety-Combinations :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (3 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-ControlFlow :white_check_mark: (3 / 0 / 50) HTML/CSV :white_check_mark: (2 / 0 / 50) HTML/CSV :white_check_mark: (17 / 0 / 50) HTML/CSV
ReachSafety-ECA :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Floats :exclamation: (7 / 1 / 50) HTML/CSV :white_check_mark: (15 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Hardware :white_check_mark: (2 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Heap :white_check_mark: (2 / 0 / 11) HTML/CSV :white_check_mark: (10 / 0 / 11) HTML/CSV :exclamation: (2 / 1 / 11) HTML/CSV
ReachSafety-Loops :white_check_mark: (16 / 0 / 50) HTML/CSV :white_check_mark: (11 / 0 / 50) HTML/CSV :white_check_mark: (12 / 0 / 50) HTML/CSV
ReachSafety-Recursive :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (13 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Sequentialized :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (1 / 0 / 50) HTML/CSV :white_check_mark: (2 / 0 / 50) HTML/CSV
ReachSafety-XCSP :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV