Merge branch 'master' into unrolltype

Author: sim642

dune-project

@@ -1,4 +1,4 @@
-(lang dune 3.7)
+(lang dune 3.13)
 (using dune_site 0.1)
 (cram enable)
 (name goblint)

goblint.opam

@@ -35,7 +35,7 @@ homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
-  "dune" {>= "3.7"}
+  "dune" {>= "3.13"}
   "ocaml" {>= "4.14"}
   "goblint-cil" {>= "2.0.5"}
   "batteries" {>= "3.5.1"}

scripts/creduce/branches.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+set -e
+
+gcc -c -Werror=implicit-function-declaration ./bad.c
+
+GOBLINTDIR="/home/simmo/dev/goblint/sv-comp/goblint"
+OPTS="--conf $GOBLINTDIR/conf/svcomp.json --set ana.specification $GOBLINTDIR/../sv-benchmarks/c/properties/unreach-call.prp bad.c --enable pre.enabled"
+LOG="goblint.log"
+
+$GOBLINTDIR/goblint $OPTS -v &> $LOG
+
+grep -F "Both branches dead" $LOG

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -4,11 +4,30 @@
 
 open Analyses
 
+open SparseVector
+open ListMatrix
+
+open ArrayVector
+open ArrayMatrix
+
 include RelationAnalysis
 
+(* There are two versions of the affeq domain.
+   1. Sparse without side effects
+   2. Dense Array with side effects
+   Default: sparse implementation
+   The array implementation with side effects of the affeq domain is used when the --disable ana.affeq.sparse option is set *)
+let get_domain: (module RelationDomain.RD) Lazy.t =
+  lazy (
+    if GobConfig.get_bool "ana.affeq.sparse" then
+      (module AffineEqualityDomain.D2 (SparseVector) (ListMatrix))
+    else
+      (module AffineEqualityDenseDomain.D2 (ArrayVector) (ArrayMatrix))
+  )
+
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
-    let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
+    let module AD = (val Lazy.force get_domain) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct

src/analyses/apron/relationAnalysis.apron.ml

@@ -465,17 +465,15 @@ struct
 
   (* Give the set of reachables from argument. *)
   let reachables (ask: Queries.ask) es =
-    let reachable e st =
-      match st with
-      | None -> None
-      | Some st ->
+    let reachable acc e =
+      Option.bind acc (fun st ->
         let ad = ask.f (Queries.ReachableFrom e) in
         if Queries.AD.is_top ad then
           None
         else
-          Some (Queries.AD.join ad st)
+          Some (Queries.AD.join ad st))
     in
-    List.fold_right reachable es (Some (Queries.AD.empty ()))
+    List.fold_left reachable (Some (Queries.AD.empty ())) es
 
 
   let forget_reachable man st es =
@@ -484,9 +482,8 @@ struct
       match reachables ask es with
       | None ->
         (* top reachable, so try to invalidate everything *)
-        RD.vars st.rel
-        |> List.filter_map RV.to_cil_varinfo
-        |> List.map Cil.var
+        let to_cil_lval x = Option.map Cil.var @@ RV.to_cil_varinfo x in
+        RD.vars st.rel |> List.filter_map to_cil_lval
       | Some ad ->
         let to_cil addr rs =
           match addr with
@@ -521,14 +518,10 @@ struct
     match desc.special args, f.vname with
     | Assert { exp; refine; _ }, _ -> assert_fn man exp refine
     | ThreadJoin { thread = id; ret_var = retvar }, _ ->
-      (
-        (* Forget value that thread return is assigned to *)
-        let st' = forget_reachable man st [retvar] in
-        let st' = Priv.thread_join ask man.global id st' in
-        match r with
-        | Some lv -> invalidate_one ask man st' lv
-        | None -> st'
-      )
+      (* Forget value that thread return is assigned to *)
+      let st' = forget_reachable man st [retvar] in
+      let st' = Priv.thread_join ask man.global id st' in
+      Option.map_default (invalidate_one ask man st') st' r
     | ThreadExit _, _ ->
       begin match ThreadId.get_current ask with
         | `Lifted tid ->
@@ -543,11 +536,10 @@ struct
       let id = List.hd args in
       Priv.thread_join ~force:true ask man.global id st
     | Rand, _ ->
-      (match r with
-       | Some lv ->
+      Option.map_default (fun lv ->
          let st = invalidate_one ask man st lv in
          assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
-       | None -> st)
+        ) st r
     | _, _ ->
       let lvallist e =
         match ask.f (Queries.MayPointTo e) with
@@ -575,10 +567,7 @@ struct
       let shallow_lvals = List.concat_map lvallist shallow_addrs in
       let st' = List.fold_left (invalidate_one ask man) st' shallow_lvals in
       (* invalidate lval if present *)
-      match r with
-      | Some lv -> invalidate_one ask man st' lv
-      | None -> st'
-
+      Option.map_default (invalidate_one ask man st') st' r
 
   let query_invariant man context =
     let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in

src/analyses/base.ml

@@ -518,7 +518,7 @@ struct
   (* From a list of values, presumably arguments to a function, simply extract
    * the pointer arguments. *)
   let get_ptrs (vals: value list): address list =
-    let f (x:value) acc = match x with
+    let f acc (x:value) = match x with
       | Address adrs when AD.is_top adrs ->
         M.info ~category:Unsound "Unknown address given as function argument"; acc
       | Address adrs when AD.to_var_may adrs = [] -> acc
@@ -528,7 +528,7 @@ struct
       | Top -> M.info ~category:Unsound "Unknown value type given as function argument"; acc
       | _ -> acc
     in
-    List.fold_right f vals []
+    List.fold_left f [] vals
 
   let rec reachable_from_value ask (value: value) (t: typ) (description: string)  =
     let empty = AD.empty () in
@@ -572,7 +572,7 @@ struct
     if M.tracing then M.traceli "reachability" "Checking reachable arguments from [%a]!" (d_list ", " AD.pretty) args;
     let empty = AD.empty () in
     (* We begin looking at the parameters: *)
-    let argset = List.fold_right (AD.join) args empty in
+    let argset = List.fold_left (AD.join) empty args in
     let workset = ref argset in
     (* And we keep a set of already visited variables *)
     let visited = ref empty in

src/analyses/baseInvariant.ml

@@ -85,6 +85,17 @@ struct
 
   let refine_lv man st c x c' pretty exp =
     let set' lval v st = set st (eval_lv ~man st lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~man in
+    let default () =
+      (* For accesses via pointers in complicated case, no refinement yet *)
+      let old_val = eval_rv_lval_refine ~man st exp x in
+      let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
+      let v = apply_invariant ~old_val ~new_val:c' in
+      if is_some_bot v then contra st
+      else (
+        if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
+        set' x v st
+      )
+    in
     match x with
     | Var var, o when refine_entire_var ->
       (* For variables, this is done at to the level of entire variables to benefit e.g. from disjunctive struct domains *)
@@ -100,17 +111,40 @@ struct
         if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r;
         r
       )
+    | Mem (Lval lv), off ->
+      (* Underlying lvals (may have offsets themselves), e.g., for struct members NOT including any offset appended to outer Mem *)
+      let lvals = eval_lv ~man st (Mem (Lval lv), NoOffset) in
+      (* Additional offset of value being refined in Addr Offset type *)
+      let original_offset = convert_offset ~man st off in
+      let res = AD.fold (fun base_a acc ->
+          Option.bind acc (fun acc ->
+              match base_a with
+              | Addr _ ->
+                let (lval_a:VD.t) = Address (AD.singleton base_a) in
+                if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty lval_a;
+                let st = set' lv lval_a st in
+                let orig = AD.Addr.add_offset base_a original_offset in
+                let old_val = get ~man st (AD.singleton orig) None in
+                let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *)
+                (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *)
+                (* let old_val = eval_rv_lval_refine ~man st exp x in *)
+                let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
+                let v = apply_invariant ~old_val ~new_val:c' in
+                if is_some_bot v then
+                  Some (D.join acc (try contra st with Analyses.Deadcode -> D.bot ()))
+                else (
+                  if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
+                  Some (D.join acc (set' x v st))
+                )
+              | _ -> None
+            )
+        ) lvals (Some (D.bot ()))
+      in
+      BatOption.map_default_delayed (fun d -> if D.is_bot d then raise Analyses.Deadcode else d) default res
     | Var _, _
     | Mem _, _ ->
-      (* For accesses via pointers, not yet *)
-      let old_val = eval_rv_lval_refine ~man st exp x in
-      let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
-      let v = apply_invariant ~old_val ~new_val:c' in
-      if is_some_bot v then contra st
-      else (
-        if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
-        set' x v st
-      )
+      default ()
+
 
   let invariant_fallback man st exp tv =
     (* We use a recursive helper function so that x != 0 is false can be handled

src/analyses/malloc_null.ml

@@ -94,7 +94,7 @@ struct
   (* Remove null values from state that are unreachable from exp.*)
   let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t =
     let reachable =
-      let do_exp e a =
+      let do_exp a e =
         match ask.f (Queries.ReachableFrom e) with
         | ad when not (Queries.AD.is_top ad) ->
           ad
@@ -103,9 +103,9 @@ struct
               | _ -> false)
           |> Queries.AD.join a
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
-        | _ -> AD.empty ()
+        | _ -> a
       in
-      List.fold_right do_exp args (AD.empty ())
+      List.fold_left do_exp (AD.empty ()) args
     in
     let vars =
       reachable
@@ -164,7 +164,7 @@ struct
   let return_addr () = !return_addr_
 
   let return man (exp:exp option) (f:fundec) : D.t =
-    let remove_var x v = List.fold_right D.remove (to_addrs v) x in
+    let remove_var x v = List.fold_left (Fun.flip D.remove) x (to_addrs v) in
     let nst = List.fold_left remove_var man.local (f.slocals @ f.sformals) in
     match exp with
     | Some ret ->

src/analyses/region.ml

@@ -55,7 +55,7 @@ struct
     | Queries.Regions e ->
       let regpart = man.global () in
       if is_bullet e regpart man.local then Queries.Result.bot q (* TODO: remove bot *) else
-        let ls = List.fold_right Queries.LS.add (regions e regpart man.local) (Queries.LS.empty ()) in
+        let ls = List.fold_left (Fun.flip Queries.LS.add) (Queries.LS.empty ()) (regions e regpart man.local) in
         ls
     | _ -> Queries.Result.top q
 

src/analyses/symbLocks.ml

@@ -43,7 +43,8 @@ struct
   let assign man lval rval = invalidate_lval (Analyses.ask_of_man man) lval man.local
 
   let return man exp fundec =
-    List.fold_right D.remove_var (fundec.sformals@fundec.slocals) man.local
+    let rm list acc = List.fold_left (Fun.flip D.remove_var) acc list in
+    rm fundec.slocals (rm fundec.sformals man.local)
 
   let enter man lval f args = [(man.local,man.local)]
   let combine_env man lval fexp f args fc au f_ask = au