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

XCFA-refactor 2023 [draft] #198

Closed leventeBajczi closed 9 months ago

leventeBajczi commented 1 year ago

This PR merges the xcfa-refactor branch.

Main features of the PR:

leventeBajczi commented 1 year ago

@csanadtelbisz: Sonar fails, because some tests ultimately fail. Relevant log:

Caused by:
2023-09-10T13:13:40.7201330Z         java.lang.UnsupportedOperationException: Solver Z3 not supported
2023-09-10T13:13:40.7201918Z             at hu.bme.mit.theta.solver.SolverManager.resolveSolverFactory(SolverManager.java:40)
2023-09-10T13:13:40.7202556Z             at hu.bme.mit.theta.xcfa.passes.LoopUnrollPass.<clinit>(LoopUnrollPass.kt:46)
2023-09-10T13:13:40.7202939Z             ... 5 more

Can you take a look if this has something to do with the moved registerSolverFactories method in XcfaCli? I think I saw some modifications there in your pr (#202). Let me know if I'm mistaken.

csanadtelbisz commented 1 year ago

@leventeBajczi The solver issue arose due to the fact that LoopUnrollPass invokes a solver (unprecedented in xcfa passes before). Tests did not register solvers. I added a dependency on Z3 and hardcoded the usage of Z3 in LoopUnrollPass. Also fixed bugs reported by sonarcloud.

szdan97 commented 1 year ago

A projection should be given in XcfaAnalysis.getXcfaAbstractor in order to avoid performance degradation compared to the original xcfa analysis, as the lack of non-trivial projection leads to a lot of unnecessary covering checks

csanadtelbisz commented 1 year ago

The WebDebuggerLogger is always enabled and it is responsible for a considerable portion of runtime. See the following lines: https://github.com/ftsrg/theta/blob/c43d0a148d0d19bcf2e01ef2547336364a1e5d71/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java#L94-L97 As it serves only debugging purposes, it should be disabled by default. @AdamZsofi git blame shows that you are the author of this change.

The following profiler output confirms the problem. The WebDebuggerLogger takes ~1/3 (more than 10 seconds in this case) of all CPU time. image

csanadtelbisz commented 1 year ago

Wrong result is given for the unreach-call property on the following tasks in the eca-rers2012 category of sv-benchmarks:

Config 1: --strategy DIRECT --maxenum 1 --loglevel RESULT --refinement SEQ_ITP --lbe LBE_SEQ --search ERR --prunestrategy FULL --predsplit ATOMS --cex-monitor DISABLE --domain EXPL Problem17_label11.yml

Config 2: --strategy DIRECT --maxenum 1 --loglevel RESULT --refinement SEQ_ITP --lbe LBE_SEQ --search ERR --prunestrategy FULL --predsplit ATOMS --cex-monitor DISABLE --domain PRED_CART Problem10_label30.yml, Problem11_label40.yml, Problem15_label49.yml

leventeBajczi commented 1 year ago

Thanks for the review! I'll get around to incorporating its findings hopefully this weekend.

AdamZsofi commented 1 year ago

@AdamZsofi WebDebuggerLogger still has an overhead, see the following lines:

https://github.com/ftsrg/theta/blob/fdc40cf95ba46bb8a94a791a785f031db2010a2a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java#L94-L95

Time taken by these lines: image

Thanks for telling me. Fixed, there should be no overhead now.

sonarcloud[bot] commented 9 months ago

Quality Gate Passed Quality Gate passed

Issues
4687 New issues

Measures
0 Security Hotspots
60.7% Coverage on New Code
1.8% Duplication on New Code

See analysis details on SonarCloud

github-actions[bot] commented 9 months ago

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

:white_check_mark: ConcurrencySafety-Main (3 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ConcurrencySafety-Main/theta.2024-02-15_17-38-16.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ConcurrencySafety-Main/theta.2024-02-15_17-38-16.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ConcurrencySafety-Main, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:38:16 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az841-158 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2761.818 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ConcurrencySafety-Main Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 6.25 2.89 None pthread-atomic/read_write_lock-1.yml true 12.52 4.56 None pthread-wmm/rfi003_tso.yml TIMEOUT (Parsing OK) 120.35 90.41 None pthread/lazy01.yml false(unreach-call) 9.08 3.63 None pthread-wmm/mix000.oepc.yml false(unreach-call) 13.14 4.72 None ----------------------------------------------------------------------------------------------------------- Run set 1 done 41.12 107.25 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 3 correct true: 1 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 2 Score: 4 (max: 8) ```
:white_check_mark: ConcurrencySafety-MemSafety (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-02-15_17-38-00.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-02-15_17-38-00.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety date: Thu, 2024-02-15 17:38:00 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az891-442 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2689.845 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety Run set 4 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 6.14 2.73 None pthread-atomic/read_write_lock-1.yml true 8.96 3.59 None pthread-wmm/rfi003_tso.yml true 9.54 3.71 None pthread/lazy01.yml true 7.23 3.13 None pthread-wmm/mix000.oepc.yml true 10.21 4.04 None ----------------------------------------------------------------------------------------------------------- Run set 4 done 42.09 17.73 - Statistics: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:white_check_mark: ConcurrencySafety-NoOverflows (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-02-15_17-38-00.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-02-15_17-38-00.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race, SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:38:00 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1490-322 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.513 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows Run set 3 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 6.09 2.72 None pthread-atomic/read_write_lock-1.yml true 9.92 3.84 None pthread-wmm/rfi003_tso.yml true 11.42 4.31 None pthread/lazy01.yml true 7.87 3.24 None pthread-wmm/mix000.oepc.yml true 10.05 3.82 None ----------------------------------------------------------------------------------------------------------- Run set 3 done 45.34 18.44 - SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:white_check_mark: NoDataRace-Main (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-NoDataRace-Main/theta.2024-02-15_17-38-09.results.SV-COMP24_no-data-race.NoDataRace-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-NoDataRace-Main/theta.2024-02-15_17-38-09.results.SV-COMP24_no-data-race.NoDataRace-Main.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race.NoDataRace-Main, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:38:09 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1153-308 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3206.321 MHz ram: 16757.784576 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race.NoDataRace-Main Run set 2 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 6.18 2.73 None pthread-atomic/read_write_lock-1.yml true 11.94 4.41 None pthread-wmm/rfi003_tso.yml true 14.70 5.31 None pthread/lazy01.yml true 7.61 3.24 None pthread-wmm/mix000.oepc.yml true 13.72 4.95 None ----------------------------------------------------------------------------------------------------------- Run set 2 done 54.15 21.16 - SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:question: ReachSafety-Arrays (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Arrays/theta.2024-02-15_17-36-31.results.SV-COMP24_unreach-call.ReachSafety-Arrays.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Arrays/theta.2024-02-15_17-36-31.results.SV-COMP24_unreach-call.ReachSafety-Arrays.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Arrays, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:36:31 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az775-790 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3115.455 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Arrays Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------------------------------- array-examples/standard_partition_ground-2.yml Parsing OK 112.93 101.17 None array-crafted/mapavg4.yml Parsing OK 114.40 101.23 None array-programs/copysome2-1.yml Parsing OK 112.41 101.17 None array-examples/sanfoundry_24-1.yml Parsing OK 8.95 3.87 None array-multidimensional/max-2-u.yml Parsing OK 118.94 101.21 None --------------------------------------------------------------------------------------------------------------- Run set 1 done 21.90 409.18 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 10) ```
:white_check_mark: ReachSafety-BitVectors (2 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-BitVectors/theta.2024-02-15_17-35-33.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-BitVectors/theta.2024-02-15_17-35-33.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-BitVectors, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:35:33 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1249-53 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3228.735 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-BitVectors Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------ bitvector/gcd_4.yml true 10.32 4.20 None bitvector/soft_float_1-3a.c.cil.yml Parsing OK 13.69 5.21 None bitvector-regression/integerpromotion-3.yml false(unreach-call) 7.07 3.31 None bitvector/sum02-1.yml Parsing OK 8.27 3.52 None bitvector-loops/diamond_2-1.yml Parsing OK 8.89 3.59 None ------------------------------------------------------------------------------------------------------------ Run set 1 done 47.66 20.34 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 2 correct true: 1 correct false: 1 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 3 Score: 3 (max: 6) ```
:question: ReachSafety-Combinations (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Combinations/theta.2024-02-15_17-37-11.results.SV-COMP24_unreach-call.ReachSafety-Combinations.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Combinations/theta.2024-02-15_17-37-11.results.SV-COMP24_unreach-call.ReachSafety-Combinations.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Combinations, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:37:11 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az700-909 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2636.776 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Combinations Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------------- pc_sfifo_3.cil+token_ring.02.cil-2.yml Parsing OK 48.29 25.97 None Problem05_label47+token_ring.02.cil-1.yml TIMEOUT (Parsing OK) 122.07 80.27 None pc_sfifo_3.cil+token_ring.11.cil-1.yml TIMEOUT (Parsing OK) 120.93 92.32 None Problem05_label45+token_ring.01.cil-2.yml TIMEOUT (Parsing OK) 121.62 75.91 None pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml Parsing OK 66.79 33.41 None ---------------------------------------------------------------------------------------------------------------------- Run set 1 done 108.97 309.51 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 5) ```
:white_check_mark: ReachSafety-ControlFlow (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-ControlFlow/theta.2024-02-15_17-35-40.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-ControlFlow/theta.2024-02-15_17-35-40.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-ControlFlow, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:35:40 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1016-227 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.576 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-ControlFlow Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------- longjmp/68-longjmp_18-simple-else_unknown_1_pos.yml Parsing OK 8.92 3.64 None locks/test_locks_11.yml Parsing OK 117.95 101.37 None locks/test_locks_5.yml true 14.40 5.33 None longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml Parsing OK 9.00 3.68 None longjmp/68-longjmp_11-counting-return_true.yml Parsing OK 6.76 3.14 None -------------------------------------------------------------------------------------------------------------------- Run set 1 done 42.33 117.69 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 8) ```
:question: ReachSafety-ECA (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-ECA/theta.2024-02-15_17-38-51.results.SV-COMP24_unreach-call.ReachSafety-ECA.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-ECA/theta.2024-02-15_17-38-51.results.SV-COMP24_unreach-call.ReachSafety-ECA.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-ECA, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:38:51 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1055-471 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3142.287 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-ECA Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------- eca-rers2012/Problem06_label18.yml TIMEOUT (Parsing OK) 120.54 79.50 None eca-rers2012/Problem06_label11.yml TIMEOUT (Parsing OK) 121.09 74.55 None eca-programs/Problem101_label07.yml TIMEOUT 121.58 69.38 None eca-rers2012/Problem05_label44.yml TIMEOUT (Parsing OK) 120.11 73.92 None eca-rers2012/Problem04_label05.yml TIMEOUT (Parsing OK) 120.60 77.87 None ---------------------------------------------------------------------------------------------------- Run set 1 done 0.62 378.16 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 7) ```
:white_check_mark: ReachSafety-Floats (3 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Floats/theta.2024-02-15_17-38-21.results.SV-COMP24_unreach-call.ReachSafety-Floats.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Floats/theta.2024-02-15_17-38-21.results.SV-COMP24_unreach-call.ReachSafety-Floats.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Floats, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:38:21 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az585-501 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2898.016 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Floats Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------- float-benchs/float_double.yml true 6.38 2.86 None float-benchs/zonotope_loose.c.v+cfa-reducer.yml Parsing OK 8.93 4.61 None float-benchs/float_int_inv_square.yml false(unreach-call) 10.77 6.37 None floats-cdfpl/square_3.yml TIMEOUT (false(unreach-call)) 120.37 115.32 None floats-cbmc-regression/float11.yml true 6.07 3.05 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 30.62 133.24 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 3 correct true: 2 correct false: 1 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 2 Score: 5 (max: 8) ```
:question: ReachSafety-Hardware (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Hardware/theta.2024-02-15_17-38-43.results.SV-COMP24_unreach-call.ReachSafety-Hardware.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Hardware/theta.2024-02-15_17-38-43.results.SV-COMP24_unreach-call.ReachSafety-Hardware.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Hardware, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:38:43 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1382-899 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.297 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Hardware Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------ btor2c-lazyMod.arbitrated_top_n4_w16_d32_e0.yml TIMEOUT 120.31 115.88 None btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml TIMEOUT (Parsing OK) 120.44 97.72 None btor2c-lazyMod.extinction.4.prop1-func-interl.yml TIMEOUT (Parsing OK) 120.39 94.83 None btor2c-lazyMod.lup.2.prop1-func-interl.yml TIMEOUT (Parsing OK) 120.52 96.03 None btor2c-lazyMod.train-gate.6.prop1-func-interl.yml Parsing OK 84.85 62.40 None ------------------------------------------------------------------------------------------------------------------ Run set 1 done 72.83 468.99 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 9) ```
:white_check_mark: ReachSafety-Heap (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Heap/theta.2024-02-15_17-35-59.results.SV-COMP24_unreach-call.ReachSafety-Heap.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Heap/theta.2024-02-15_17-35-59.results.SV-COMP24_unreach-call.ReachSafety-Heap.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Heap, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:35:59 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az738-575 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2933.091 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Heap Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------- test09.yml Parsing OK 4.97 2.30 None test15.yml Parsing OK 4.92 2.30 None just_assert.yml true 5.47 2.68 None volatile_alias.yml Parsing OK 4.01 2.16 None mutex_lock_int.c_1.yml Parsing OK 5.04 2.34 None --------------------------------------------------------------------------------------- Run set 1 done 24.41 12.30 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 10) ```
:question: ReachSafety-Loops (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Loops/theta.2024-02-15_17-37-45.results.SV-COMP24_unreach-call.ReachSafety-Loops.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Loops/theta.2024-02-15_17-37-45.results.SV-COMP24_unreach-call.ReachSafety-Loops.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Loops, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:37:45 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1382-899 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2611.36 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Loops Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------- nla-digbench/ps3-ll.yml Parsing OK 110.72 101.20 None loop-crafted/simple_vardep_2.yml Parsing OK 107.26 101.27 None nla-digbench-scaling/divbin_valuebound100.yml Parsing OK 82.87 77.15 None nla-digbench-scaling/mannadiv_valuebound50.yml Parsing OK 6.32 2.82 None nla-digbench-scaling/mannadiv_unwindbound10.yml Parsing OK 7.06 3.09 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 102.38 286.06 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 9) ```
:question: ReachSafety-Recursive (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Recursive/theta.2024-02-15_17-38-27.results.SV-COMP24_unreach-call.ReachSafety-Recursive.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Recursive/theta.2024-02-15_17-38-27.results.SV-COMP24_unreach-call.ReachSafety-Recursive.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Recursive, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:38:27 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az659-196 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2939.021 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Recursive Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------------- recursive-simple/id_o100.yml TIMEOUT (Parsing OK) 120.45 98.62 None recursive-simple/id2_i5_o5-2.yml TIMEOUT (Parsing OK) 120.24 101.10 None recursified_nla-digbench/recursified_geo2-ll.yml ERROR (frontend failed) 1.66 0.74 None recursive/recHanoi03-2.yml TIMEOUT (Parsing OK) 120.29 100.41 None recursified_nla-digbench/recursified_lcm2.yml ERROR (frontend failed) 1.59 0.70 None ----------------------------------------------------------------------------------------------------------------- Run set 1 done 3.61 303.29 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 9) ```
:question: ReachSafety-Sequentialized (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Sequentialized/theta.2024-02-15_17-40-07.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-Sequentialized/theta.2024-02-15_17-40-07.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Sequentialized, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:40:07 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az530-262 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3074.801 MHz ram: 16757.788672 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Sequentialized Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------------------- systemc/transmitter.12.cil.yml TIMEOUT (Parsing OK) 120.58 91.70 None seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml Parsing OK 14.56 5.43 None systemc/pipeline.cil-1.yml TIMEOUT (Parsing OK) 120.12 97.78 None seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml Parsing OK 17.79 6.46 None seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml Parsing OK 29.83 11.10 None ------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 60.02 213.99 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 6) ```
:white_check_mark: ReachSafety-XCSP (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-XCSP/theta.2024-02-15_17-38-33.results.SV-COMP24_unreach-call.ReachSafety-XCSP.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor/BenchexecResults-ReachSafety-XCSP/theta.2024-02-15_17-38-33.results.SV-COMP24_unreach-call.ReachSafety-XCSP.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-XCSP, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Thu, 2024-02-15 17:38:33 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1152-29 os: Linux-6.2.0-1019-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.943 MHz ram: 16757.78048 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-XCSP Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------- CostasArray-14.yml TIMEOUT (false(unreach-call)) 120.74 96.35 None Dubois-025.yml Parsing OK 22.72 9.77 None aim-100-2-0-unsat-4.yml Parsing OK 34.82 16.62 None AllInterval-014.yml Parsing OK 112.56 101.97 None AllInterval-005.yml false(unreach-call) 12.09 4.50 None ---------------------------------------------------------------------------------------- Run set 1 done 65.71 230.24 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 1 correct true: 0 correct false: 1 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 1 (max: 7) ```