Merge pull request #1914 from goblint/valuedomain-do-offset

Remove constant `do_eval_offset` and `do_update_offset` arguments

Author: sim642

src/cdomain/value/cdomains/valueDomain.ml

@@ -907,26 +907,26 @@ struct
 
   (* Funny, this does not compile without the final type annotation! *)
   let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t =
-    let rec do_eval_offset (ask:VDQ.t) f (x:t) (offs:offs) (exp:exp option) (l:lval option) (o:offset option) (v:lval option) (t:typ): t =
+    let rec do_eval_offset (x:t) (offs:offs) (l:lval option) (o:offset option): t =
       if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp;
       let r =
         match x, offs with
         | Blob((va, _, zeroinit) as c), `Index (_, ox) ->
           begin
             let l', o' = shift_one_over l o in
-            let ev = do_eval_offset ask f (Blobs.value c) ox exp l' o' v t in
+            let ev = do_eval_offset (Blobs.value c) ox l' o' in
             zero_init_calloced_memory zeroinit ev t
           end
         | Blob((va, _, zeroinit) as c), `Field _ ->
           begin
             let l', o' = shift_one_over l o in
-            let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t in
+            let ev = do_eval_offset (Blobs.value c) offs l' o' in
             zero_init_calloced_memory zeroinit ev t
           end
         | Blob((va, _, zeroinit) as c), `NoOffset ->
           begin
             let l', o' = shift_one_over l o in
-            let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t in
+            let ev = do_eval_offset (Blobs.value c) offs l' o' in
             zero_init_calloced_memory zeroinit ev t
           end
         | Bot, _ -> Bot
@@ -938,7 +938,7 @@ struct
               | Struct str ->
                 let x = Structs.get str fld in
                 let l', o' = shift_one_over l o in
-                do_eval_offset ask f x offs exp l' o' v t
+                do_eval_offset x offs l' o'
               | Top -> M.info ~category:Imprecise "Trying to read a field, but the struct is unknown"; top ()
               | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read a field, but was not given a struct"; top ()
             end
@@ -953,7 +953,7 @@ struct
                  | _ ->
                    let x = cast ~kind:Internal fld.ftype value in (* TODO: proper castkind *)
                    let l', o' = shift_one_over l o in
-                   do_eval_offset ask f x offs exp l' o' v t)
+                   do_eval_offset x offs l' o')
               | Union _ -> top ()
               | Top -> M.info ~category:Imprecise "Trying to read a field, but the union is unknown"; top ()
               | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read a field, but was not given a union"; top ()
@@ -963,12 +963,12 @@ struct
               match x with
               | Array x ->
                 let e = determine_offset ask l o exp v in
-                do_eval_offset ask f (CArrays.get ask x (e, idx)) offs exp l' o' v t
+                do_eval_offset (CArrays.get ask x (e, idx)) offs l' o'
               | Address _ ->
                 begin
-                  do_eval_offset ask f x offs exp l' o' v t (* this used to be `blob `address -> we ignore the index *)
+                  do_eval_offset x offs l' o' (* this used to be `blob `address -> we ignore the index *)
                 end
-              | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t
+              | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t (* TODO: why recursive call to outer function? *)
               | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()
               | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top ()
             end
@@ -980,10 +980,10 @@ struct
       | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o)
       | _ -> None, None
     in
-    do_eval_offset ask f x offs exp l o v t
+    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) (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset 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? *)
       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 =
@@ -994,7 +994,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 ask x ofs value exp l' o' v t), s, zeroinit))
+            mu (Blob (join x (do_update_offset x ofs l' o' t), s, zeroinit))
           end
         | Blob (x,s,zeroinit), `Field(f, _) ->
           begin
@@ -1017,9 +1017,9 @@ struct
               | _ -> false
             in
             if do_strong_update then
-              Blob ((do_update_offset ask x offs value exp l' o' v t), s, zeroinit)
+              Blob ((do_update_offset x offs l' o' t), s, zeroinit)
             else
-              mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit))
+              mu (Blob (join x (do_update_offset x offs l' o' t), s, zeroinit))
           end
         | Blob (x,s,zeroinit), `NoOffset -> (* `NoOffset is only remaining possibility for Blob here *)
           begin
@@ -1043,9 +1043,9 @@ struct
                 end
               in
               if do_strong_update then
-                Blob ((do_update_offset ask x offs value exp l' o' v t), s, zeroinit)
+                Blob ((do_update_offset x offs l' o' t), s, zeroinit)
               else
-                mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit))
+                mu (Blob (join x (do_update_offset x offs l' o' t), s, zeroinit))
           end
         | Thread _, _ ->
           (* hack for pthread_t variables *)
@@ -1088,7 +1088,7 @@ struct
                 | Struct str ->
                   begin
                     let l', o' = shift_one_over l o in
-                    let value' = do_update_offset ~bitfield:fld.fbitfield ask (Structs.get str fld) offs value exp l' o' v t in
+                    let value' = do_update_offset ~bitfield:fld.fbitfield (Structs.get str fld) offs l' o' t in
                     Struct (Structs.replace str fld value')
                   end
                 | Bot ->
@@ -1099,7 +1099,7 @@ 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 ask Bot offs value exp l' o' v t))
+                  Struct (Structs.replace strc fld (do_update_offset Bot offs l' o' t))
                 | 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
@@ -1132,8 +1132,8 @@ struct
                         top (), offs
                     end
                   in
-                  Union (`Lifted fld, do_update_offset ask tempval tempoffs value exp l' o' v t)
-                | Bot -> Union (`Lifted fld, do_update_offset ask Bot offs value exp l' o' v t)
+                  Union (`Lifted fld, do_update_offset tempval tempoffs l' o' t)
+                | Bot -> Union (`Lifted fld, do_update_offset Bot offs l' o' t)
                 | 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
@@ -1145,7 +1145,7 @@ struct
                       | 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 ask (CArrays.get ask x' (e,idx)) offs value exp l' o' v t in
+                  let new_value_at_index = do_update_offset (CArrays.get ask x' (e,idx)) offs l' o' t in
                   let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in
                   Array new_array_value
                 | Bot ->
@@ -1154,15 +1154,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 ask Bot offs value exp l' o' v t in
+                  let new_value_at_index = do_update_offset Bot offs l' o' t 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 ask x offs value exp l' o' v t
+                | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset x offs l' o' t
                 | _ -> M.warn ~category:Imprecise "Trying to update an index, but was not given an array(%a)" pretty x; top ()
               end
           in mu result
@@ -1174,7 +1174,7 @@ struct
       | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o)
       | _ -> None, None
     in
-    do_update_offset ask x offs value exp l o v t
+    do_update_offset x offs l o t
 
   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