Skip to content

Commit

Permalink
Merge branch 'master' into rm-virtual-library
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Nov 29, 2024
2 parents a5ab08b + 68cd952 commit 6039b1d
Show file tree
Hide file tree
Showing 398 changed files with 6,542 additions and 3,075 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/coverage.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
# don't add any other because they won't be used
Expand All @@ -40,7 +40,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

- name: Install graph-easy # TODO: remove if depext --with-test works
if: ${{ matrix.os == 'ubuntu-latest' }}
if: ${{ matrix.os == 'ubuntu-22.04' }}
run: sudo apt install -y libgraph-easy-perl

- name: Install dependencies
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/docs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ jobs:
strategy:
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
# don't add any other because they won't be used
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/indentation.yml
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ jobs:
strategy:
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- 4.14.x

Expand Down
10 changes: 5 additions & 5 deletions .github/workflows/locked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
- macos-13
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
Expand All @@ -42,7 +42,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

- name: Install graph-easy # TODO: remove if depext --with-test works
if: ${{ matrix.os == 'ubuntu-latest' }}
if: ${{ matrix.os == 'ubuntu-22.04' }}
run: sudo apt install -y libgraph-easy-perl

- name: Install dependencies
Expand Down Expand Up @@ -70,7 +70,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
# don't add any other because they won't be used
Expand All @@ -91,7 +91,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

- name: Install graph-easy # TODO: remove if depext --with-test works
if: ${{ matrix.os == 'ubuntu-latest' }}
if: ${{ matrix.os == 'ubuntu-22.04' }}
run: sudo apt install -y libgraph-easy-perl

- name: Install spin
Expand All @@ -112,7 +112,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
# don't add any other because they won't be used
Expand Down
16 changes: 9 additions & 7 deletions .github/workflows/unlocked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
- macos-13
ocaml-compiler:
- 5.2.x
Expand All @@ -30,9 +30,11 @@ jobs:
- false

include:
- os: ubuntu-latest
- os: ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler: 4.14.x
z3: true
- os: macos-latest
ocaml-compiler: 4.14.x

# customize name to use readable string for apron instead of just a boolean
# workaround for missing ternary operator: https://github.com/actions/runner/issues/409
Expand All @@ -50,7 +52,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

- name: Install graph-easy # TODO: remove if depext --with-test works
if: ${{ matrix.os == 'ubuntu-latest' }}
if: ${{ matrix.os == 'ubuntu-22.04' }}
run: sudo apt install -y libgraph-easy-perl

- name: Install dependencies
Expand Down Expand Up @@ -88,7 +90,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
- macos-13
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
Expand All @@ -110,7 +112,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

- name: Install graph-easy # TODO: remove if depext --with-test works
if: ${{ matrix.os == 'ubuntu-latest' }}
if: ${{ matrix.os == 'ubuntu-22.04' }}
run: sudo apt install -y libgraph-easy-perl

- name: Install dependencies
Expand Down Expand Up @@ -185,7 +187,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
- macos-13
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
Expand All @@ -202,7 +204,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

- name: Install graph-easy # TODO: remove if depext --with-test works
if: ${{ matrix.os == 'ubuntu-latest' }}
if: ${{ matrix.os == 'ubuntu-22.04' }}
run: sudo apt install -y libgraph-easy-perl

- name: Install Goblint with test
Expand Down
26 changes: 26 additions & 0 deletions .semgrep/fold.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
rules:
- id: fold-exists
patterns:
- pattern-either:
- pattern: $D.fold ... false
- pattern: $D.fold_left ... false
- pattern: $D.fold_right ... false
- pattern: fold ... false
- pattern: fold_left ... false
- pattern: fold_right ... false
message: consider replacing fold with exists
languages: [ocaml]
severity: WARNING

- id: fold-for_all
patterns:
- pattern-either:
- pattern: $D.fold ... true
- pattern: $D.fold_left ... true
- pattern: $D.fold_right ... true
- pattern: fold ... true
- pattern: fold_left ... true
- pattern: fold_right ... true
message: consider replacing fold with for_all
languages: [ocaml]
severity: WARNING
8 changes: 8 additions & 0 deletions .semgrep/tracing.yml
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,16 @@ rules:
- pattern: Messages.tracec
- pattern: Messages.traceu
- pattern: Messages.traceli
- pattern: M.trace
- pattern: M.tracel
- pattern: M.tracei
- pattern: M.tracec
- pattern: M.traceu
- pattern: M.traceli
- pattern-not-inside: if Messages.tracing then ...
- pattern-not-inside: if Messages.tracing && ... then ...
- pattern-not-inside: if M.tracing then ...
- pattern-not-inside: if M.tracing && ... then ...
message: trace functions should only be called if tracing is enabled at compile time
languages: [ocaml]
severity: WARNING
30 changes: 30 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,33 @@
## v2.5.0
Functionally equivalent to Goblint in SV-COMP 2025.

* Add 32bit vs 64bit architecture support (#54, #1574).
* Add per-function context gas analysis (#1569, #1570, #1598).
* Adapt automatic static loop unrolling (#1516, #1582, #1583, #1584, #1590, #1595, #1599).
* Adapt automatic configuration tuning (#1450, #1612, #1181, #1604).
* Simplify non-relational integer invariants in witnesses (#1517).
* Fix excessive hash collisions (#1594, #1602).
* Clean up various code (#1095, #1523, #1554, #1575, #1588, #1597, #1614).

## v2.4.0
* Remove unmaintained analyses: spec, file (#1281).
* Add linear two-variable equalities analysis (#1297, #1412, #1466).
* Add callstring, loopfree callstring and context gas analyses (#1038, #1340, #1379, #1427, #1439).
* Add non-relational thread-modular value analyses with thread IDs (#1366, #1398, #1399).
* Add NULL byte array domain (#1076).
* Fix spurious overflow warnings from internal evaluations (#1406, #1411, #1511).
* Refactor non-definite mutex handling to fix unsoundness (#1430, #1500, #1503, #1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (#1457, #1458).
* Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510).
* Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407).
* Improve narrowing operators (#1502, #1540, #1543).
* Extract automatic configuration tuning for soundness (#1469).
* Fix many locations in witnesses (#1355, #1372, #1400, #1403).
* Improve output readability (#1294, #1312, #1405, #1497).
* Refactor logging (#1117).
* Modernize all library function specifications (#1029, #688, #1174, #1289, #1447, #1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (#1448).

## v2.3.0
Functionally equivalent to Goblint in SV-COMP 2024.

Expand Down
2 changes: 1 addition & 1 deletion bench/basic/benchSet.ml
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ let () =
]
);
"const" @> lazy (
let args = ((fun x -> 42), set1) in
let args = ((fun _ -> 42), set1) in
throughputN 1 [
("map1", map1, args);
("map2", map2, args);
Expand Down
123 changes: 123 additions & 0 deletions conf/svcomp-validate.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,123 @@
{
"ana": {
"sv-comp": {
"enabled": true,
"functions": true
},
"int": {
"def_exc": true,
"enums": false,
"interval": true
},
"float": {
"interval": true,
"evaluate_math_functions": true
},
"activated": [
"base",
"threadid",
"threadflag",
"threadreturn",
"mallocWrapper",
"mutexEvents",
"mutex",
"access",
"race",
"escape",
"expRelation",
"mhp",
"assert",
"var_eq",
"symb_locks",
"region",
"thread",
"threadJoins",
"abortUnless",
"unassume"
],
"path_sens": [
"mutex",
"malloc_null",
"uninit",
"expsplit",
"activeSetjmp",
"memLeak",
"threadflag"
],
"context": {
"widen": false
},
"base": {
"arrays": {
"domain": "partitioned"
}
},
"race": {
"free": false,
"call": false
},
"autotune": {
"enabled": true,
"activated": [
"singleThreaded",
"mallocWrappers",
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
"noOverflows",
"termination",
"tmpSpecialAnalysis"
]
},
"widen": {
"tokens": true
}
},
"exp": {
"region-offsets": true
},
"solver": "td3",
"sem": {
"unknown_function": {
"spawn": false
},
"int": {
"signed_overflow": "assume_none"
},
"null-pointer": {
"dereference": "assume_none"
}
},
"witness": {
"graphml": {
"enabled": false
},
"yaml": {
"enabled": false,
"strict": true,
"format-version": "2.0",
"entry-types": [
"location_invariant",
"loop_invariant",
"invariant_set",
"violation_sequence"
],
"invariant-types": [
"location_invariant",
"loop_invariant"
]
},
"invariant": {
"loop-head": true,
"after-lock": true,
"other": true
}
},
"pre": {
"enabled": false
}
}
Loading

0 comments on commit 6039b1d

Please sign in to comment.