Merge pull request #861 from goblint/base-invariant-lvals

Fix base Invariant query lval and offset handling

Author: sim642

src/analyses/base.ml

@@ -1186,8 +1186,8 @@ struct
       CilLval.Set.fold (fun k a ->
           let i =
             match k with
-            | (Var k, offset) ->
-              (try var_invariant ~offset k with Not_found -> Invariant.none)
+            | (Var v, offset) when not (InvariantCil.var_is_heap v) ->
+              (try I.key_invariant_lval v ~offset ~lval:k (Arg.find v) with Not_found -> Invariant.none)
             | _ -> Invariant.none
           in
           Invariant.(a && i)

src/cdomains/structDomain.ml

@@ -28,7 +28,7 @@ sig
   val widen_with_fct: (value -> value -> value) -> t -> t -> t
   val join_with_fct: (value -> value -> value) -> t -> t -> t
   val leq_with_fct: (value -> value -> bool) -> t -> t -> bool
-  val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval option -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval option -> t -> Invariant.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 Simple (Val: Arg) =
@@ -81,18 +81,15 @@ struct
     match offset with
     (* invariants for all fields *)
     | NoOffset ->
-      let c_lval = Option.get lval in
       fold (fun f v acc ->
-          let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) c_lval in
-          let i = value_invariant ~offset ~lval:(Some f_lval) v in
+          let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) lval in
+          let i = value_invariant ~offset ~lval:f_lval v in
           Invariant.(acc && i)
         ) x (Invariant.top ())
     (* invariant for one field *)
     | Field (f, offset) ->
       let v = get x f in
-      let c_lval = Option.get lval in
-      let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) c_lval in
-      value_invariant ~offset ~lval:(Some f_lval) v
+      value_invariant ~offset ~lval v
     (* invariant for one index *)
     | Index (i, offset) ->
       Invariant.none

src/cdomains/structDomain.mli

@@ -27,7 +27,7 @@ sig
   val widen_with_fct: (value -> value -> value) -> t -> t -> t
   val join_with_fct: (value -> value -> value) -> t -> t -> t
   val leq_with_fct: (value -> value -> bool) -> t -> t -> bool
-  val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval option -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval option -> t -> Invariant.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 Simple (Val: Arg): S with type value = Val.t and type field = fieldinfo

src/cdomains/unionDomain.ml

@@ -10,7 +10,7 @@ module type S =
 sig
   include Lattice.S
   type value
-  val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval option -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval option -> t -> Invariant.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 Field =  Lattice.Flat (CilType.Fieldinfo) (struct
@@ -27,23 +27,20 @@ struct
     match offset with
     (* invariants for all fields *)
     | Cil.NoOffset ->
-      let c_lval = Option.get lval in
       begin match lift_f with
-      | `Lifted f ->
-        let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) c_lval in
-        value_invariant ~offset ~lval:(Some f_lval) v
-      | `Top
-      | `Bot ->
-        Invariant.none
+        | `Lifted f ->
+          let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) lval in
+          value_invariant ~offset ~lval:f_lval v
+        | `Top
+        | `Bot ->
+          Invariant.none
       end
     (* invariant for one field *)
     | Field (f, offset) ->
-      let c_lval = Option.get lval in
       begin match lift_f with
         | `Lifted f' ->
           let v = Values.cast ~torg:f'.ftype f.ftype v in
-          let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) c_lval in
-          value_invariant ~offset ~lval:(Some f_lval) v
+          value_invariant ~offset ~lval v
         | `Top
         | `Bot ->
           Invariant.none

src/cdomains/valueDomain.ml

@@ -1221,7 +1221,7 @@ struct
   module VS = Set.Make (Basetype.Variables)
 
   let rec ad_invariant ~vs ~offset ~lval x =
-    let c_exp = Cil.(Lval (Option.get lval)) in
+    let c_exp = Lval lval in
     let i_opt = AD.fold (fun addr acc_opt ->
         BatOption.bind acc_opt (fun acc ->
             match addr with
@@ -1246,7 +1246,7 @@ struct
                 else
                   Invariant.none
               in
-              let i_deref = deref_invariant ~vs ~lval vi offset (Mem c_exp, NoOffset) in
+              let i_deref = deref_invariant ~vs vi ~offset ~lval:(Mem c_exp, NoOffset) in
 
               Some (Invariant.(acc || (i && i_deref)))
             | Addr.NullPtr ->
@@ -1273,13 +1273,13 @@ struct
 
   and vd_invariant ~vs ~offset ~lval = function
     | `Int n ->
-      let e = Lval (Option.get lval) in
+      let e = Lval lval in
       if InvariantCil.(not (exp_contains_tmp e) && exp_is_in_scope scope e) then
         ID.invariant e n
       else
         Invariant.none
     | `Float n ->
-      let e = Lval (Option.get lval) in
+      let e = Lval lval in
       if InvariantCil.(not (exp_contains_tmp e) && exp_is_in_scope scope e) then
         FD.invariant e n
       else
@@ -1290,20 +1290,18 @@ struct
     | `Union n -> Unions.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
     | _ -> Invariant.none (* TODO *)
 
-  (* TODO: remove duplicate lval arguments? *)
-  and deref_invariant ~vs ~lval vi offset lval' =
+  and deref_invariant ~vs vi ~offset ~lval =
     let v = find vi in
-    key_invariant_lval ~vs ~lval vi offset lval' v
+    key_invariant_lval ~vs vi ~offset ~lval v
 
-  and key_invariant_lval ~vs ~lval k offset lval' v =
+  and key_invariant_lval ?(vs=VS.empty) k ~offset ~lval v =
     if not (VS.mem k vs) then
       let vs' = VS.add k vs in
-      vd_invariant ~vs:vs' ~offset ~lval:(Some lval') v
+      vd_invariant ~vs:vs' ~offset ~lval v
     else
       Invariant.none
 
-
-  let key_invariant k ?(offset=NoOffset) v = key_invariant_lval ~vs:VS.empty ~lval:None k offset (var k) v
+  let key_invariant k ?(offset=NoOffset) v = key_invariant_lval k ~offset ~lval:(var k) v
 end
 
 let invariant_global find g =