[Eva] Moves functions used by Inout to interpret assigns clauses in logic_inout.

Exports these functions in Eva.mli.

src/plugins/eva/Eva.mli

@@ -610,6 +610,22 @@ end
 
 module Logic_inout: sig
 
+  (** Returns the list of behaviors of the given function that are active for
+      the given initial state. *)
+  val valid_behaviors:
+    Cil_types.kernel_function -> Cvalue.Model.t -> Cil_types.behavior list
+
+  (** Evaluation of the memory zone read by the \from part of an assigns clause,
+      in the given cvalue state.  *)
+  val assigns_inputs_to_zone:
+    Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
+  (** Evaluation of the memory zone written by an assigns clauses, in the given
+      cvalue state. *)
+  val assigns_outputs_to_zone:
+    result: Cil_types.varinfo option ->
+    Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
   (** Evaluate the assigns clauses of the given function in its given pre-state,
       and compare them with the given froms (computed by the from plugin).
       Emits warnings if needed, and sets statuses to the assigns clauses. *)

src/plugins/eva/legacy/logic_inout.ml

@@ -22,6 +22,68 @@
 
 open Cil_types
 
+let valid_behaviors kf state =
+  let funspec = Annotations.funspec kf in
+  let eval_predicate pred =
+    match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
+    | True -> Alarmset.True
+    | False -> Alarmset.False
+    | Unknown -> Alarmset.Unknown
+  in
+  let ab = Active_behaviors.create eval_predicate funspec in
+  Active_behaviors.active_behaviors ab
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute inout from assigns clauses                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+let eval_error_reason fmt e =
+  if e <> Eval_terms.CAlarm
+  then Eval_terms.pretty_logic_evaluation_error fmt e
+
+let eval_tlval_as_zone assigns kind env acc t =
+  try
+    let alarm_mode = Eval_terms.Ignore in
+    let zone = Eval_terms.eval_tlval_as_zone ~alarm_mode kind env t.it_content in
+    Locations.Zone.join acc zone
+  with Eval_terms.LogicEvalError e ->
+    let pp_clause fmt =
+      if kind = Read
+      then Printer.pp_from fmt assigns
+      else Printer.pp_term fmt (fst assigns).it_content
+    in
+    Self.warning ~current:true ~once:true
+      "Failed to interpret %sassigns clause '%t'%a"
+      (if kind = Read then "inputs in " else "")
+      pp_clause eval_error_reason e;
+    Locations.Zone.top
+
+let assigns_inputs_to_zone state assigns =
+  let env = Eval_terms.env_assigns ~pre:state in
+  let treat_asgn acc (_,ins as asgn) =
+    match ins with
+    | FromAny -> Locations.Zone.top
+    | From l -> List.fold_left (eval_tlval_as_zone asgn Read env) acc l
+  in
+  match assigns with
+  | WritesAny -> Locations.Zone.top
+  | Writes l  -> List.fold_left treat_asgn Locations.Zone.bottom l
+
+let assigns_outputs_to_zone ~result state assigns =
+  let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
+  let treat_asgn acc (out,_ as asgn) =
+    if Logic_utils.is_result out.it_content && result = None
+    then acc
+    else eval_tlval_as_zone asgn Write env acc out
+  in
+  match assigns with
+  | WritesAny -> Locations.Zone.top
+  | Writes l  -> List.fold_left treat_asgn Locations.Zone.bottom l
+
+(* -------------------------------------------------------------------------- *)
+(* --- Verify assigns clauses                                             --- *)
+(* -------------------------------------------------------------------------- *)
+
 (* Eval: under-approximation of the term.  Note that ACSL states
    that assigns clauses are evaluated in the pre-state.
    We skip [\result]: it is meaningless when evaluating the 'assigns' part,

src/plugins/eva/legacy/logic_inout.mli

@@ -22,6 +22,22 @@
 
 [@@@ api_start]
 
+(** Returns the list of behaviors of the given function that are active for
+    the given initial state. *)
+val valid_behaviors:
+  Cil_types.kernel_function -> Cvalue.Model.t -> Cil_types.behavior list
+
+(** Evaluation of the memory zone read by the \from part of an assigns clause,
+    in the given cvalue state.  *)
+val assigns_inputs_to_zone:
+  Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
+(** Evaluation of the memory zone written by an assigns clauses, in the given
+    cvalue state. *)
+val assigns_outputs_to_zone:
+  result: Cil_types.varinfo option ->
+  Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
 (** Evaluate the assigns clauses of the given function in its given pre-state,
     and compare them with the given froms (computed by the from plugin).
     Emits warnings if needed, and sets statuses to the assigns clauses. *)

src/plugins/eva/register.ml

@@ -34,76 +34,6 @@ let main () =
 let () = Db.Main.extend main
 
 
-(* Functions to register in Db.Value *)
-
-let eval_error_reason fmt e =
-  if e <> Eval_terms.CAlarm
-  then Eval_terms.pretty_logic_evaluation_error fmt e
-
-let assigns_inputs_to_zone state assigns =
-  let env = Eval_terms.env_assigns ~pre:state in
-  let treat_asgn acc (_,ins as asgn) =
-    match ins with
-    | FromAny -> Zone.top
-    | From l ->
-      try
-        List.fold_left
-          (fun acc t ->
-             let z =
-               Eval_terms.eval_tlval_as_zone ~alarm_mode:Eval_terms.Ignore
-                 Read env t.it_content
-             in
-             Zone.join acc z)
-          acc
-          l
-      with Eval_terms.LogicEvalError e ->
-        Self.warning ~current:true ~once:true
-          "Failed to interpret inputs in assigns clause '%a'%a"
-          Printer.pp_from asgn eval_error_reason e;
-        Zone.top
-  in
-  match assigns with
-  | WritesAny -> Zone.top
-  | Writes l  -> List.fold_left treat_asgn Zone.bottom l
-
-let assigns_outputs_aux ~eval ~bot ~top ~join state ~result assigns =
-  let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
-  let treat_asgn acc ({it_content = out},_) =
-    if Logic_utils.is_result out && result = None
-    then acc
-    else
-      try
-        let z = eval env out in
-        join z acc
-      with Eval_terms.LogicEvalError e ->
-        Self.warning ~current:true ~once:true
-          "Failed to interpret assigns clause '%a'%a"
-          Printer.pp_term out eval_error_reason e;
-        join top acc
-  in
-  match assigns with
-  | WritesAny -> join top bot
-  | Writes l  -> List.fold_left treat_asgn bot l
-
-let assigns_outputs_to_zone =
-  let eval env term =
-    Eval_terms.eval_tlval_as_zone
-      ~alarm_mode:Eval_terms.Ignore Write env term
-  in
-  assigns_outputs_aux ~eval
-    ~bot:Locations.Zone.bottom ~top:Locations.Zone.top ~join:Locations.Zone.join
-
-let assigns_outputs_to_locations =
-  let eval env term =
-    Eval_terms.eval_tlval_as_location
-      ~alarm_mode:Eval_terms.Ignore env term
-  in
-  assigns_outputs_aux
-    ~eval
-    ~bot:[] ~top:(Locations.make_loc Locations.Location_Bits.top Int_Base.top)
-    ~join:(fun v l -> v :: l)
-
-
 (* "access" functions before evaluation, registered in Db.Value *)
 let access_value_of_lval kinstr lv =
   let state = Db.Value.get_state kinstr in
@@ -132,30 +62,19 @@ let eval_predicate ~pre ~here p =
   | False -> Property_status.False_if_reachable
   | Unknown -> Property_status.Dont_know
 
-let valid_behaviors kf state =
-  let funspec = Annotations.funspec kf in
-  let eval_predicate pred =
-    match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
-    | Eval_terms.True -> Alarmset.True
-    | Eval_terms.False -> Alarmset.False
-    | Eval_terms.Unknown -> Alarmset.Unknown
-  in
-  let ab = Active_behaviors.create eval_predicate funspec in
-  Active_behaviors.active_behaviors ab
-
 let () =
   Db.Value.is_called := Function_calls.is_called;
   Db.Value.callers := Function_calls.callsites;
   Db.Value.use_spec_instead_of_definition :=
     Function_calls.use_spec_instead_of_definition;
-  Db.Value.assigns_outputs_to_zone := assigns_outputs_to_zone;
-  Db.Value.assigns_outputs_to_locations := assigns_outputs_to_locations;
-  Db.Value.assigns_inputs_to_zone := assigns_inputs_to_zone;
+  Db.Value.assigns_outputs_to_zone :=
+    (fun s ~result a -> Logic_inout.assigns_outputs_to_zone ~result s a);
+  Db.Value.assigns_inputs_to_zone := Logic_inout.assigns_inputs_to_zone;
   Db.Value.access := access_value_of_lval;
   Db.Value.access_location := access_value_of_location;
   Db.Value.access_expr := access_value_of_expr;
   Db.Value.Logic.eval_predicate := eval_predicate;
-  Db.Value.valid_behaviors := valid_behaviors;
+  Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
   Db.From.find_deps_term_no_transitivity_state :=
     find_deps_term_no_transitivity_state;