Merge branch 'master' into svcomp26-dev

Author: sim642

.semgrep/apron.yml

@@ -0,0 +1,9 @@
+rules:
+  - id: apron-linexp0-get_size
+    pattern-either:
+      - pattern: Linexpr0.get_size
+      - pattern: Apron.Linexpr0.get_size
+      - pattern: GobApron.Linexpr0.get_size
+    message: don't use (returns some internal size, not number of dimensions)
+    languages: [ocaml]
+    severity: ERROR

.semgrep/batio.yml

@@ -0,0 +1,6 @@
+rules:
+  - id: batio-to_input_channel
+    pattern: BatIO.to_input_channel
+    message: don't use (leaks two file descriptors)
+    languages: [ocaml]
+    severity: ERROR

conf/svcomp26/level02.json

@@ -62,7 +62,6 @@
         "noRecursiveIntervals",
         "enums",
         "congruence",
-        "octagon",
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",

conf/svcomp26/level03.json

@@ -33,7 +33,8 @@
       "mutexGhosts",
       "pthreadMutexType",
       "affeq",
-      "apron"
+      "apron",
+      "branchSet"
     ],
     "apron": {
       "domain": "octagon"
@@ -45,7 +46,8 @@
       "expsplit",
       "activeSetjmp",
       "memLeak",
-      "threadflag"
+      "threadflag",
+      "branchSet"
     ],
     "base": {
       "arrays": {

conf/svcomp26/seq-validate.txt

@@ -5,9 +5,9 @@
 --conf conf/svcomp26/common.json --conf conf/svcomp26/validate.json --conf conf/svcomp26/level00.json --set ana.activated[+] unassume
 # standard run based on svcomp 25 settings, but with context gas
 --conf conf/svcomp26/common.json --conf conf/svcomp26/validate.json --conf conf/svcomp26/level01.json --set ana.activated[+] unassume
-# apron/affeq run with enums,congruence, bitfield and sets for structs, sporting (side_)widen_gas 30
---conf conf/svcomp26/common.json --conf conf/svcomp26/validate.json --conf conf/svcomp26/level02.json --set ana.activated[+] unassume
 # apron/affeq run with enums,congruence, bitfield and sets for structs, sporting (side_)widen_gas 30, no autotuner for apron
+--conf conf/svcomp26/common.json --conf conf/svcomp26/validate.json --conf conf/svcomp26/level02.json --set ana.activated[+] unassume
+# apron/affeq run with enums,congruence, bitfield and sets for structs, sporting (side_)widen_gas 30, no autotuner for apron, branchset-sensitive
 --conf conf/svcomp26/common.json --conf conf/svcomp26/validate.json --conf conf/svcomp26/level03.json --set ana.activated[+] unassume
 # base-pathsensitive run
 --conf conf/svcomp26/common.json --conf conf/svcomp26/validate.json --conf conf/svcomp26/level04-validate.json --set ana.activated[+] unassume

conf/svcomp26/seq.txt

@@ -5,9 +5,9 @@
 --conf conf/svcomp26/common.json --conf conf/svcomp26/verify.json --conf conf/svcomp26/level00.json
 # standard run based on svcomp 25 settings, but with context gas
 --conf conf/svcomp26/common.json --conf conf/svcomp26/verify.json --conf conf/svcomp26/level01.json
-# apron/affeq run with enums,congruence, bitfield and sets for structs, sporting (side_)widen_gas 30
---conf conf/svcomp26/common.json --conf conf/svcomp26/verify.json --conf conf/svcomp26/level02.json
 # apron/affeq run with enums,congruence, bitfield and sets for structs, sporting (side_)widen_gas 30, no autotuner for apron
+--conf conf/svcomp26/common.json --conf conf/svcomp26/verify.json --conf conf/svcomp26/level02.json
+# apron/affeq run with enums,congruence, bitfield and sets for structs, sporting (side_)widen_gas 30, no autotuner for apron, branchset-sensitive
 --conf conf/svcomp26/common.json --conf conf/svcomp26/verify.json --conf conf/svcomp26/level03.json
 # base-pathsensitive run
 --conf conf/svcomp26/common.json --conf conf/svcomp26/verify.json --conf conf/svcomp26/level04.json

src/analyses/accessAnalysis.ml

@@ -29,7 +29,7 @@ struct
   let init _ =
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
     let activated = get_string_list "ana.activated" in
-    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
+    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *)
 
   let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;

src/analyses/apron/apronAnalysis.apron.ml

@@ -8,8 +8,6 @@ let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module Man = (val ApronDomain.get_manager ()) in
     let module AD = ApronDomain.D2 (Man) in
-    let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in
-    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct

src/analyses/apron/relationAnalysis.apron.ml

@@ -613,7 +613,7 @@ struct
         if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
           RD.cil_exp_of_lincons1 lincons1
           |> Option.map e_inv
-          |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
+          |> Option.filter (InvariantCil.exp_is_suitable ~scope)
         else
           None
       )

src/analyses/apron/relationPriv.apron.ml

@@ -733,7 +733,7 @@ struct
               (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
               if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
                 RD.cil_exp_of_lincons1 lincons1
-                |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))
+                |> Option.filter (InvariantCil.exp_is_suitable ?scope:None)
               else
                 None
             )