Commit 1b7f90a6 authored by David Bühler's avatar David Bühler Committed by Andre Maroneze
Browse files

[Eva] Abstract domains: changes the signature of [logic_assign].

The logical clause and the pre-state are now optional. The function can now
be used to remove from a state all inferred properties that depend on a given
memory location.
This only impacts the cvalue domain, which is the only one to use the assign
clause.
parent a2c983f1
......@@ -358,12 +358,13 @@ module type S = sig
(** Logical evaluation. This API is subject to changes. *)
(* TODO: cooperative evaluation of predicates in the engine. *)
(** [logic_assign from loc_asgn pre state] applies the effect of the
[assigns ... \from ...] clause [from] to [state]. [pre] is the state
before the assign clauses, in which the terms of the clause are evaluated.
[loc_asgn] is the result of the evaluation of the [assigns] part of [from]
in [pre]. *)
val logic_assign: logic_assign -> location -> pre:state -> state -> state
(** [logic_assign None loc state] removes from [state] all inferred properties
that depend on the memory location [loc].
If the first argument is not None, it contains the logical clause being
interpreted and the pre-state in which the terms of the clause are
evaluated. The clause can be an \assign, \allocated or \free clause.
[loc] is then the memory location concerned by the clause. *)
val logic_assign: (logic_assign * state) option -> location -> state -> state
(** Evaluates a [predicate] to a logical status in the current [state].
The [logic_environment] contains the states at some labels and the
......
......@@ -673,7 +673,7 @@ module Make (Man : Input) = struct
let show_expr _valuation _state _fmt _expr = ()
let logic_assign _assigns location ~pre:_ state = kill_bases location state
let logic_assign _assigns location state = kill_bases location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
......
......@@ -308,15 +308,19 @@ module State = struct
Printer.pp_from assign pp_eval_error e;
Cvalue.V.top
let logic_assign logic_assign location ~pre:(pre_state, _) (state, sclob) =
let logic_assign logic_assign location (state, sclob) =
match logic_assign with
| Assigns assign ->
| None ->
let location = Precise_locs.imprecise_location location
and value = Cvalue.V.top in
Cvalue.Model.add_binding ~exact:false state location value, sclob
| Some (Assigns assign, (pre_state, _)) ->
let location = Precise_locs.imprecise_location location in
let env = Eval_terms.env_assigns pre_state in
let value = evaluate_from_clause env assign in
Locals_scoping.remember_if_locals_in_value sclob location value;
Cvalue.Model.add_binding ~exact:false state location value, sclob
| Frees _ | Allocates _ -> state, sclob
| Some ((Frees _ | Allocates _), _) -> state, sclob
(* ------------------------------------------------------------------------ *)
(* Initialization *)
......
......@@ -102,7 +102,7 @@ module Make_Minimal
let lval = Cil.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
let logic_assign _assigns _location ~pre:_ _state = top
let logic_assign _assigns _location _state = top
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ t _ _ = `Value t
......@@ -239,7 +239,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let lval = Cil.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
let logic_assign _assigns _location ~pre:_ _state = top
let logic_assign _assigns _location _state = top
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ t _ _ = `Value t
......
......@@ -123,8 +123,8 @@ module Make
let show_expr valuation = Domain.show_expr (lift_valuation valuation)
let logic_assign assigns location ~pre state =
Domain.logic_assign assigns (Convert.restrict_loc location) ~pre state
let logic_assign assigns location state =
Domain.logic_assign assigns (Convert.restrict_loc location) state
let evaluate_predicate = Domain.evaluate_predicate
let reduce_by_predicate = Domain.reduce_by_predicate
......
......@@ -227,9 +227,14 @@ module Make
print_one_side fmt right_log Right.name Right.pretty right)
let logic_assign assign location ~pre:(left_pre, right_pre) (left, right) =
Left.logic_assign assign location ~pre:left_pre left,
Right.logic_assign assign location ~pre:right_pre right
let logic_assign assign location (left, right) =
let left_assign, right_assign =
match assign with
| None -> None, None
| Some (assign, (left, right)) -> Some (assign, left), Some (assign, right)
in
Left.logic_assign left_assign location left,
Right.logic_assign right_assign location right
let lift_logic_env f logic_env =
Abstract_domain.{ states = (fun label -> f (logic_env.states label));
......
......@@ -503,7 +503,7 @@ module Make
| Some equality -> Equality.Equality.pretty fmt equality
| None -> ()
let logic_assign _assigns location ~pre:_ state =
let logic_assign _assigns location state =
let loc = Precise_locs.imprecise_location location in
let zone = Locations.(enumerate_valid_bits Write loc) in
kill Hcexprs.Modified zone state
......
......@@ -1296,7 +1296,7 @@ module D_Impl : Abstract_domain.S
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
let logic_assign _assigns location ~pre:_ state = kill location state
let logic_assign _assigns location state = kill location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
......
......@@ -261,7 +261,7 @@ module Internal
let initialize_variable_using_type _ _ state = state
(* TODO *)
let logic_assign _assign _location ~pre:_ _state = top
let logic_assign _assign _location _state = top
(* Logic *)
let evaluate_predicate _ _ _ = Alarmset.Unknown
......
......@@ -1235,7 +1235,7 @@ module Domain = struct
let show_expr _valuation _state _fmt _expr = ()
let logic_assign _logic_assign location ~pre:_ state =
let logic_assign _logic_assign location state =
let loc = Precise_locs.imprecise_location location in
let zone = Locations.(enumerate_valid_bits Write loc) in
let state = kill zone state in
......
......@@ -216,7 +216,7 @@ module Internal : Domain_builder.InputDomain
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
let logic_assign _assign location ~pre:_ state =
let logic_assign _assign location state =
let loc = Precise_locs.imprecise_location location in
kill loc state
......
......@@ -300,7 +300,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
let incr_loop_counter _ state = state
let leave_loop _ state = state
let logic_assign _assign location ~pre:_ state = remove location state
let logic_assign _assign location state = remove location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
......
......@@ -631,7 +631,7 @@ module Internal : Domain_builder.InputDomain
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
let logic_assign _assigns location ~pre:_ state =
let logic_assign _assigns location state =
let loc = Precise_locs.imprecise_location location in
Memory.kill loc state
......
......@@ -931,7 +931,7 @@ module Internal = struct
Traces.add_trans state (Msg msg)
(* TODO *)
let logic_assign _assign _location ~pre:_ state =
let logic_assign _assign _location state =
Traces.add_trans state (Msg "logic assign")
(* Logic *)
......
......@@ -67,7 +67,7 @@ module Make
let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
let show_expr _ _ _ _ = ()
let logic_assign _ _ ~pre:_ _ = ()
let logic_assign _ _ _ = ()
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ _ _ _ = `Value ()
......
......@@ -267,7 +267,7 @@ module Make
let env = make_env state in
let assigns_with_locations = evaluate_locations env retres_loc assigns in
let transfer state (logic_assign, location) =
Domain.logic_assign logic_assign location ~pre state
Domain.logic_assign (Some (logic_assign, pre)) location state
in
List.fold_left transfer state assigns_with_locations
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment