Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

MDD-based analysis #274

Closed
wants to merge 211 commits into from
Closed

MDD-based analysis #274

wants to merge 211 commits into from

Conversation

mondokm
Copy link
Contributor

@mondokm mondokm commented Jul 5, 2024

This PR contains the following:

  • Expression MDDs (hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression package)
  • Direct petrinet-based analyses (theta-petrinet-analysis subproject)
  • BFS, Saturation and Generalized Saturation fixed point enumaration algorithms
  • Saturation-based analysis for STS and XSTS
  • Saturation-based analysis for MonolithicExpr

@mondokm
Added interchange.pnml project to xsts subproject
692f8aa
@mondokm
Merge branch 'master' into zeta-merge
735dcfd
@mondokm
Added zeta to theta repo
203b2da
@mondokm
Removed redundant pnml models, added delta jar
641094e
@mondokm
Unified xsts-cli and zeta cli
76088e1
@mondokm
Added saturation test cases
35ac696
@mondokm
Refactoring
733ddc1
@mondokm
Renamed pnml-frontend to petrinet-frontend
730412c
@mondokm
Removed clipboard paste from gsat test
7e4f072
@mondokm
Restructured petrinet-frontend into 3 modules
d54529d
@mondokm
Added AssignmentEnumerator
1371bb6
@mondokm
Added LazyCursor and improved ExpressionNode
db2ec33
@mondokm
separated interpretation of symbolic node, added expression mdd trave…
ddb6090 
…rser
@mondokm
Added incomplete interpretation cursor
cb4cf9d
@mondokm
Progress on expr node traverser
78321fe
@mondokm
Added example code
269dbb3
@mondokm
Generified symbolic nodes
60832a5
@mondokm
Added symbolic node visualization
069bb51
@mondokm
Added terminal1
7dbaf1c
@mondokm
Minor changes
11f06b8
@mondokm
Minor changes
8aa3c93
@mondokm
Improved incomplete interpretation cursor
f7caa73
@mondokm
Added lattice definition, improved caching
ee3a716
@mondokm
Refactoring
f9d1083
@mondokm
Refactoring
bfdf159
@mondokm
Added valuation collector
8e8f10e
@mondokm
Bugfixes and new example
fb3038d
@mondokm
Added basic constrained traversal
fbb771c
@mondokm
Minor changes
9898b1b
@mondokm
Minor changes
cb7ccdd
mondokm and others added 24 commits March 12, 2024 16:34
@mondokm
Set max-workers to 1
b4953cd
@mondokm
Include mddVariable in equality check
625180b
@mondokm
Formatting
a4e8716
@mondokm
Fix path
e323c58
@mondokm
Merge branch 'master' into zeta-merge
f7ffc12 
# Conflicts:
#	.github/actions/cache-build/action.yml
#	buildSrc/gradle.properties
@mondokm
Update guava version in delta jar to match sosylab-common
4fddf1a
@mondokm
disable bhmr
9409af1
@mondokm
Added prints
8fe2bc0
@mondokm
Added close
f7de45a
@mondokm
Print errors
6a2a219
@mondokm
Print
9d73ae5
@mondokm
Close all solvers
0f19710
@mondokm
Disable bhmr
fb78b21
@thetabotmaintainer
Reformatted code
5633c5e
@mondokm
Close all solvers
c9f235b
@mondokm
Merge remote-tracking branch 'origin/zeta-merge' into zeta-merge
fd898d0
@mondokm
Reduced bhmr state space
bb0e606
@mondokm
close solverpool
67f0f76
@mondokm
Merge master into zeta-merge, fix conflicts
03f0114
@thetabotmaintainer
Reformatted code
ed8c82a
@mondokm
Adjust to new checker interface in MultiConfig
c6c30b3
@mondokm
Add methods for MemoryAssignStmt
a16784b
@mondokm
Adjust to new checker interface
e477d98
@mondokm
Remove logback dependency
439cc63
@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 5, 2024

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

✅ ConcurrencySafety-Main (3 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:59:13 UTC
tool:                    Theta 6.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-az1146-212
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2817.241 MHz
ram:                     16757.342208000002 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                      10.07        4.91        None
pthread-atomic/read_write_lock-1.yml          true                            11.19        4.15        None
pthread-wmm/rfi003_tso.yml                    TIMEOUT                        120.65       89.06        None
pthread/lazy01.yml                            false(unreach-call)              8.63        3.46        None
pthread-wmm/mix000.oepc.yml                   false(unreach-call)             19.69        7.39        None
-----------------------------------------------------------------------------------------------------------
Run set 1                                     done                            49.68      109.71           -


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)
✅ ConcurrencySafety-MemSafety (4 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:59:02 UTC
tool:                    Theta 6.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-az1205-349
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.613 MHz
ram:                     16757.338112 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                      10.78        5.10        None
pthread-atomic/read_write_lock-1.yml          true                             9.02        3.59        None
pthread-wmm/rfi003_tso.yml                    true                            13.78        5.67        None
pthread/lazy01.yml                            true                             7.83        3.29        None
pthread-wmm/mix000.oepc.yml                   true                            13.44        5.61        None
-----------------------------------------------------------------------------------------------------------
Run set 4                                     done                            54.82       23.78           -

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)
✅ ConcurrencySafety-NoOverflows (4 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:59:05 UTC
tool:                    Theta 6.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-az2021-263
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3149.981 MHz
ram:                     16757.338112 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                      11.61        5.31        None
pthread-atomic/read_write_lock-1.yml          true                             9.17        3.64        None
pthread-wmm/rfi003_tso.yml                    true                            16.43        6.49        None
pthread/lazy01.yml                            true                             7.86        3.29        None
pthread-wmm/mix000.oepc.yml                   true                            15.62        6.35        None
-----------------------------------------------------------------------------------------------------------
Run set 3                                     done                            60.66       25.61           -


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)
✅ NoDataRace-Main (4 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:59:12 UTC
tool:                    Theta 6.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-127
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3211.604 MHz
ram:                     16757.342208000002 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                      10.97        5.14        None
pthread-atomic/read_write_lock-1.yml          true                            11.11        4.12        None
pthread-wmm/rfi003_tso.yml                    true                            17.32        6.74        None
pthread/lazy01.yml                            true                             7.83        3.31        None
pthread-wmm/mix000.oepc.yml                   true                            16.31        6.34        None
-----------------------------------------------------------------------------------------------------------
Run set 2                                     done                            63.51       26.17           -


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)
✅ ReachSafety-Arrays (1 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:57:27 UTC
tool:                    Theta 6.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-az1986-351
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3240.626 MHz
ram:                     16757.342208000002 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    TIMEOUT                         75.82      161.00        None
array-crafted/mapavg4.yml                         TIMEOUT                         76.93      161.02        None
array-programs/copysome2-1.yml                    TIMEOUT                         77.74      161.02        None
array-examples/sanfoundry_24-1.yml                true                            11.51      102.91        None
array-multidimensional/max-2-u.yml                ERROR (frontend failed)          1.84        0.76        None
---------------------------------------------------------------------------------------------------------------
Run set 1                                         done                            13.69      587.94           -


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)
✅ ReachSafety-BitVectors (3 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:56:28 UTC
tool:                    Theta 6.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-az973-881
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3232.734 MHz
ram:                     16757.342208000002 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                             7.03        3.00        None
bitvector/soft_float_1-3a.c.cil.yml            false(unreach-call)             32.71       17.24        None
bitvector-regression/integerpromotion-3.yml    false(unreach-call)              5.41        2.97        None
bitvector/sum02-1.yml                          Parsing OK                      37.36       18.77        None
bitvector-loops/diamond_2-1.yml                TIMEOUT                        121.68       84.06        None
------------------------------------------------------------------------------------------------------------
Run set 1                                      done                            77.06      126.66           -


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: 6)
❓ ReachSafety-Combinations (0 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:58:06 UTC
tool:                    Theta 6.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-az1532-138
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3241.477 MHz
ram:                     16757.342208000002 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                   TIMEOUT                        120.40       74.32        None
Problem05_label47+token_ring.02.cil-1.yml                TIMEOUT                        120.26       98.48        None
pc_sfifo_3.cil+token_ring.11.cil-1.yml                   TIMEOUT                        121.44      108.53        None
Problem05_label45+token_ring.01.cil-2.yml                TIMEOUT                        120.42       93.91        None
pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml    TIMEOUT                        122.10       69.47        None
----------------------------------------------------------------------------------------------------------------------
Run set 1                                                done                             0.59      445.84           -


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)
✅ ReachSafety-ControlFlow (1 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:56:34 UTC
tool:                    Theta 6.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-az736-73
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3102.892 MHz
ram:                     16757.342208000002 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    ERROR (frontend failed)          3.94        1.38        None
locks/test_locks_11.yml                                TIMEOUT                        120.52      102.53        None
locks/test_locks_5.yml                                 true                            13.82        5.32        None
longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml    ERROR (frontend failed)          4.43        1.60        None
longjmp/68-longjmp_11-counting-return_true.yml         ERROR (frontend failed)          2.06        0.84        None
--------------------------------------------------------------------------------------------------------------------
Run set 1                                              done                            23.73      112.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:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 8)
❓ ReachSafety-ECA (0 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:59:50 UTC
tool:                    Theta 6.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-az1242-951
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3180.277 MHz
ram:                     16757.342208000002 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                        120.78       80.42        None
eca-rers2012/Problem06_label11.yml     TIMEOUT                        120.37       75.36        None
eca-programs/Problem101_label07.yml    TIMEOUT                        121.28       72.79        None
eca-rers2012/Problem05_label44.yml     TIMEOUT                        121.21       73.49        None
eca-rers2012/Problem04_label05.yml     TIMEOUT                        120.94       75.02        None
----------------------------------------------------------------------------------------------------
Run set 1                              done                             0.60      380.11           -


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)
✅ ReachSafety-Floats (4 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:59:17 UTC
tool:                    Theta 6.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-az1445-91
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3223.613 MHz
ram:                     16757.342208000002 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                             5.71        2.66        None
float-benchs/zonotope_loose.c.v+cfa-reducer.yml    TIMEOUT                        120.44      112.92        None
float-benchs/float_int_inv_square.yml              false(unreach-call)              6.29        3.08        None
floats-cdfpl/square_3.yml                          false(unreach-call)             76.82       72.90        None
floats-cbmc-regression/float11.yml                 true                             5.26        2.79        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            24.04      195.37           -


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:               4
    correct true:        2
    correct false:       2
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 6 (max: 8)
❓ ReachSafety-Hardware (0 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:59:45 UTC
tool:                    Theta 6.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-az1445-91
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.358 MHz
ram:                     16757.338112 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.63      111.92        None
btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml    TIMEOUT                        120.66       96.13        None
btor2c-lazyMod.extinction.4.prop1-func-interl.yml    TIMEOUT                        120.47       94.61        None
btor2c-lazyMod.lup.2.prop1-func-interl.yml           TIMEOUT                        120.56       96.35        None
btor2c-lazyMod.train-gate.6.prop1-func-interl.yml    TIMEOUT                        120.98       86.10        None
------------------------------------------------------------------------------------------------------------------
Run set 1                                            done                             0.61      487.73           -


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)
✅ ReachSafety-Heap (5 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:57:06 UTC
tool:                    Theta 6.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-az1208-977
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2695.445 MHz
ram:                     16757.342208000002 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                true                             9.62        4.61        None
test15.yml                true                             8.69        4.25        None
just_assert.yml           true                             5.41        2.77        None
volatile_alias.yml        true                             7.80        4.04        None
mutex_lock_int.c_1.yml    true                             8.92        4.36        None
---------------------------------------------------------------------------------------
Run set 1                 done                            40.42       20.56           -


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:               5
    correct true:        5
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               0
  Score:                10 (max: 10)
✅ ReachSafety-Loops (1 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:58:45 UTC
tool:                    Theta 6.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-az1208-977
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.572 MHz
ram:                     16757.342208000002 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                            TIMEOUT                        120.52      107.45        None
loop-crafted/simple_vardep_2.yml                   TIMEOUT                        120.81      109.88        None
nla-digbench-scaling/divbin_valuebound100.yml      TIMEOUT                        120.65      107.88        None
nla-digbench-scaling/mannadiv_valuebound50.yml     true                            22.36       10.00        None
nla-digbench-scaling/mannadiv_unwindbound10.yml    Parsing OK                      28.10       12.15        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            50.70      348.60           -


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: 9)
✅ ReachSafety-Recursive (1 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:56:45 UTC
tool:                    Theta 6.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-az1242-951
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3178.566 MHz
ram:                     16757.342208000002 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                        Parsing OK                      16.28        6.62        None
recursive-simple/id2_i5_o5-2.yml                    true                            12.61        4.67        None
recursified_nla-digbench/recursified_geo2-ll.yml    TIMEOUT                         32.78      161.02        None
recursive/recHanoi03-2.yml                          TIMEOUT                        120.52       92.53        None
recursified_nla-digbench/recursified_lcm2.yml       TIMEOUT                        120.34      114.49        None
-----------------------------------------------------------------------------------------------------------------
Run set 1                                           done                            29.22      380.70           -


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: 9)
✅ ReachSafety-Sequentialized (1 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:57:56 UTC
tool:                    Theta 6.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-az979-911
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2659.709 MHz
ram:                     16757.342208000002 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                        121.07      109.53        None
seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml        TIMEOUT                        120.38       94.11        None
systemc/pipeline.cil-1.yml                                        TIMEOUT                        120.56      103.94        None
seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml    TIMEOUT                        120.54       93.79        None
seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml            false(unreach-call)            104.70       67.53        None
-------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                         done                           103.37      469.94           -


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: 6)
❓ ReachSafety-XCSP (0 / 0 / 5)

table-generator output: HTML/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:                    Fri, 2024-07-05 08:56:31 UTC
tool:                    Theta 6.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-az1498-10
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3192.69 MHz
ram:                     16757.342208000002 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                        120.98      107.74        None
Dubois-025.yml             TIMEOUT                        120.11      107.51        None
aim-100-2-0-unsat-4.yml    TIMEOUT                        120.13      107.31        None
AllInterval-014.yml        TIMEOUT                        121.02      105.99        None
AllInterval-005.yml        TIMEOUT                        120.24      105.82        None
----------------------------------------------------------------------------------------
Run set 1                  done                             0.61      535.39           -


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)

@mondokm mondokm closed this Jul 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@mondokm @marci543