Merge branch 'fix/eva/eval-address' into 'master'

[Eva] Results: adds optional argument [for_writing] to [eval_address].

See merge request frama-c/frama-c!3589

src/plugins/inout/outputs.ml

@@ -48,10 +48,10 @@ class virtual do_it_ = object(self)
     (* For local initializations, counts the written variable as an output of the
        function, even if it is const; thus, [for_writing] is false in this case. *)
   method private do_assign ~for_writing lv =
-    let access = if for_writing then Write else Read in
-    let bits_loc = Eva.Results.(
-        before_kinstr self#current_kinstr |> eval_address lv |>
-        as_zone ~access) in
+    let ki = self#current_kinstr in
+    let bits_loc =
+      Eva.Results.(before_kinstr ki |> eval_address ~for_writing lv |> as_zone)
+    in
     self#join bits_loc
 
   method! vinst i =

src/plugins/scope/datascope.ml

@@ -81,7 +81,7 @@ module InitSid = struct
 end
 
 let get_writes stmt lval =
-  Eva.Results.(before stmt |> eval_address lval |> as_zone ~access:Write)
+  Eva.Results.(before stmt |> eval_address ~for_writing:true lval |> as_zone)
 
 (** Add to [stmt] to [lmap] for all the locations modified by the statement.
  * Something to do only for calls and assignments.

src/plugins/slicing/slicingCmds.ml

@@ -55,9 +55,9 @@ let apply_all ~propagate_to_callers =
 
 let get_select_kf (fvar, _select) = Globals.Functions.get fvar
 
-let get_lval_zone ?(access=Locations.Read) stmt lval =
+let get_lval_zone ?(for_writing=false) stmt lval =
   let open Eva.Results in
-  before stmt |> eval_address lval |> as_zone ~access
+  before stmt |> eval_address ~for_writing lval |> as_zone
 
 (** Utilities for [kinstr]. *)
 module Kinstr: sig
@@ -80,7 +80,7 @@ struct
       (* returns [read_zone] joined to [Zone.t read] by [lv], [Zone.t written] by [lv] *)
       (* The modified locations are [looking_for], those address are
          function of [deps]. *)
-      let zloc = get_lval_zone ~access:Locations.Write stmt lv in
+      let zloc = get_lval_zone ~for_writing:true stmt lv in
       let deps = Eva.Results.(before stmt |> address_deps lv) in
       Locations.Zone.join read_zone deps, zloc
     in
@@ -349,8 +349,7 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
           (fun lval_str acc ->
              let lval_term = !Db.Properties.Interp.term_lval kf lval_str in
              let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
-             let access = if for_writing then Locations.Write else Locations.Read in
-             let zone = get_lval_zone ~access eval lval in
+             let zone = get_lval_zone ~for_writing eval lval in
              Locations.Zone.join zone acc)
           lval_str Locations.Zone.bottom
       in SlicingParameters.debug ~level:3

src/plugins/value/Eva.mli

@@ -193,7 +193,8 @@ module Results: sig
 
 
   (** Returns (an overapproximation of) the possible addresses of the lvalue. *)
-  val eval_address : Cil_types.lval -> request -> address evaluation
+  val eval_address : ?for_writing:bool ->
+    Cil_types.lval -> request -> address evaluation
 
 
   (** Returns the kernel functions into which the given expression may evaluate.
@@ -241,12 +242,10 @@ module Results: sig
 
   (** Converts into a Zone. Error cases are converted into bottom or top zones
       accordingly. *)
-  val as_zone: ?access:Locations.access -> address evaluation ->
-    Locations.Zone.t
+  val as_zone: address evaluation -> Locations.Zone.t
 
   (** Converts into a Zone result. *)
-  val as_zone_result : ?access:Locations.access -> address evaluation ->
-    Locations.Zone.t result
+  val as_zone_result : address evaluation -> Locations.Zone.t result
 
 
   (** Evaluation properties *)

src/plugins/value/utils/results.ml

@@ -217,7 +217,7 @@ struct
   type ('a,'c) evaluation =
     | LValue: (EvalTypes.lval, 'c) Response.t -> (value,'c) evaluation
     | Value: (EvalTypes.exp, 'c) Response.t -> (value,'c) evaluation
-    | Address: (EvalTypes.loc, 'c) Response.t * Cil_types.lval ->
+    | Address: (EvalTypes.loc, 'c) Response.t * Locations.access ->
         (address,'c) evaluation
 
   let get_by_callstack (req : request) :
@@ -308,9 +308,10 @@ struct
     let eval state = A.Eval.evaluate state exp in
     Value (Response.map eval (get req))
 
-  let eval_address lval req =
-    let eval state = A.Eval.lvaluate ~for_writing:false state lval in
-    Address (Response.map eval (get req), lval)
+  let eval_address ~for_writing lval req =
+    let eval state = A.Eval.lvaluate ~for_writing state lval in
+    let access = if for_writing then Locations.Write else Read in
+    Address (Response.map eval (get req), access)
 
   let eval_callee exp req =
     let join = (@)
@@ -347,11 +348,11 @@ struct
 
   let extract_loc :
     type c. (address, c) evaluation ->
-    (A.Loc.location or_bottom, c) Response.t * Cil_types.lval =
+    (A.Loc.location or_bottom, c) Response.t * Locations.access =
     function
-    | Address (r, lval) ->
+    | Address (r, access) ->
       let extract (x, _alarms) = x >>-: (fun (_valuation,loc,_typ) -> loc) in
-      Response.map extract r, lval
+      Response.map extract r, access
 
   let as_location res =
     match A.Loc.get Main_locations.PLoc.key with
@@ -369,22 +370,17 @@ struct
       in
       extract_loc res |> fst |> Response.map_join' extract join |> convert
 
-  let as_zone ~access res =
-    let response_loc, lv = extract_loc res in
-    let is_const_lv = Eva_utils.is_const_write_invalid (Cil.typeOfLval lv) in
-    (* No write effect if [lv] is const *)
-    if access=Locations.Write && is_const_lv
-    then Result.ok Locations.Zone.bottom
-    else
-      match A.Loc.get Main_locations.PLoc.key with
-      | None ->
-        Result.error DisabledDomain
-      | Some get ->
-        let join = Locations.Zone.join
-        and extract loc =
-          loc  >>>-: get >>>-: Precise_locs.enumerate_valid_bits access
-        in
-        response_loc |> Response.map_join' extract join |> convert
+  let as_zone res =
+    match A.Loc.get Main_locations.PLoc.key with
+    | None ->
+      Result.error DisabledDomain
+    | Some get ->
+      let response_loc, access = extract_loc res in
+      let join = Locations.Zone.join
+      and extract loc =
+        loc >>>-: get >>>-: Precise_locs.enumerate_valid_bits access
+      in
+      response_loc |> Response.map_join' extract join |> convert
 
   let is_initialized : type c. (value,c) evaluation -> bool =
     function
@@ -520,9 +516,9 @@ let eval_var vi req = eval_lval (Cil.var vi) req
 
 let eval_exp exp req = Value ((snd @@ build_eval_lval_and_exp ()) exp req)
 
-let eval_address lval req =
+let eval_address ?(for_writing=false) lval req =
   let module M = Make () in
-  let v = M.eval_address lval req in
+  let v = M.eval_address ~for_writing lval req in
   Address
     (module struct
       include M
@@ -601,12 +597,12 @@ let as_location (Address lvaluation) =
   let module E = (val lvaluation : Lvaluation) in
   E.as_location E.v
 
-let as_zone_result ?(access=Locations.Read) (Address lvaluation) =
+let as_zone_result (Address lvaluation) =
   let module E = (val lvaluation : Lvaluation) in
-  E.as_zone ~access E.v
+  E.as_zone E.v
 
-let as_zone ?access address =
-  match as_zone_result ?access address with
+let as_zone address =
+  match as_zone_result address with
   | Ok zone -> zone
   | Error Bottom -> Locations.Zone.bottom
   | Error (Top | DisabledDomain) -> Locations.Zone.top

src/plugins/value/utils/results.mli

@@ -181,7 +181,8 @@ val eval_exp : Cil_types.exp -> request -> value evaluation
 
 
 (** Returns (an overapproximation of) the possible addresses of the lvalue. *)
-val eval_address : Cil_types.lval -> request -> address evaluation
+val eval_address : ?for_writing:bool ->
+  Cil_types.lval -> request -> address evaluation
 
 
 (** Returns the kernel functions into which the given expression may evaluate.
@@ -229,12 +230,10 @@ val as_location : address evaluation -> Locations.location result
 
 (** Converts into a Zone. Error cases are converted into bottom or top zones
     accordingly. *)
-val as_zone: ?access:Locations.access -> address evaluation ->
-  Locations.Zone.t
+val as_zone: address evaluation -> Locations.Zone.t
 
 (** Converts into a Zone result. *)
-val as_zone_result : ?access:Locations.access -> address evaluation ->
-  Locations.Zone.t result
+val as_zone_result : address evaluation -> Locations.Zone.t result
 
 
 (** Evaluation properties *)