Merge pull request #1984 from goblint/valuedomain-do-offset-2

Remove type argument from `do_update_offset`, fix calls with incorrect offset type

Author: sim642

src/analyses/base.ml

@@ -1675,7 +1675,7 @@ struct
    * not include the flag. *)
   let set_mval ~(man: _ man) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) ((x, offs): Addr.Mval.t) (lval_type: Cil.typ) (value: value): store =
     let ask = Analyses.ask_of_man man in
-    let cil_offset = Offs.to_cil_offset offs in
+    let cil_offset = Offs.to_cil_offset offs in (* Only for partitioned arrays! Drops indices. *)
     let t = match t_override with
       | Some t -> t
       | None ->
@@ -1685,11 +1685,11 @@ struct
           lval_type
         else
           try
-            Cilfacade.typeOfLval (Var x, cil_offset)
-          with Cilfacade.TypeOfError _ ->
+            Offs.type_of ~base:x.vtype offs
+          with Offset.Type_of_error _ ->
             (* If we cannot determine the correct type here, we go with the one of the LVal *)
             (* This will usually lead to a type mismatch in the ValueDomain (and hence supertop) *)
-            M.debug ~category:Analyzer "Cilfacade.typeOfLval failed Could not obtain the type of %a" d_lval (Var x, cil_offset);
+            M.debug ~category:Analyzer "Could not obtain the type of %a" Addr.Mval.pretty (x, offs);
             lval_type
     in
     let update_offset old_value =
@@ -1708,7 +1708,7 @@ struct
       else
         new_value
     in
-    if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" AD.pretty (AD.of_mval (x,offs)) d_type x.vtype D.pretty st;
+    if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" Addr.Mval.pretty (x,offs) d_type t D.pretty st;
     if isFunctionType x.vtype then begin
       if M.tracing then M.tracel "set" "update_one_addr: returning: '%a' is a function type " d_type x.vtype;
       st
@@ -2002,7 +2002,7 @@ struct
               let t = v.vtype in
               let iv = VD.bot_value ~varAttr:v.vattr t in (* correct bottom value for top level variable *)
               if M.tracing then M.tracel "set" "init bot value (%a): %a" d_plaintype t VD.pretty iv;
-              let nv = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) iv offs rval_val (Some  (Lval lval)) lval t in (* do desired update to value *)
+              let nv = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) iv offs rval_val (Some  (Lval lval)) lval lval_t in (* do desired update to value *)
               set_savetop ~man  man.local (AD.of_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *)
             | _ ->
               set_savetop ~man man.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval

src/analyses/baseInvariant.ml

@@ -103,7 +103,7 @@ struct
       let old_val = get_var ~man st var in
       let old_val = map_oldval old_val var.vtype in
       let offs = convert_offset ~man st o in
-      let new_val = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) old_val offs c' (Some exp) x (var.vtype) in
+      let new_val = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) old_val offs c' (Some exp) x (Cilfacade.typeOfLval x) in
       let v = apply_invariant ~old_val ~new_val in
       if is_some_bot v then contra st
       else (

src/cdomain/value/cdomains/valueDomain.ml

@@ -978,7 +978,7 @@ struct
     do_eval_offset x offs l o
 
   let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
-    let rec do_update_offset ?(bitfield:int option=None) (x:t) (offs:offs) (l:lval option) (o:offset option) (t:typ):t = (* TODO: why does inner t argument change here, but not in eval_offset? *)
+    let rec do_update_offset ?(bitfield:int option=None) (x:t) (offs:offs) (l:lval option) (o:offset option):t =
       if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value;
       let mu = function Blob (Blob (y, s', zeroinit), s, _) -> Blob (y, ID.join s s', zeroinit) | x -> x in
       let r =
@@ -989,7 +989,7 @@ struct
           begin
             let l', o' = shift_one_over l o in
             let x = zero_init_calloced_memory zeroinit x t in
-            mu (Blob (join x (do_update_offset x ofs l' o' t), s, zeroinit))
+            mu (Blob (join x (do_update_offset x ofs l' o'), s, zeroinit))
           end
         | Blob (x,s,zeroinit), `Field(f, _) ->
           begin
@@ -1009,9 +1009,9 @@ struct
               | _ -> false
             in
             if do_strong_update then
-              Blob ((do_update_offset x offs l' o' t), s, zeroinit)
+              Blob ((do_update_offset x offs l' o'), s, zeroinit)
             else
-              mu (Blob (join x (do_update_offset x offs l' o' t), s, zeroinit))
+              mu (Blob (join x (do_update_offset x offs l' o'), s, zeroinit))
           end
         | Blob (x,s,zeroinit), `NoOffset -> (* `NoOffset is only remaining possibility for Blob here *)
           begin
@@ -1036,9 +1036,9 @@ struct
                 end
               in
               if do_strong_update then
-                Blob ((do_update_offset x offs l' o' t), s, zeroinit)
+                Blob ((do_update_offset x offs l' o'), s, zeroinit)
               else
-                mu (Blob (join x (do_update_offset x offs l' o' t), s, zeroinit))
+                mu (Blob (join x (do_update_offset x offs l' o'), s, zeroinit))
           end
         | Thread _, _ ->
           (* hack for pthread_t variables *)
@@ -1076,12 +1076,11 @@ struct
                 | _ -> value
               end
             | `Field (fld, offs) when fld.fcomp.cstruct -> begin
-                let t = fld.ftype in
                 match x with
                 | Struct str ->
                   begin
                     let l', o' = shift_one_over l o in
-                    let value' = do_update_offset ~bitfield:fld.fbitfield (Structs.get str fld) offs l' o' t in
+                    let value' = do_update_offset ~bitfield:fld.fbitfield (Structs.get str fld) offs l' o' in
                     Struct (Structs.replace str fld value')
                   end
                 | Bot ->
@@ -1092,12 +1091,11 @@ struct
                   in
                   let strc = init_comp fld.fcomp in
                   let l', o' = shift_one_over l o in
-                  Struct (Structs.replace strc fld (do_update_offset Bot offs l' o' t))
+                  Struct (Structs.replace strc fld (do_update_offset Bot offs l' o'))
                 | Top -> M.warn ~category:Imprecise "Trying to update a field, but the struct is unknown"; top ()
                 | _ -> M.warn ~category:Imprecise "Trying to update a field, but was not given a struct"; top ()
               end
             | `Field (fld, offs) -> begin
-                let t = fld.ftype in
                 let l', o' = shift_one_over l o in
                 match x with
                 | Union (last_fld, prev_val) ->
@@ -1125,20 +1123,17 @@ struct
                         top (), offs
                     end
                   in
-                  Union (`Lifted fld, do_update_offset tempval tempoffs l' o' t)
-                | Bot -> Union (`Lifted fld, do_update_offset Bot offs l' o' t)
+                  Union (`Lifted fld, do_update_offset tempval tempoffs l' o')
+                | Bot -> Union (`Lifted fld, do_update_offset Bot offs l' o')
                 | Top -> M.warn ~category:Imprecise "Trying to update a field, but the union is unknown"; top ()
                 | _ -> M.warn ~category:Imprecise "Trying to update a field, but was not given a union"; top ()
               end
             | `Index (idx, offs) -> begin
                 let l', o' = shift_one_over l o in
                 match x with
                 | Array x' ->
-                  let t = (match Cil.unrollType t with
-                      | TArray(t1 ,_,_) -> t1
-                      | _ -> t) in (* This is necessary because t is not a TArray in case of calloc *)
                   let e = determine_offset ask l o exp (Some v) in
-                  let new_value_at_index = do_update_offset (CArrays.get ask x' (e,idx)) offs l' o' t in
+                  let new_value_at_index = do_update_offset (CArrays.get ask x' (e,idx)) offs l' o' in
                   let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in
                   Array new_array_value
                 | Bot ->
@@ -1147,15 +1142,15 @@ struct
                       | _ -> t, None) in (* This is necessary because t is not a TArray in case of calloc *)
                   let x' = CArrays.bot () in
                   let e = determine_offset ask l o exp (Some v) in
-                  let new_value_at_index = do_update_offset Bot offs l' o' t in
+                  let new_value_at_index = do_update_offset Bot offs l' o' in
                   let new_array_value =  CArrays.set ask x' (e, idx) new_value_at_index in
                   let len_ci = BatOption.bind len (fun e -> Cil.getInteger @@ Cil.constFold true e) in
                   let len_id = BatOption.map (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) len_ci in
                   let newl = BatOption.default (ID.starting (Cilfacade.ptrdiff_ikind ()) Z.zero) len_id in
                   let new_array_value = CArrays.update_length newl new_array_value in
                   Array new_array_value
                 | Top -> M.warn ~category:Imprecise "Trying to update an index, but the array is unknown"; top ()
-                | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset x offs l' o' t
+                | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset x offs l' o'
                 | _ -> M.warn ~category:Imprecise "Trying to update an index, but was not given an array(%a)" pretty x; top ()
               end
           in mu result
@@ -1167,7 +1162,7 @@ struct
       | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o)
       | _ -> None, None
     in
-    do_update_offset x offs l o t
+    do_update_offset x offs l o
 
   let rec affect_move ?(replace_with_const=false) ask (x:t) (v:varinfo) movement_for_expr:t =
     let move_fun x = affect_move ~replace_with_const:replace_with_const ask x v movement_for_expr in