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

Adding JavaSMT support #258

Merged
merged 45 commits into from
Mar 25, 2024
Merged

Adding JavaSMT support #258

merged 45 commits into from
Mar 25, 2024

Conversation

leventeBajczi
Copy link
Contributor

@leventeBajczi leventeBajczi commented Mar 18, 2024 •
edited
Loading

This PR adds support for the JavaSMT framework, thus enabling a long list of solvers to be natively used by Theta.

Furthermore, there are some patches to the CI checks as to not fail due to memory limits, and cvc5 libraries are also included in the lib folder from now on. Unfortunately, no cvc5 support is present in JavaSMT for Windows/Mac for now.

There were also of course some bugs I uncovered, especially regarding floating point operations. I tried my best in fixing them.

I also created further testFixtures for expressions, and I include them in non-JavaSMT unit tests as well.

@leventeBajczi leventeBajczi added the Ready to test This will run the final sonar check in PRs. label Mar 19, 2024
@leventeBajczi leventeBajczi marked this pull request as ready for review March 19, 2024 19:31
@leventeBajczi leventeBajczi mentioned this pull request Mar 19, 2024
Open
leventeBajczi
leventeBajczi commented Mar 19, 2024
View reviewed changes
subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java Outdated Show resolved Hide resolved
...jects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java Outdated Show resolved Hide resolved
...olver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java Show resolved Hide resolved
...ver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java Outdated Show resolved Hide resolved
...ver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java Outdated Show resolved Hide resolved
...ver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java Outdated Show resolved Hide resolved
...ver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java Outdated Show resolved Hide resolved
...olver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ExprTransformer.java Show resolved Hide resolved
subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java Show resolved Hide resolved
subprojects/solver/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3UserPropagatorTest.java Outdated Show resolved Hide resolved
leventeBajczi and others added 25 commits March 21, 2024 18:48
@leventeBajczi
Added javasmt-solver as new subproject
a28479d
@leventeBajczi
Added CVC5 libraries, fixed some bugs
ac9b50e
@leventeBajczi
Fixed interpolation, and tests
d93deef
@leventeBajczi
Fixed JavaSMTTransformerTest
1c6abba
@leventeBajczi
Implemented some missing exprs
bb0fa05
@leventeBajczi
Added lots more tests, aiming for 100% coverage
718673b
@leventeBajczi
Updated tests and implementation
a9784bf
@thetabotmaintainer @leventeBajczi
Reformatted code
922dbd0
@leventeBajczi
version bump
da0ad6e
@leventeBajczi
Fixed errors
c575e51
@leventeBajczi
Limited max memory for tests on the jvm
e1757ad
@leventeBajczi
Added --max-workers 2 --no-daemon to CI
cfc6c0f
@leventeBajczi
Added flags to sonar as well
26d2cb1
@leventeBajczi
Further minimizing memory footprint in CI
c061f5b
@leventeBajczi
Fixed flag
7f1d023
@leventeBajczi
Disabled PRINCESS tests
529b9a6
@leventeBajczi
Reverted some gradle flags
d536768
@leventeBajczi
Added solver managers in xcfa-cli
5a89953
@leventeBajczi
Allocating 1G for tests instead of 5
22cb4b1
@leventeBajczi
Added try-with-resources and removed logging
48a222d
@leventeBajczi
Handling exceptions for solvers
1b11dc7
@leventeBajczi
Added README on limitations
540b8d9
@leventeBajczi
Apply suggestions from code review
3b4a47f
@leventeBajczi
removed userprop test
40a4246
@leventeBajczi
fix
938d095
@leventeBajczi
Copy link
Contributor Author

I addressed all TODOs I left for myself, so I consider this PR ready. @as3810t, when you have the time, please take a look!

@sonarcloud SonarCloud
Copy link

sonarcloud bot commented Mar 24, 2024

Quality Gate Passed Quality Gate passed

Issues
278 New issues
0 Accepted issues

Measures
0 Security Hotspots
79.6% Coverage on New Code
3.8% Duplication on New Code

See analysis details on SonarCloud

as3810t
as3810t previously approved these changes Mar 25, 2024
View reviewed changes
Copy link
Contributor

@as3810t as3810t left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ithink it is a great addition to the existing solvers.

Questions:

  • Right now, CVC5 and JavaSMT dependencies are included directly as a jar into the project. Can we use Gradle's dependency management instead?

Suggestions:

  • It would be great to add description on how to use the new solvers. I get that the names start with JavaSMT:..., but it would be useful to document the different strings in the README that can follow the colon.

@csanadtelbisz csanadtelbisz mentioned this pull request Mar 25, 2024
Open
@leventeBajczi leventeBajczi merged commit fd60827 into master Mar 25, 2024
15 of 33 checks passed
@leventeBajczi leventeBajczi deleted the javasmt branch March 25, 2024 15:15
@github-actions GitHub Actions
Copy link

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:                    Mon, 2024-03-25 15:30:05 UTC
tool:                    Theta 5.1.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-325
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2992.367 MHz
ram:                     16757.3504 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                       5.90        2.69        None
pthread-atomic/read_write_lock-1.yml          true                            12.01        4.42        None
pthread-wmm/rfi003_tso.yml                    TIMEOUT (Parsing OK)           120.61       90.68        None
pthread/lazy01.yml                            false(unreach-call)              8.57        3.49        None
pthread-wmm/mix000.oepc.yml                   false(unreach-call)             13.72        4.90        None
-----------------------------------------------------------------------------------------------------------
Run set 1                                     done                            40.31      106.82           -


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:                    Mon, 2024-03-25 15:29:57 UTC
tool:                    Theta 5.1.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-az732-608
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3218.33 MHz
ram:                     16757.3504 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                       5.95        2.66        None
pthread-atomic/read_write_lock-1.yml          true                             9.41        3.71        None
pthread-wmm/rfi003_tso.yml                    true                            10.62        4.11        None
pthread/lazy01.yml                            true                             7.44        3.19        None
pthread-wmm/mix000.oepc.yml                   true                            10.32        3.94        None
-----------------------------------------------------------------------------------------------------------
Run set 4                                     done                            43.72       18.15           -

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:                    Mon, 2024-03-25 15:30:14 UTC
tool:                    Theta 5.1.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-az849-642
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.412 MHz
ram:                     16757.3504 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.00        2.76        None
pthread-atomic/read_write_lock-1.yml          true                            10.44        3.97        None
pthread-wmm/rfi003_tso.yml                    true                            11.43        4.38        None
pthread/lazy01.yml                            true                             8.57        3.53        None
pthread-wmm/mix000.oepc.yml                   true                            10.91        4.14        None
-----------------------------------------------------------------------------------------------------------
Run set 3                                     done                            47.32       19.31           -


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:                    Mon, 2024-03-25 15:30:04 UTC
tool:                    Theta 5.1.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-az1542-632
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3130.068 MHz
ram:                     16757.346304 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                       5.96        2.67        None
pthread-atomic/read_write_lock-1.yml          true                            12.41        4.54        None
pthread-wmm/rfi003_tso.yml                    true                            13.89        5.08        None
pthread/lazy01.yml                            true                             7.84        3.27        None
pthread-wmm/mix000.oepc.yml                   true                            13.99        5.04        None
-----------------------------------------------------------------------------------------------------------
Run set 2                                     done                            54.07       21.11           -


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 (0 / 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:                    Mon, 2024-03-25 15:29:52 UTC
tool:                    Theta 5.1.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-az1247-846
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.736 MHz
ram:                     16757.3504 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                     113.42      101.36        None
array-crafted/mapavg4.yml                         Parsing OK                     114.39      101.34        None
array-programs/copysome2-1.yml                    Parsing OK                     113.01      101.17        None
array-examples/sanfoundry_24-1.yml                Parsing OK                       9.33        4.07        None
array-multidimensional/max-2-u.yml                Parsing OK                     119.06      101.18        None
---------------------------------------------------------------------------------------------------------------
Run set 1                                         done                            22.49      409.65           -


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)
✅ ReachSafety-BitVectors (2 / 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:                    Mon, 2024-03-25 15:27:25 UTC
tool:                    Theta 5.1.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-33
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2893.955 MHz
ram:                     16757.3504 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                             8.79        3.53        None
bitvector/soft_float_1-3a.c.cil.yml            Parsing OK                      12.82        4.80        None
bitvector-regression/integerpromotion-3.yml    false(unreach-call)              6.46        3.10        None
bitvector/sum02-1.yml                          Parsing OK                       7.32        3.15        None
bitvector-loops/diamond_2-1.yml                Parsing OK                       8.58        3.47        None
------------------------------------------------------------------------------------------------------------
Run set 1                                      done                            43.86       18.57           -


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)
❓ 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:                    Mon, 2024-03-25 15:29:08 UTC
tool:                    Theta 5.1.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-33
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3244.917 MHz
ram:                     16757.3504 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.54       26.21        None
Problem05_label47+token_ring.02.cil-1.yml                TIMEOUT (Parsing OK)           122.14       79.80        None
pc_sfifo_3.cil+token_ring.11.cil-1.yml                   TIMEOUT (Parsing OK)           120.86       91.85        None
Problem05_label45+token_ring.01.cil-2.yml                TIMEOUT (Parsing OK)           121.21       75.27        None
pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml    Parsing OK                      67.97       33.69        None
----------------------------------------------------------------------------------------------------------------------
Run set 1                                                done                           110.32      308.85           -


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:                    Mon, 2024-03-25 15:27:32 UTC
tool:                    Theta 5.1.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-az1538-251
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.134 MHz
ram:                     16757.3504 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.07        3.47        None
locks/test_locks_11.yml                                Parsing OK                     117.48      101.31        None
locks/test_locks_5.yml                                 true                            13.54        4.94        None
longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml    Parsing OK                       7.99        3.49        None
longjmp/68-longjmp_11-counting-return_true.yml         Parsing OK                       6.37        2.96        None
--------------------------------------------------------------------------------------------------------------------
Run set 1                                              done                            39.50      116.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: 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:                    Mon, 2024-03-25 15:30:44 UTC
tool:                    Theta 5.1.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-33
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3101.944 MHz
ram:                     16757.3504 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)           121.23       81.75        None
eca-rers2012/Problem06_label11.yml     TIMEOUT (Parsing OK)           120.65       75.49        None
eca-programs/Problem101_label07.yml    TIMEOUT                        120.33       67.72        None
eca-rers2012/Problem05_label44.yml     TIMEOUT (Parsing OK)           120.62       71.68        None
eca-rers2012/Problem04_label05.yml     TIMEOUT (Parsing OK)           120.65       76.82        None
----------------------------------------------------------------------------------------------------
Run set 1                              done                             0.60      376.38           -


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 (3 / 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:                    Mon, 2024-03-25 15:30:10 UTC
tool:                    Theta 5.1.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-551
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2608.06 MHz
ram:                     16757.3504 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.00        2.87        None
float-benchs/zonotope_loose.c.v+cfa-reducer.yml    Parsing OK                       8.65        4.20        None
float-benchs/float_int_inv_square.yml              false(unreach-call)             10.37        5.99        None
floats-cdfpl/square_3.yml                          TIMEOUT (false(unreach-call))      120.36      115.50        None
floats-cbmc-regression/float11.yml                 true                             5.84        3.02        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            29.50      132.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:               3
    correct true:        2
    correct false:       1
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                 5 (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:                    Mon, 2024-03-25 15:30:37 UTC
tool:                    Theta 5.1.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-az568-540
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.859 MHz
ram:                     16757.342208000002 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.32      115.58        None
btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml    TIMEOUT (Parsing OK)           120.38       98.07        None
btor2c-lazyMod.extinction.4.prop1-func-interl.yml    TIMEOUT (Parsing OK)           120.40       94.85        None
btor2c-lazyMod.lup.2.prop1-func-interl.yml           Parsing OK                     117.14       93.70        None
btor2c-lazyMod.train-gate.6.prop1-func-interl.yml    Parsing OK                      85.01       62.29        None
------------------------------------------------------------------------------------------------------------------
Run set 1                                            done                           174.17      466.13           -


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 (1 / 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:                    Mon, 2024-03-25 15:28:46 UTC
tool:                    Theta 5.1.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-az1426-296
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.851 MHz
ram:                     16757.3504 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                       5.05        2.34        None
test15.yml                Parsing OK                       4.99        2.32        None
just_assert.yml           true                             5.67        2.77        None
volatile_alias.yml        Parsing OK                       3.93        2.12        None
mutex_lock_int.c_1.yml    Parsing OK                       5.11        2.39        None
---------------------------------------------------------------------------------------
Run set 1                 done                            24.74       12.47           -


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-Loops (0 / 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:                    Mon, 2024-03-25 15:29:39 UTC
tool:                    Theta 5.1.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-az1040-315
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3233.079 MHz
ram:                     16757.3504 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.90      101.20        None
loop-crafted/simple_vardep_2.yml                   Parsing OK                     107.58      101.22        None
nla-digbench-scaling/divbin_valuebound100.yml      Parsing OK                      83.18       77.54        None
nla-digbench-scaling/mannadiv_valuebound50.yml     Parsing OK                       6.61        2.90        None
nla-digbench-scaling/mannadiv_unwindbound10.yml    Parsing OK                       7.32        3.14        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                           103.28      286.54           -


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-Recursive (0 / 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:                    Mon, 2024-03-25 15:27:44 UTC
tool:                    Theta 5.1.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-az525-520
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2613.19 MHz
ram:                     16757.3504 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.12      100.81        None
recursive-simple/id2_i5_o5-2.yml                    TIMEOUT (Parsing OK)           120.29      100.82        None
recursified_nla-digbench/recursified_geo2-ll.yml    ERROR (frontend failed)          1.65        0.73        None
recursive/recHanoi03-2.yml                          TIMEOUT (Parsing OK)           120.38       99.30        None
recursified_nla-digbench/recursified_lcm2.yml       ERROR (frontend failed)          1.63        0.74        None
-----------------------------------------------------------------------------------------------------------------
Run set 1                                           done                             3.64      304.13           -


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-Sequentialized (0 / 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:                    Mon, 2024-03-25 15:30:09 UTC
tool:                    Theta 5.1.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-az711-489
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3097.582 MHz
ram:                     16757.3504 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.13       96.72        None
seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml        Parsing OK                      14.62        5.40        None
systemc/pipeline.cil-1.yml                                        TIMEOUT (Parsing OK)           120.99      101.42        None
seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml    Parsing OK                      17.32        6.32        None
seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml            Parsing OK                      26.38       10.67        None
-------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                         done                            56.45      222.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: 6)
✅ ReachSafety-XCSP (1 / 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:                    Mon, 2024-03-25 15:27:29 UTC
tool:                    Theta 5.1.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-az1536-160
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3166.821 MHz
ram:                     16757.3504 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.59       97.26        None
Dubois-025.yml             Parsing OK                      22.80        9.67        None
aim-100-2-0-unsat-4.yml    Parsing OK                      33.61       16.42        None
AllInterval-014.yml        Parsing OK                     112.81      101.84        None
AllInterval-005.yml        false(unreach-call)             11.82        4.39        None
----------------------------------------------------------------------------------------
Run set 1                  done                            64.29      230.61           -


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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@as3810t as3810t as3810t left review comments

Assignees
No one assigned
Labels
Ready to test This will run the final sonar check in PRs.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@leventeBajczi @as3810t