usi-verification-and-security / golem Goto Github PK

Solver for Constrained Horn Clauses

License: MIT License

CMake 0.82% C++ 97.92% C 0.22% Shell 0.15% SMT 0.78% Python 0.10%

golem's Introduction

Golem

Golem is a solver for Constrained Horn Clauses (CHCs). It accepts the input in the format of (extended) SMT-LIB 2.6, as defined by CHC-COMP.

Installation

The easiest way is to download the executables from our release page. This way, all dependencies are already bundled in the executable.

Building from source

Golem can be compiled on Linux and MacOS. It uses CMake for build configuration. Golem depends on OpenSMT for SMT solving and interpolation. If you already have OpenSMT installed, you can pass the path using -DOPENSMT_HOME option to cmake command. Note that Golem requires a specific version of OpenSMT, currently v2.6.0. Otherwise, cmake will download the latest compatible version of OpenSMT and build it as a subproject.

Usage

You can view the usage in the help message after running

$ golem -h

At the moment, you should specified the SMT theory used in the CHC encoding with -l option. The supported theories are QF_LRA and QF_LIA, i.e., the linear arithmetic over reals or integers. Golem now has limited support to automatically detect the theory from the script, so the option is no longer mandatory, but still recommended.

Backend engines

Golem currently supports 6 different backend algorithms for solving CHCs.

spacer [default]
bmc
imc
kind
lawi
tpa
split-tpa

Spacer engine is the default one. It represents our own implementation of the algorithm from this paper. You might be familiar with the original implementation of Spacer inside Z3.

BMC engine implements the simple bounded model checking algorithm which checks for existence of increasingly longer counterexample paths in a given transition system. It uses incremental capibilities of the underlying SMT solver to speed up the process.

IMC engine implements the original McMillan's interpolation-based model-checking algorithm from this paper. Currently, it only supports transition systems.

KIND engine implements very basic k-induction algorithm from this paper. Currently, it only supports transition systems.

LAWI stands for Lazy Abstraction With Interpolants. The algorithm is described in this paper. It is also known as Impact, which was the first tool where the algorithm was implemented. LAWI engine supports only linear systems of Horn clauses.

TPA stands for Transition Power Abstraction. It is an algorithm we have developed recently with the goal to detect long counterexample quickly. The description of the algorithm can be found in this paper. TPA supports a subset of linear CHC systems that represent DAGs of transition systems.

split-TPA is a different instantiation of the TPA paradigm and is typically more powerful than TPA on satisfiable (safe) CHC systems.

Golem also supports multiprocessing run of the few engine simultaneously. For example, to run split-tpa, spacer and lawi in parralel golem should be called like this:

golem -l {Logic} -e split-tpa,spacer,lawi {File}

Witness validation and printing

Golem supports internal validation of witnesses for its answer using --validate option. Witness for sat is a model, an interpretation of the predicates. Witness for unsat is a proof. This option is still experimental. For example, tpa/split-tpa does not always produce the witness yet.

To obtain the produced model or proof of unsatisfiability, use --print-witness.

golem's People

Contributors

Stargazers

Watchers

Forkers

gitter-badger pkalita595 stepanhen erkansukgen m4mbo jakubsarnik

golem's Issues

Crash when printing sat witnesses

With CHC-LIA-Lin_110, Golem (v0.4.0) produces an output when run without arguments, but with --print-witness, it crashes with the following message:

terminate called after throwing an instance of 'std::out_of_range'
  what():  _Map_base::at
Aborted (core dumped)

Check handling of auxiliary variables after inlining

After resolving on some predicate in multiple clauses, the same auxiliary variable from one clause may end up in multiple clauses. This is undesirable, because it causes problems in engines that make global, not just local satisfiability checks.

Moreover, former state variables may become auxiliary in the new clause and hence they should be renamed, so they do not confuse our versioning system.

Hints:

Look at ChcDirectedHyperGraph::contractVertex and its requiresRenamingAuxiliaryVars flag.
Possibly add another preprocessing pass that will try to eliminate auxiliary variables after other rewriting passes.

std::out_of_range when running with --print-witness

When running chc-LIA_387 from CHC-COMP 2023, Golem outputs the following:

For the command golem chc-LIA_387.smt2 the output is sat.

For the command golem --print-witness chc-LIA_387.smt2 the output is as below.

sat
terminate called after throwing an instance of 'std::out_of_range'
  what():  basic_string::erase: __pos (which is 18446744073709551615) > this->size() (which is 6)
Aborted (core dumped)

Fix print-witness to not include definitions for top and bottom (true and false)

Add a formatter to the CI

SAT witnesses with invalid function names

For some of the CHC-comp instances, e.g., CHC-LIA-Lin_307 and CHC-LIA-Lin_314, Golem generates witnesses with invalid function names.

CHC-LIA-Lin_307 has functions names as fail$unknown:38, and I get the error syntax error, unexpected TK_KEY, expecting '('.
CHC-LIA-Lin_314 has functions names as <Main: void main(JayArray_java_lang_String)>_Block10_6, and I get the error Syntax error at line 4 near :.

After manually enclosing the function names as |funName|, the witnesses can validated by an SMT solver.

Small issues that require further investigation

Long time for validation of a model; LAWI engine; chc-comp-21/LRA-TS/chc-LRA-TS_111.smt2
Golem creating a huge number of terms in OpenSMT; Spacer engine; chc-comp-21/LIA-NonLin/chc-LIA-NonLin_522.smt2

Assertion violation in computing witness with Spacer engine

chc22/LIA-Lin/chc-LIA-Lin_434.smt2

Alethe proof rejected

Alethe proof produced by golem is rejected by carcara on chc-LIA-Lin_366. This is another problem on this benchmark revealed after the fix of #55.

Here is the carcara output:

[ERROR] checking failed on step 't145814' with rule 'resolution': pivot was not eliminated: '(main_1 1 2 286 158 9 0)'
invalid

Usage of negation in models produced not in line with smt-lib

Models produced by golem seem to contain elements such as -1, which are not compliant with smt-lib. When trying to validate a model with SMT solvers strictly following smt-lib, e.g., cvc5 and veriT, I get parsing errors. Solvers that are not so strict, e.g., z3 and opensmt, do not give any errors.

Example

On chc-comp24-LIA-001.smt2 the model produced under golem --print-witness contains elements such as (<= -2 (* -1 |x#6| ) ), leading to errors such as the ones below.

cvc5 error: (error "Parse Error: test.smt2:4.16: Symbol '-1' not declared as a variable")
veriT error: (error "smt2_term: unresolved symbol -1 on line 4")

This can be fixed by substituting -1 by (- 1).

Improve auxiliary variable elimination in Normalizer

Currently, some auxiliary variables are not eliminated, because the code for detecting substitutions does not distinguish between the variables we want to keep and variables we want to eliminate.
Thus, from an equality s = aux + 1 (where s is a state variable) it may pick s as the variable to eliminate.

It would be better if the code preferred TBE (to be eliminated) variables over the other ones.

Example to test: 2021/LIA-Lin/chc-LIA-Lin_569.smt2

Add more testing infrastructure

Add infrastructure for

testing Alethe proof production
regression SMT-LIB tests

Alethe proofs rejected with rule mod_simplify

The alethe proofs for chc-LIA_366 and chc-LIA_379, from CHC-COMP 2023, are being rejected by carcara.

Production command: golem --logic QF_LIA --print-witness --proof-format alethe [file.smt2]
Checking command: carcara check --allow-int-real-subtyping --expand-let-bindings [proof.alethe] [file.smt2]

Checking output for chc-LIA_366:

[ERROR] checking failed on step 't77427' with rule 'mod_simplify': expected term '1' to be numerical constant 9.0
invalid

Checking output for chc-LIA_379:

[ERROR] checking failed on step 't6544' with rule 'mod_simplify': expected term '26' to be numerical constant 63.0
invalid

std::bad_alloc when running a SAT instance with --print-witness

When running chc-LIA_177 from CHC-COMP 2023, Golem outputs the following:

For the command golem chc-LIA_177.smt2 the output is sat.

For the command golem --print-witness chc-LIA_177.smt2 the output is as below.

sat
terminate called after throwing an instance of 'std::bad_alloc'
  what():  std::bad_alloc
Aborted (core dumped)

Steps to make Golem fully usable by Korn

Add solution-translating mechanism in order to recompute solution when preprocessing is used
Compute counterexamples from Spacer engine
Enable building fully static library (+ make a release of such binary)