Verifier interface instead of ModelChecker

[ThomasHaas]

I added a new Verifier interface which is implemented by AssumeSolver/RefinementSolver and VerificationTaskSolver uses this interface instead of the previous ModelChecker class. The interface is not SMT-specific and requires the solver to just return a VerificationResult (the result's model is still an IREvaluator, which is currently SMT-specific though).

I renamed ModelChecker to SMTModelChecker and simplified it. It is no longer task-specific and simply provides utility for SMT-based approaches (essentially just managing prover and solver context).

Possible TODOs:

• Move the static utility processing and analysis methods from SMTModelChecker to somewhere else. [EDIT: Won't move.]
• Maybe rename Verifier to VerifierBackend to make it more distinguished from VerificationTaskSolver which uses Verifier(Backend) to solve tasks. [EDIT: Not important]
• [EDIT: resolved] Add new Exception types to TaskSolvers and/or Verifiers. Our VerificationTaskSolver.run throws SolverException, InterruptedException, InvalidConfigurationException of which the SolverException originates from SMT solvers (though we could reuse the exception beyond just SMT solvers).
  Currently, I have not decided what exceptions Verifier.verify should throw and simply omitted them: this forces all actually thrown exceptions to be wrapped into a RuntimeException.

[github-actions]

Performance comparison

Linux x64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	16.046 ± 0.436 s	16.336 ± 0.293 s	➖ -1.8% [-7.8%, +4.1%]	UNKNOWN
benchmarks/locks/mutex_musl.c	30.847 ± 4.102 s	30.389 ± 3.160 s	➖ +1.2% [-17.8%, +20.2%]	UNKNOWN
benchmarks/lfds/dglm.c	21.743 ± 0.564 s	21.044 ± 1.007 s	➖ +3.2% [-28.0%, +34.4%]	UNKNOWN
benchmarks/lfds/ms.c	34.870 ± 1.213 s	36.995 ± 4.240 s	➖ -5.9% [-54.9%, +43.1%]	UNKNOWN
benchmarks/lfds/treiber.c	11.697 ± 0.627 s	11.727 ± 0.626 s	➖ -0.4% [-35.7%, +34.9%]	UNKNOWN
benchmarks/lfds/safe_stack.c	8.922 ± 0.702 s	9.353 ± 0.767 s	➖ -5.7% [-97.5%, +86.2%]	UNKNOWN
benchmarks/challenging/cna.c	35.974 ± 1.164 s	36.730 ± 1.411 s	➖ -2.2% [-39.5%, +35.1%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	7.116 ± 0.067 s	7.177 ± 0.224 s	➖ -0.9% [-23.4%, +21.6%]	UNKNOWN
benchmarks/locks/mutex_musl.c	5.974 ± 0.596 s	5.478 ± 0.146 s	➖ +7.7% [-49.7%, +65.0%]	UNKNOWN
benchmarks/challenging/cna.c	16.677 ± 2.272 s	16.355 ± 2.019 s	➖ +1.6% [-40.7%, +43.9%]	UNKNOWN
benchmarks/challenging/wsq.c	6.877 ± 0.263 s	6.768 ± 0.073 s	➖ +1.5% [-18.1%, +21.2%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	21.653 ± 2.599 s	22.757 ± 1.257 s	➖ -5.6% [-42.7%, +31.5%]	UNKNOWN
benchmarks/locks/mutex_musl.c	20.956 ± 0.237 s	19.243 ± 1.037 s	➖ +8.2% [-15.2%, +31.6%]	UNKNOWN
benchmarks/lfds/dglm.c	5.918 ± 0.147 s	5.757 ± 0.560 s	➖ +2.8% [-44.4%, +50.0%]	UNKNOWN
benchmarks/lfds/ms.c	25.187 ± 3.272 s	24.752 ± 3.012 s	➖ +0.0% [-121.8%, +121.9%]	UNKNOWN
benchmarks/lfds/treiber.c	18.955 ± 0.488 s	19.035 ± 0.988 s	➖ -0.4% [-25.4%, +24.5%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	289.413 ± 9.348 s	289.896 ± 8.698 s	➖ -0.2% [-19.7%, +19.2%]

2 benchmark(s) omitted because both averages were below 5 seconds.

macOS ARM64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	24.071 ± 1.433 s	25.751 ± 1.119 s	➖ -7.1% [-38.4%, +24.1%]	UNKNOWN
benchmarks/locks/mutex_musl.c	32.041 ± 5.702 s	30.713 ± 4.193 s	➖ +3.2% [-57.3%, +63.8%]	UNKNOWN
benchmarks/lfds/dglm.c	44.436 ± 8.712 s	49.838 ± 3.155 s	➖ -14.2% [-108.4%, +80.0%]	UNKNOWN
benchmarks/lfds/ms.c	69.000 ± 7.211 s	78.000 ± 2.000 s	➖ -13.8% [-75.8%, +48.3%]	UNKNOWN
benchmarks/lfds/treiber.c	18.141 ± 1.575 s	16.001 ± 1.743 s	➖ +11.8% [-13.9%, +37.6%]	UNKNOWN
benchmarks/lfds/safe_stack.c	9.349 ± 1.799 s	8.654 ± 0.780 s	➖ +4.6% [-128.8%, +138.0%]	UNKNOWN
benchmarks/challenging/cna.c	42.675 ± 5.036 s	38.356 ± 3.184 s	➖ +9.0% [-81.4%, +99.4%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	21.750 ± 0.164 s	20.252 ± 0.972 s	➖ +6.9% [-19.1%, +32.8%]	UNKNOWN
benchmarks/locks/mutex_musl.c	14.500 ± 0.786 s	15.965 ± 2.009 s	➖ -9.9% [-64.4%, +44.6%]	UNKNOWN
benchmarks/lfds/dglm.c	15.363 ± 2.512 s	13.500 ± 0.710 s	➖ +11.0% [-51.5%, +73.4%]	PASS
benchmarks/lfds/ms.c	14.114 ± 2.053 s	11.825 ± 0.887 s	➖ +15.6% [-21.8%, +53.0%]	UNKNOWN
benchmarks/challenging/cna.c	33.890 ± 6.179 s	31.345 ± 7.936 s	➖ +8.1% [-39.5%, +55.7%]	UNKNOWN
benchmarks/challenging/wsq.c	13.897 ± 1.259 s	15.041 ± 0.908 s	➖ -8.6% [-56.2%, +39.0%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	59.684 ± 6.340 s	43.873 ± 3.161 s	✅ +26.3% [+6.4%, +46.2%]	UNKNOWN
benchmarks/locks/mutex_musl.c	30.648 ± 4.778 s	31.174 ± 2.978 s	➖ -2.4% [-48.3%, +43.5%]	UNKNOWN
benchmarks/lfds/dglm.c	11.479 ± 0.778 s	11.597 ± 0.618 s	➖ -1.3% [-48.2%, +45.6%]	UNKNOWN
benchmarks/lfds/ms.c	47.801 ± 1.860 s	57.835 ± 1.966 s	➖ -21.1% [-61.8%, +19.5%]	UNKNOWN
benchmarks/lfds/treiber.c	24.418 ± 3.401 s	29.021 ± 4.301 s	➖ -20.6% [-170.9%, +129.7%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	527.260 ± 12.847 s	528.742 ± 0.975 s	➖ -0.3% [-15.2%, +14.5%]

[ThomasHaas]

I made a change that affects a lot of code: ResultStatus is now specialized to VerificationStatus and only available as part of a VerificationResult. This enables us to use a custom EnumerationStatus in #1086 instead of the usual PASS/FAIL/UNKNOWN if we want to.