Witness invariants for arrays and principled handling of unknown indices

src/analyses/base.ml

@@ -625,8 +625,7 @@ struct
       let toInt i =
         match IdxDom.to_int @@ ID.cast_to ik i with
         | Some x -> Const (CInt (x,ik, None))
-        | _ -> Cilfacade.mkCast ~e:(Const (CStr ("unknown",No_encoding))) ~newt:intType
-
+        | _ -> Lval.any_index_exp
       in
       match o with
       | `NoOffset -> `NoOffset
@@ -1059,7 +1058,7 @@ struct
     match ofs with
     | NoOffset -> `NoOffset
     | Field (fld, ofs) -> `Field (fld, convert_offset a gs st ofs)
-    | Index (CastE (TInt(IInt,[]), Const (CStr ("unknown",No_encoding))), ofs) -> (* special offset added by convertToQueryLval *)
+    | Index (exp, ofs) when CilType.Exp.equal exp Lval.any_index_exp -> (* special offset added by convertToQueryLval *)
       `Index (IdxDom.top (), convert_offset a gs st ofs)
     | Index (exp, ofs) ->
       match eval_rv a gs st exp with
@@ -1637,7 +1636,7 @@ struct
 
     let get_var = get_var
     let get a gs st addrs exp = get a gs st addrs exp
-    let set a ~ctx gs st lval lval_type value = set a ~ctx ~invariant:true gs st lval lval_type value
+    let set a ~ctx gs st lval lval_type ?lval_raw value = set a ~ctx ~invariant:true gs st lval lval_type ?lval_raw value
 
     let refine_entire_var = true
     let map_oldval oldval _ = oldval
@@ -2522,7 +2521,7 @@ struct
           (* all updates happen in ctx with top values *)
           let get_var = get_var
           let get a gs st addrs exp = get a gs st addrs exp
-          let set a ~ctx gs st lval lval_type value = set a ~ctx ~invariant:false gs st lval lval_type value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *)
+          let set a ~ctx gs st lval lval_type ?lval_raw value = set a ~ctx ~invariant:false gs st lval lval_type ?lval_raw value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *)
 
           let refine_entire_var = false
           let map_oldval oldval t_lval =

src/analyses/baseInvariant.ml

@@ -20,7 +20,7 @@ sig
 
   val get_var: Queries.ask -> (V.t -> G.t) -> D.t -> varinfo -> VD.t
   val get: Queries.ask -> (V.t -> G.t) -> D.t -> AD.t -> exp option -> VD.t
-  val set: Queries.ask -> ctx:(D.t, G.t, _, V.t) Analyses.ctx -> (V.t -> G.t) -> D.t -> AD.t -> typ -> VD.t -> D.t
+  val set: Queries.ask -> ctx:(D.t, G.t, _, V.t) Analyses.ctx -> (V.t -> G.t) -> D.t -> AD.t -> typ -> ?lval_raw:lval -> VD.t -> D.t
 
   val refine_entire_var: bool
   val map_oldval: VD.t -> typ -> VD.t
@@ -93,7 +93,7 @@ struct
       else set a gs st addr t_lval new_val ~ctx (* no *_raw because this is not a real assignment *)
 
   let refine_lv ctx a gs st c x c' pretty exp =
-    let set' lval v st = set a gs st (eval_lv a gs st lval) (Cilfacade.typeOfLval lval) v ~ctx in
+    let set' lval v st = set a gs st (eval_lv a gs st lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx 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 *)

src/analyses/malloc_null.ml

@@ -18,7 +18,7 @@ struct
   let should_join x y = D.equal x y
 
   (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain
-     element) answers with the string "unknown" on all non-concrete cases. *)
+     element) answers with Lval.any_index_exp on all non-concrete cases. *)
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset

src/analyses/mutexAnalysis.ml

@@ -109,7 +109,7 @@ struct
       let i_exp =
         match ValueDomain.IndexDomain.to_int i with
         | Some i -> Const (CInt (i, Cilfacade.ptrdiff_ikind (), Some (Z.to_string i)))
-        | None -> MyCFG.unknown_exp
+        | None -> Lval.any_index_exp
       in
       `Index (i_exp, conv_offset_inv o)
 

src/analyses/region.ml

@@ -83,7 +83,7 @@ struct
       let rec unknown_index = function
         | `NoOffset -> `NoOffset
         | `Field (f, os) -> `Field (f, unknown_index os)
-        | `Index (i, os) -> `Index (MyCFG.unknown_exp, unknown_index os) (* forget specific indices *)
+        | `Index (i, os) -> `Index (Lval.any_index_exp, unknown_index os) (* forget specific indices *)
       in
       Option.map (Lvals.of_list % List.map (Tuple2.map2 unknown_index)) (get_region ctx e)
 

src/analyses/uninit.ml

@@ -31,7 +31,7 @@ struct
   let exitstate  v : D.t = D.empty ()
 
   (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain
-     element) answers with the string "unknown" on all non-concrete cases. *)
+     element) answers with Lval.any_index_exp on all non-concrete cases. *)
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset

src/cdomains/arrayDomain.ml

@@ -61,6 +61,7 @@ sig
   val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool
   val update_length: idx -> t -> t
   val project: ?varAttr:attributes -> ?typAttr:attributes -> VDQ.t -> t -> t
+  val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval -> t -> Invariant.t
 end
 
 module type LatticeWithSmartOps =
@@ -85,7 +86,12 @@ struct
   let pretty () x = text "Array: " ++ pretty () x
   let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
   let get ?(checkBounds=true) (ask: VDQ.t) a i = a
-  let set (ask: VDQ.t) a i v = join a v
+  let set (ask: VDQ.t) a (ie, i) v =
+    match ie with
+    | Some ie when CilType.Exp.equal ie Lval.all_index_exp ->
+      v
+    | _ ->
+      join a v
   let make ?(varAttr=[]) ?(typAttr=[])  i v = v
   let length _ = None
 
@@ -100,6 +106,21 @@ struct
   let smart_leq _ _ = leq
   let update_length _ x = x
   let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+
+  let invariant ~value_invariant ~offset ~lval x =
+    match offset with
+    (* invariants for all indices *)
+    | NoOffset when get_bool "witness.invariant.goblint" ->
+      let i_lval = Cil.addOffsetLval (Index (Lval.all_index_exp, NoOffset)) lval in
+      value_invariant ~offset ~lval:i_lval x
+    | NoOffset ->
+      Invariant.none
+    (* invariant for one index *)
+    | Index (i, offset) ->
+      value_invariant ~offset ~lval x
+    (* invariant for one field *)
+    | Field (f, offset) ->
+      Invariant.none
 end
 
 let factor () =
@@ -170,6 +191,13 @@ struct
     if Z.geq min_i f then (xl, (Val.join xr v))
     else if Z.lt max_i f then ((update_unrolled_values min_i max_i), xr)
     else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v))
+  let set ask (xl, xr) (ie, i) v =
+    match ie with
+    | Some ie when CilType.Exp.equal ie Lval.all_index_exp ->
+      (BatList.make (factor ()) v, v)
+    | _ ->
+      set ask (xl, xr) (ie, i) v
+
   let make ?(varAttr=[]) ?(typAttr=[]) _ v =
     let xl = BatList.make (factor ()) v in
     (xl,Val.bot ())
@@ -188,6 +216,32 @@ struct
   let smart_leq _ _ = leq
   let update_length _ x = x
   let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+
+  let invariant ~value_invariant ~offset ~lval ((xl, xr) as x) =
+    match offset with
+    (* invariants for all indices *)
+    | NoOffset ->
+      let i_all =
+        if Val.is_bot xr then
+          Invariant.top ()
+        else if get_bool "witness.invariant.goblint" then (
+          let i_lval = Cil.addOffsetLval (Index (Lval.all_index_exp, NoOffset)) lval in
+          value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
+        )
+        else
+          Invariant.top ()
+      in
+      BatList.fold_lefti (fun acc i x ->
+          let i_lval = Cil.addOffsetLval (Index (Cil.integer i, NoOffset)) lval in
+          let i = value_invariant ~offset ~lval:i_lval x in
+          Invariant.(acc && i)
+        ) i_all xl
+    (* invariant for one index *)
+    | Index (i, offset) ->
+      Invariant.none (* TODO: look up *)
+    (* invariant for one field *)
+    | Field (f, offset) ->
+      Invariant.none
 end
 
 (** Special signature so that we can use the _with_length functions from PartitionedWithLength but still match the interface *
@@ -425,13 +479,16 @@ struct
 
   let set_with_length length (ask:VDQ.t) x (i,_) a =
     if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a\n" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
-    if i = Some MyCFG.all_array_index_exp then
+    match i with
+    | Some ie when CilType.Exp.equal ie Lval.all_index_exp ->
+      Joint a
+    | Some i when CilType.Exp.equal i Lval.any_index_exp ->
       (assert !Goblintutil.global_initialization; (* just joining with xm here assumes that all values will be set, which is guaranteed during inits *)
        (* the join is needed here! see e.g 30/04 *)
        let o = match x with Partitioned (_, (_, xm, _)) -> xm | Joint v -> v in
        let r =  Val.join o a in
        Joint r)
-    else
+    | _ ->
       normalize @@
       let use_last = get_string "ana.base.partition-arrays.keep-expr" = "last" in
       let exp_value e =
@@ -701,6 +758,21 @@ struct
 
   let update_length _ x = x
   let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+
+  let invariant ~value_invariant ~offset ~lval x =
+    match offset with
+    (* invariants for all indices *)
+    | NoOffset when get_bool "witness.invariant.goblint" ->
+      let i_lval = Cil.addOffsetLval (Index (Lval.all_index_exp, NoOffset)) lval in
+      value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
+    | NoOffset ->
+      Invariant.none
+    (* invariant for one index *)
+    | Index (i, offset) ->
+      Invariant.none (* TODO: look up *)
+    (* invariant for one field *)
+    | Field (f, offset) ->
+      Invariant.none
 end
 
 (* This is the main array out of bounds check *)
@@ -759,6 +831,9 @@ struct
 
   let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
 
+  let invariant ~value_invariant ~offset ~lval (x, _) =
+    Base.invariant ~value_invariant ~offset ~lval x
+
   let printXml f (x,y) =
     BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y
 
@@ -811,6 +886,9 @@ struct
 
   let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
 
+  let invariant ~value_invariant ~offset ~lval (x, _) =
+    Base.invariant ~value_invariant ~offset ~lval x
+
   let printXml f (x,y) =
     BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y
 
@@ -852,6 +930,9 @@ struct
 
   let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
 
+  let invariant ~value_invariant ~offset ~lval (x, _) =
+    Base.invariant ~value_invariant ~offset ~lval x
+
   let printXml f (x,y) =
     BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y
 
@@ -972,4 +1053,10 @@ struct
     | UnrolledDomain, (None, Some (Some x, None)) -> to_t @@ (None, None, Some (unroll_of_trivial ask x) )
     | UnrolledDomain, (None, Some (None, Some x)) -> to_t @@ (None, None, Some x)
     | _ ->  failwith "AttributeConfiguredArrayDomain received a value where not exactly one component is set"
+
+  let invariant ~value_invariant ~offset ~lval =
+    unop'
+      (P.invariant ~value_invariant ~offset ~lval)
+      (T.invariant ~value_invariant ~offset ~lval)
+      (U.invariant ~value_invariant ~offset ~lval)
 end

src/cdomains/arrayDomain.mli

@@ -57,6 +57,7 @@ sig
   val update_length: idx -> t -> t
 
   val project: ?varAttr:Cil.attributes -> ?typAttr:Cil.attributes -> VDQ.t -> t -> t
+  val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval -> t -> Invariant.t
 end
 
 module type LatticeWithSmartOps =

src/cdomains/lval.ml

@@ -4,6 +4,17 @@ open Pretty
 module GU = Goblintutil
 module M = Messages
 
+(** Special index expression for some unknown index.
+    Weakly updates array in assignment.
+    Used for exp.fast_global_inits. *)
+let any_index_exp = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "any_index")
+
+(** Special index expression for all indices.
+    Strongly updates array in assignment.
+    Used for Goblint-specific witness invariants. *)
+let all_index_exp = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index")
+
+
 type ('a, 'b) offs = [
   | `NoOffset
   | `Field of 'a * ('a,'b) offs
@@ -583,7 +594,7 @@ struct
     match o with
     | `NoOffset -> a
     | `Field (f,o) -> short_offs o (a^"."^f.fname)
-    | `Index (e,o) when CilType.Exp.equal e MyCFG.unknown_exp -> short_offs o (a^"[?]")
+    | `Index (e,o) when CilType.Exp.equal e any_index_exp -> short_offs o (a^"[?]")
     | `Index (e,o) -> short_offs o (a^"["^CilType.Exp.show e^"]")
 
   let rec of_ciloffs x =

src/cdomains/valueDomain.ml

@@ -873,7 +873,7 @@ struct
 
   let update_offset (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
     let rec do_update_offset (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t =
-      if M.tracing then M.traceli "update_offset" "do_update_offset %a %a %a\n" pretty x Offs.pretty offs pretty value;
+      if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value;
       let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in
       let r =
       match x, offs with
@@ -1317,6 +1317,7 @@ struct
     | `Address n -> ad_invariant ~vs ~offset ~lval n
     | `Struct n -> Structs.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
     | `Union n -> Unions.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
+    | `Array n -> CArrays.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
     | `Blob n when GobConfig.get_bool "ana.base.invariant.blobs" -> blob_invariant ~vs ~offset ~lval n
     | _ -> Invariant.none (* TODO *)
 

src/framework/cfgTools.ml

@@ -682,21 +682,21 @@ let getGlobalInits (file: file) : edges  =
       doInit (addOffsetLval offs lval) loc init is_zero;
       lval
     in
-    let rec all_index = function
-      | Index (e,o) -> Index (all_array_index_exp, all_index o)
-      | Field (f,o) -> Field (f, all_index o)
+    let rec any_index_offset = function
+      | Index (e,o) -> Index (Lval.any_index_exp, any_index_offset o)
+      | Field (f,o) -> Field (f, any_index_offset o)
       | NoOffset -> NoOffset
     in
-    let all_index (lh,offs) = lh, all_index offs in
+    let any_index (lh,offs) = lh, any_index_offset offs in
     match init with
     | SingleInit exp ->
       let assign lval = (loc, Assign (lval, exp)) in
       (* This is an optimization so that we don't get n*m assigns for an array a[n][m].
          Instead, we get one assign for each distinct value in the array *)
       if not fast_global_inits then
         Hashtbl.add inits (assign lval) ()
-      else if not (Hashtbl.mem inits (assign (all_index lval))) then
-        Hashtbl.add inits (assign (all_index lval)) ()
+      else if not (Hashtbl.mem inits (assign (any_index lval))) then
+        Hashtbl.add inits (assign (any_index lval)) ()
       else
         ()
     | CompoundInit (typ, lst) ->

src/framework/myCFG.ml

@@ -58,8 +58,6 @@ let unknown_exp : exp = mkString "__unknown_value__"
 let dummy_func = emptyFunction "__goblint_dummy_init" (* TODO get rid of this? *)
 let dummy_node = FunctionEntry Cil.dummyFunDec
 
-let all_array_index_exp : exp = CastE(TInt(Cilfacade.ptrdiff_ikind (),[]), unknown_exp)
-
 
 module type FileCfg =
 sig

src/util/options.schema.json

@@ -1679,7 +1679,7 @@
         "fast_global_inits": {
           "title": "exp.fast_global_inits",
           "description":
-            "Only generate one 'a[MyCFG.all_array_index_exp] = x' for all assignments a[...] = x for a global array a[n].",
+            "Only generate one 'a[any_index] = x' for all assignments a[...] = x for a global array a[n].",
           "type": "boolean",
           "default": true
         },
@@ -2319,6 +2319,12 @@
                 "cond",
                 "RETURN"
               ]
+            },
+            "goblint": {
+              "title": "witness.invariant.goblint",
+              "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.",
+              "type": "boolean",
+              "default": false
             }
           },
           "additionalProperties": false

tests/regression/56-witness/44-base-unassume-array.c

@@ -0,0 +1,16 @@
+// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 44-base-unassume-array.yml --enable ana.int.interval
+#include <goblint.h>
+
+int main() {
+  int a[10];
+
+  for (int i = 0; i < 3; i++) {
+    a[i] = i;
+  }
+
+  for (int i = 0; i < 10; i++) {
+    __goblint_check(a[i] >= 0);
+    __goblint_check(a[i] < 3);
+  }
+  return 0;
+}