diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 64a4fc5df5cfb797d825dd490ef6af3eb721a477..950b8972cb76431cd7f12ed45aaf3869b6c5ea2f 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -342,10 +342,6 @@ module Results: sig
(** State requests *)
- (** Returns the list of expressions which have been inferred to be equal to
- the given expression by the Equality domain. *)
- val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
-
(** Returns the Cvalue state. Error cases are converted into the bottom or top
cvalue state accordingly. *)
val get_cvalue_model : request -> Cvalue.Model.t
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 94f68b3d3d6d77e5204678bf89416a67fed148c8..635e56b8847bf75e152ef2f9fd0558cbb8a354e5 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -450,9 +450,9 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
(* --- Evaluates an expression or lvalue into an evaluation [result]. ----- *)
- let lval_to_offsetmap lval state =
+ let lval_to_offsetmap (lval : Evast.lval) state =
let cvalue_state = get_cvalue_or_top state in
- match lval with
+ match lval.node with
| Var vi, NoOffset ->
let r = extract_single_var vi cvalue_state in
`Value r, Alarmset.none
@@ -461,8 +461,8 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let precise_loc = get_precise_loc loc in
find_offsetmap cvalue_state precise_loc
- let eval_lval lval state =
- match Cil.(unrollType (typeOfLval lval)) with
+ let eval_lval (lval : Evast.lval) state =
+ match Cil.(unrollType lval.typ) with
| TInt _ | TEnum _ | TPtr _ | TFloat _ ->
A.copy_lvalue state lval >>=: fun value -> Value value
| _ ->
@@ -489,8 +489,9 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let do_next eval state eval_point callstack =
match next_steps eval_point with
| `Condition (stmt, cond) ->
- let then_state = (A.assume_cond stmt state cond true :> dstate) in
- let else_state = (A.assume_cond stmt state cond false :> dstate) in
+ let cond' = Evast_builder.translate_exp cond in
+ let then_state = (A.assume_cond stmt state cond' true :> dstate) in
+ let else_state = (A.assume_cond stmt state cond' false :> dstate) in
Cond (eval then_state, eval else_state)
| `Effect stmt ->
let after_state = get_stmt_state ~after:true stmt callstack in
@@ -516,9 +517,11 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let evaluate (term, eval_point) callstack =
match term with
| Plval lval ->
- eval_steps (Cil.typeOfLval lval) (eval_lval lval) eval_point callstack
+ let lval' = Evast_builder.translate_lval lval in
+ eval_steps lval'.typ (eval_lval lval') eval_point callstack
| Pexpr expr ->
- eval_steps (Cil.typeOf expr) (eval_expr expr) eval_point callstack
+ let expr' = Evast_builder.translate_exp expr in
+ eval_steps expr'.typ (eval_expr expr') eval_point callstack
| Ppred pred ->
eval_steps Cil.intType (eval_pred eval_point pred) eval_point callstack
end
diff --git a/src/plugins/eva/ast/evast_utils.ml b/src/plugins/eva/ast/evast_utils.ml
index 56f944e0efab310f38af905d45309763cd16b409..6cc774741fdd5482480db0b606b4a4134a03c92c 100644
--- a/src/plugins/eva/ast/evast_utils.ml
+++ b/src/plugins/eva/ast/evast_utils.ml
@@ -187,7 +187,7 @@ let invert_relation : binop -> binop = function
| Ge -> Lt
| Eq -> Ne
| Ne -> Eq
- | _ -> assert false
+ | _ -> invalid_arg "invert_relation: must be given a comparison operator"
let conv_relation : binop -> Abstract_interp.Comp.t =
function
diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml
index 9f359ed133e988bd3e1197fa4af26eb9ef2668d3..6dbc334ca2095d4b8077bb1aae27d57785e4f852 100644
--- a/src/plugins/eva/domains/abstract_domain.ml
+++ b/src/plugins/eva/domains/abstract_domain.ml
@@ -79,6 +79,9 @@
(* The types of the Cil AST. *)
open Cil_types
+type exp = Evast.exp
+type lval = Evast.lval
+
(* Definition of the types frequently used in Eva. *)
open Eval
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index ec320503fdf6537338066f6f4f02b6c7639838fc..751103832d6fe17bebee19844f08ee0b71608a7e 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -20,8 +20,8 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
+open Evast
open Apron
let dkey = Self.register_category "d-apron"
@@ -35,21 +35,21 @@ let abort exclog =
print_exc exclog.exn print_funid exclog.funid exclog.msg
let is_relevant_varinfo varinfo =
- not (Cil.typeHasQualifier "volatile" varinfo.vtype)
+ not (Cil.typeHasQualifier "volatile" varinfo.Cil_types.vtype)
&& (true || not varinfo.vglob)
-let is_relevant_lval = function
+let is_relevant_lval lval = match lval.node with
| Var varinfo, NoOffset -> is_relevant_varinfo varinfo
| _ -> false
-let rec contains_relevant_lval expr = match expr.enode with
+let rec contains_relevant_lval expr = match expr.node with
| Lval lval -> is_relevant_lval lval
| UnOp (_, e, _) | CastE (_, e) -> contains_relevant_lval e
| BinOp (_, e1, e2, _) ->
contains_relevant_lval e1 || contains_relevant_lval e2
| _ -> false
-let is_relevant expr = match expr.enode with
+let is_relevant expr = match expr.node with
| Lval _ -> true
| UnOp (_, e, _) | CastE (_, e) -> contains_relevant_lval e
| BinOp (_, e1, e2, _) ->
@@ -237,7 +237,7 @@ let translate_varinfo varinfo =
var
| _ -> raise (Out_of_Scope "translate_varinfo not integer")
-let translate_lval = function
+let translate_lval lval = match lval.node with
| Var varinfo, NoOffset -> translate_varinfo varinfo
| _ -> raise (Out_of_Scope "translate_lval not Var")
@@ -249,7 +249,7 @@ let translate_constant = function
| _ -> raise (Out_of_Scope "translate_constant not integer")
(* Translation of expressions from cil to apron. *)
-let rec translate_expr eval oracle expr = match expr.enode with
+let rec translate_expr eval oracle expr = match expr.node with
| Const cst -> Texpr1.Cst (translate_constant cst)
| Lval lval -> Texpr1.Var (translate_lval lval)
| UnOp (Neg, e1, typ) ->
@@ -261,15 +261,15 @@ let rec translate_expr eval oracle expr = match expr.enode with
let e1' = translate_expr_linearize eval oracle e1 in
let e2' = translate_expr_linearize eval oracle e2 in
let need_coercion = op = Mod || op = Div in
- let e1' = if need_coercion then coerce eval (Cil.typeOf e1) e1' else e1' in
- let e2' = if need_coercion then coerce eval (Cil.typeOf e2) e2' else e2' in
+ let e1' = if need_coercion then coerce eval e1.typ e1' else e1' in
+ let e2' = if need_coercion then coerce eval e2.typ e2' else e2' in
let op' = translate_binop op in
Texpr1.(Binop (op', e1', e2', translate_typ typ, round))
| CastE (typ, e)->
coerce ~cast:true eval typ (translate_expr_linearize eval oracle e)
| AddrOf _ | StartOf _ -> raise (Out_of_Scope "translate_expr addr")
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
- match Cil.constFoldToInt expr with
+ match Evast_utils.fold_to_integer expr with
| None -> raise (Out_of_Scope "translate_expr sizeof alignof")
| Some i -> Texpr1.Cst (Coeff.s_of_int (Integer.to_int_exn i))
(* Expressions that cannot be translated by [translate_expr] are replaced
@@ -281,17 +281,17 @@ and translate_expr_linearize eval oracle expr =
(* Express a cil expression into an apron constraint. *)
let rec constraint_expr eval oracle env expr positive =
- match expr.enode with
+ match expr.node with
| UnOp (LNot, e, _) -> constraint_expr eval oracle env e (not positive)
| BinOp ((Le|Ne|Eq|Gt|Lt|Ge as binop), e1, e2, typ) ->
let e1' = translate_expr_linearize eval oracle e1 in
let e2' = translate_expr_linearize eval oracle e2 in
- let e1'' = coerce eval (Cil.typeOf e1) e1' in
- let e2'' = coerce eval (Cil.typeOf e2) e2' in
+ let e1'' = coerce eval e1.typ e1' in
+ let e2'' = coerce eval e2.typ e2' in
let typ = translate_typ (Cil.unrollType typ) in
let e = Texpr1.Binop (Texpr1.Sub, e1'', e2'', typ, round) in
let expr = Texpr1.of_expr env e in
- let binop = Eva_utils.conv_comp binop in
+ let binop = Evast_utils.conv_relation binop in
let binop = if positive then binop else Abstract_interp.Comp.inv binop in
translate_relation expr typ binop
| _ -> raise (Out_of_Scope "constraint_expr not handled")
@@ -450,7 +450,7 @@ module Make (Man : Input) = struct
let _constraint_to_typ env state vars =
let aux (var_apron, vi) =
- match Eval_typ.classify_as_scalar vi.vtype with
+ match Eval_typ.classify_as_scalar vi.Cil_types.vtype with
| Some (Eval_typ.TSInt range) ->
let inf, sup, _size = bounds_of_typ range in
let inf = Scalar.of_mpqf (Mpqf.of_mpz inf)
@@ -495,10 +495,10 @@ module Make (Man : Input) = struct
| Z.Overflow | Failure _ -> top
let extract_expr ~oracle:_ _context state expr =
- compute state expr (Cil.typeOf expr)
+ compute state expr expr.typ
let extract_lval ~oracle:_ _context state lval typ _loc =
- let expr = Eva_utils.lval_to_exp lval in
+ let expr = Evast_builder.lval lval in
compute state expr typ
let maybe_bottom state =
@@ -559,7 +559,7 @@ module Make (Man : Input) = struct
into Apron intervals. *)
let make_oracle valuation =
fun exp exn ->
- if Cil.isIntegralType (Cil.typeOf exp) then
+ if Cil.isIntegralType exp.typ then
match valuation.Abstract_domain.find exp with
| `Value { value = { v = `Value itv } } ->
let interval = ival_to_interval itv in
@@ -579,7 +579,7 @@ module Make (Man : Input) = struct
then
try
let expr = translate_expr_linearize eval oracle exp in
- let expr = coerce eval (Cil.typeOf exp) expr in
+ let expr = coerce eval exp.typ expr in
(* When the value is top or bottom, no constraint is expressible. *)
let cons = record.value.v >>- fun ival ->
let interval = ival_to_interval ival in
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index dd54fc49505d64cda2157bcfd8a9587898b950fc..268fc9925b6e9f8653fe11545a40db6b428517f8 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -244,7 +244,7 @@ let compute_arguments arguments rest =
in
let list = List.map (fun arg -> arg.concrete, compute arg.avalue) arguments in
let rest = List.map (fun (exp, v) -> exp, compute v) rest in
- list @ rest
+ List.map (fun (exp, v) -> Evast_utils.to_cil_exp exp, v) (list @ rest)
let process_result call state call_result =
let clob = Locals_scoping.bottom () in
@@ -254,7 +254,8 @@ let process_result call state call_result =
let b_ret = Base.of_varinfo vi_ret in
let offsm = Eval_op.offsetmap_of_v ~typ:vi_ret.vtype value in
let prefix = "Builtin " ^ Kernel_function.get_name call.kf in
- Cvalue_transfer.warn_imprecise_offsm_write ~prefix (Cil.var vi_ret) offsm;
+ let lval_ret = Evast_builder.var vi_ret in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix lval_ret offsm;
Cvalue.Model.add_base b_ret offsm state, clob
| _, _ -> state, clob (* TODO: error? *)
in
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index cc33f02c7db7e07a260ca99dfd49d901b6959230..1173be960017738cd0d0604cfa535d8560885381 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -32,9 +32,9 @@ let dkey = Self.register_category "imprecision"
let rec lval_of_address exp =
match exp.enode with
- | AddrOf lval -> lval
+ | AddrOf lval -> Evast_builder.translate_lval lval
| CastE (_typ, exp) -> lval_of_address exp
- | _ -> Cil.mkMem ~addr:exp ~off:Cil_types.NoOffset
+ | _ -> Evast_builder.mem (Evast_builder.translate_exp exp)
let plevel = Parameters.ArrayPrecisionLevel.get
diff --git a/src/plugins/eva/domains/cvalue/builtins_misc.ml b/src/plugins/eva/domains/cvalue/builtins_misc.ml
index 08bedfdd74b4f1ab7c6a58730471800f49409c49..18114892b1f9049954afb37bc16dcb7a784501f4 100644
--- a/src/plugins/eva/domains/cvalue/builtins_misc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_misc.ml
@@ -37,6 +37,7 @@ let frama_C_assert state actuals =
else if Cvalue.V.contains_zero arg
then begin
let state =
+ let arg_exp = Evast_builder.translate_exp arg_exp in
let* valuation = fst (Cvalue_queries.reduce state arg_exp true) in
let valuation = Cvalue_queries.to_domain_valuation valuation in
Cvalue_transfer.update valuation state
diff --git a/src/plugins/eva/domains/cvalue/builtins_split.ml b/src/plugins/eva/domains/cvalue/builtins_split.ml
index 334913fd178b88b29aae628e0a2132c1f26ea214..8bf921c0940070a64aa6b1d4158099d747738d62 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_split.ml
@@ -74,7 +74,8 @@ let warning warn s =
[max_card] elements. *)
let split_v ~warn lv state max_card =
if Cil.isArithmeticOrPointerType (Cil.typeOfLval lv) then
- let loc = Cvalue_queries.lval_to_loc state lv in
+ let lv' = Evast_builder.translate_lval lv in
+ let loc = Cvalue_queries.lval_to_loc state lv' in
if Locations.Location_Bits.cardinal_zero_or_one loc.Locations.loc then
let v_indet = Cvalue.Model.find_indeterminate state loc in
let v = Cvalue.V_Or_Uninitialized.get_v v_indet in
diff --git a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
index d9e6f24dfe9028b7963c742cf2ec358da37dddb3..d24bfc1feefd64b1f9181ecb4d29aae4bef0a1ea 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
@@ -32,4 +32,4 @@ let offsetmap_of_assignment state expr = function
| Copy (lv, _value) ->
Bottom.non_bottom (Eval_op.offsetmap_of_loc lv.lloc state)
| Assign value ->
- offsetmap_of_v ~typ:(Cil.typeOf expr) value
+ offsetmap_of_v ~typ:expr.Evast.typ value
diff --git a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
index ef0355a15813b8f8c8d8f0de62a29c6039589814..185292cb1fe528f71144c7fa61de68aa11471be7 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
@@ -22,12 +22,11 @@
(** Auxiliary functions on cvalue offsetmaps, used by the cvalue domain. *)
-open Cil_types
open Cvalue
(** Computes the offsetmap for an assignment:
- in case of a copy, extracts the offsetmap from the state;
- otherwise, translates the value assigned into an offsetmap. *)
val offsetmap_of_assignment:
- Model.t -> exp -> (Precise_locs.precise_location, V.t) Eval.assigned ->
+ Model.t -> Evast.exp -> (Precise_locs.precise_location, V.t) Eval.assigned ->
V_Offsetmap.t
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index f6a375c1366fc68c9e6f2f931e357e0ba9c1acfc..dc29f792434d3347aeeec3e750badca6a2577496 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -45,6 +45,7 @@ module Queries = struct
let status =
if Cvalue.V.is_bottom (get_v v) then Alarmset.False else Alarmset.Unknown
in
+ let lval = Evast_utils.to_cil_lval lval in
match v with
| C_uninit_noesc _ -> Alarmset.singleton ~status (Alarms.Uninitialized lval)
| C_init_esc _ -> Alarmset.singleton ~status (Alarms.Dangling lval)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.mli b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
index f2b03356ad70e9052684db92e1b327b88e9e4c71..bb32e78e1c38833fddec28d289b941f27295232e 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
@@ -36,4 +36,4 @@ include Evaluation_sig.S with type state := state
and type origin := origin
(** Evaluates the location of a lvalue in a given cvalue state. *)
-val lval_to_loc: state -> Cil_types.lval -> Locations.location
+val lval_to_loc: state -> Evast.lval -> Locations.location
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 42610cca8f0c3d439baaf7b1a4f20af457c42593..b77e15acd93df827178fa36cbee061466fd0e412 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -20,8 +20,8 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
+open Evast
type value = Main_values.CVal.t
type origin = value
@@ -42,7 +42,7 @@ let warn_imprecise_value ?prefix lval value =
let prefix = Option.fold ~none:"A" ~some:(fun s -> s ^ ": a") prefix in
Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
"@[%sssigning imprecise value to %a@ because of %s.@]%t"
- prefix Printer.pp_lval lval (Origin.descr origin)
+ prefix Evast_printer.pp_lval lval (Origin.descr origin)
Eva_utils.pp_callstack
| _ -> ()
@@ -70,8 +70,7 @@ let warn_imprecise_offsm_write ?prefix lval offsm =
(* ---------------------------------------------------------------------- *)
let reduce valuation lval value t =
- let typ = Cil.typeOfLval lval in
- if Cil.typeHasQualifier "volatile" typ
+ if Cil.typeHasQualifier "volatile" lval.typ
then t
else
match valuation.Abstract_domain.find_loc lval with
@@ -91,9 +90,9 @@ let is_smaller_value typ v1 v2 =
(* Update the state according to a Valuation. *)
let update valuation t =
let process exp record t =
- match exp.enode with
+ match exp.node with
| Lval lv ->
- if record.reductness = Reduced && Cil.isScalarType (Cil.typeOfLval lv)
+ if record.reductness = Reduced && Cil.isScalarType lv.typ
then
let {v; initialized; escaping} = record.value in
let v = unbottomize v in
@@ -105,8 +104,7 @@ let update valuation t =
abstract values to choose the best value to keep. *)
match record.origin with
| Some previous_v ->
- let typ = Cil.typeOfLval lv in
- if is_smaller_value typ v previous_v then v else previous_v
+ if is_smaller_value lv.typ v previous_v then v else previous_v
| _ -> v
in
let value = Cvalue.V_Or_Uninitialized.make ~initialized ~escaping v in
@@ -220,7 +218,7 @@ let actualize_formals state arguments =
let offsm =
Cvalue_offsetmap.offsetmap_of_assignment state arg.concrete arg.avalue
in
- warn_imprecise_offsm_write (Cil.var arg.formal) offsm;
+ warn_imprecise_offsm_write (Evast_builder.var arg.formal) offsm;
Cvalue.Model.add_base (Base.of_varinfo arg.formal) offsm state
in
List.fold_left treat_one_formal state arguments
@@ -232,15 +230,14 @@ let finalize_call _stmt _call _recursion ~pre:_ ~post:state =
`Value state
let show_expr valuation state fmt expr =
- match expr.enode with
+ match expr.node with
| Lval lval | StartOf lval ->
let loc = match valuation.Abstract_domain.find_loc lval with
| `Value record -> record.loc
| `Top -> assert false
in
let offsm = Bottom.non_bottom (Eval_op.offsetmap_of_loc loc state) in
- let typ = Cil.typeOfLval lval in
- Eval_op.pretty_offsetmap typ fmt offsm
+ Eval_op.pretty_offsetmap lval.typ fmt offsm
| _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.mli b/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
index fd30e64f87cfc22d8a00627cc8de69cffd9ee117..a04d9a982874aea74addd0a3d1dd9becbd4916c8 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
@@ -36,13 +36,13 @@ include Abstract_domain.Transfer
value [v] into location [loc] if one of them is overly imprecise. [lval] is
the assigned lvalue, and [prefix] is an optional prefix to the warning. *)
val warn_imprecise_write:
- ?prefix:string -> Cil_types.lval -> Locations.location -> Cvalue.V.t -> unit
+ ?prefix:string -> Evast.lval -> Locations.location -> Cvalue.V.t -> unit
(** [warn_imprecise_offsm_write lval offsm] emits a warning about the assignment
of offsetmap [offsm] if it contains an overly imprecise value. [lval] is the
assigned lvalue, and [prefix] is an optional prefix to the warning. *)
val warn_imprecise_offsm_write:
- ?prefix:string -> Cil_types.lval -> Cvalue.V_Offsetmap.t -> unit
+ ?prefix:string -> Evast.lval -> Cvalue.V_Offsetmap.t -> unit
(*
Local Variables:
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index 76daf8972998165baf7faed8160bbb9787b3f371..5f717fd6f54596dd395d91b53a577d2780689ca3 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -165,7 +165,7 @@ module Make_Minimal
Domain.initialize_variable lval ~initialized value state
let initialize_variable_using_type _kind varinfo state =
- let lval = Cil.var varinfo in
+ let lval = Evast_builder.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
let logic_assign _assigns _location _state = top
@@ -295,7 +295,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
Domain.initialize_variable lval ~initialized value state
let initialize_variable_using_type _kind varinfo state =
- let lval = Cil.var varinfo in
+ let lval = Evast_builder.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
let logic_assign _assigns _location _state = top
diff --git a/src/plugins/eva/domains/equality/equality.ml b/src/plugins/eva/domains/equality/equality.ml
index b5233ec148bc9a55465b2b0d662519f0037b6c0f..3295cf02364c9953fb101a332b376e874a14a06e 100644
--- a/src/plugins/eva/domains/equality/equality.ml
+++ b/src/plugins/eva/domains/equality/equality.ml
@@ -184,12 +184,12 @@ module Set = struct
let pick_representative set =
let choose elt (current, height) =
let elt = HCE.to_exp elt in
- let h = Eva_utils.height_expr elt in
+ let h = Evast_utils.height_exp elt in
if h < height then (elt, h) else (current, height)
in
let head = HCESet.choose set in
let current = HCE.to_exp head in
- let height = Eva_utils.height_expr current in
+ let height = Evast_utils.height_exp current in
fst (HCESet.fold choose (HCESet.remove head set) (current, height))
(* Binds the terms of the [equality] to [equality] in the [map].
diff --git a/src/plugins/eva/domains/equality/equality.mli b/src/plugins/eva/domains/equality/equality.mli
index f05fcdcc9d518799d92e120479929be9ac069c1f..c88dbbb1ff131008a14bfe04ded26005b9a9d4f8 100644
--- a/src/plugins/eva/domains/equality/equality.mli
+++ b/src/plugins/eva/domains/equality/equality.mli
@@ -22,8 +22,6 @@
(** Equalities between syntactic lvalues and expressions. *)
-open Cil_types
-
type 'a trivial = Trivial | NonTrivial of 'a
type 'a tree = Empty | Leaf of 'a | Node of 'a tree * 'a tree
@@ -120,7 +118,7 @@ module Set : sig
(** [remove lval set] remove any expression [e] such that [lval] belongs to
[syntactic_lval e] from the set of equalities [set]. *)
- val remove : Hcexprs.kill_type -> lval -> t -> t
+ val remove : Hcexprs.kill_type -> Evast.lval -> t -> t
(** [unite (a, a_set) (b, b_set) map] unites [a] and [b] in [map].
[a_set] must be equal to [syntactic_lval a],
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 680f09fd4ec955d1b4a65f64c33b6505f3c68da6..ede5722da837c345a694b2dad0e96f3873a39f34 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
type call_init_state =
@@ -201,7 +200,7 @@ struct
Equality.Equality.fold
(fun atom acc ->
let e = HCE.to_exp atom in
- if Cil_datatype.ExpStructEq.equal e expr
+ if Evast_datatype.Exp.equal e expr
then acc else (e, value) :: acc)
equality []
| None -> []
@@ -241,7 +240,7 @@ struct
| None -> `Value (Value.top, None), Alarmset.all
let extract_expr ~oracle _context (equalities, _, _) expr =
- let expr = Cil.constFold true expr in
+ let expr = Evast_utils.const_fold expr in
let atom_e = HCE.of_exp expr in
coop_eval oracle equalities atom_e
@@ -320,11 +319,11 @@ struct
| E _ -> assert false
| LV lv ->
let zone =
- match lv with
+ match lv.node with
| Var vi, NoOffset -> Locations.zone_of_varinfo vi
| _ ->
- let expr = Cil.dummy_exp (Lval lv) in
- Eva_utils.zone_of_expr (find_loc valuation) expr
+ let expr = Evast_builder.lval lv in
+ Evast_utils.zone_of_exp (find_loc valuation) expr
in
Deps.add lval zone deps
@@ -346,8 +345,8 @@ struct
| `Top -> false (* should not happen *)
| `Value { value = { v } } -> is_singleton v
- let expr_is_cardinal_zero_or_one_loc valuation e =
- match e.enode with
+ let expr_is_cardinal_zero_or_one_loc valuation (e : Evast.exp) =
+ match e.node with
| Lval lv -> begin
let loc = valuation.Abstract_domain.find_loc lv in
match loc with
@@ -380,9 +379,9 @@ struct
the reevaluation of [right_expr] would reduce it incorrectly, by
removing indeterminate flags without emitting alarms. *)
let assign_eq left_lval right_expr value valuation state =
- if Eval_typ.lval_contains_volatile left_lval ||
- Eval_typ.expr_contains_volatile right_expr ||
- not (Cil.isArithmeticOrPointerType (Cil.typeOfLval left_lval)) ||
+ if Evast_utils.lval_contains_volatile left_lval ||
+ Evast_utils.exp_contains_volatile right_expr ||
+ not (Cil.isArithmeticOrPointerType left_lval.typ) ||
indeterminate_copy value
then state
else
@@ -402,12 +401,12 @@ struct
let left_loc = Precise_locs.imprecise_location left_value.lloc in
let direct_left_zone = Locations.(enumerate_valid_bits Write left_loc) in
let state = kill Hcexprs.Modified direct_left_zone state in
- let right_expr = Cil.constFold true right_expr in
+ let right_expr = Evast_utils.const_fold right_expr in
try
let indirect_left_zone =
- Eva_utils.indirect_zone_of_lval (find_loc valuation) left_value.lval
+ Evast_utils.indirect_zone_of_lval (find_loc valuation) left_value.lval
and right_zone =
- Eva_utils.zone_of_expr (find_loc valuation) right_expr
+ Evast_utils.zone_of_exp (find_loc valuation) right_expr
in
(* After an assignment lv = e, the equality [lv == eq] holds iff the value
of [e] and the location of [lv] are not modified by the assignment,
@@ -432,7 +431,7 @@ struct
state
else
try
- let left_value = Var arg.formal, NoOffset in
+ let left_value = Evast_builder.var arg.formal in
assign_eq left_value arg.concrete arg.avalue valuation state
with Top_location -> state
in
@@ -447,18 +446,18 @@ struct
reasoning. This is the case for equalities between 0. and -0., and
between non-comparable pointers, so we need to skip such equalities. *)
let assume _stmt expr positive valuation (eqs, deps, modified_zone as state) =
- match positive, expr.enode with
+ match positive, (expr : Evast.exp).node with
| true, BinOp (Eq, e1, e2, _)
| false, BinOp (Ne, e1, e2, _) ->
begin
if not (is_safe_equality valuation e1 e2)
then `Value state
else
- let e1 = Cil.constFold true e1
- and e2 = Cil.constFold true e2 in
- if Eval_typ.expr_contains_volatile e1
- || Eval_typ.expr_contains_volatile e2
- || not (Cil.isArithmeticOrPointerType (Cil.typeOf e1))
+ let e1 = Evast_utils.const_fold e1
+ and e2 = Evast_utils.const_fold e2 in
+ if Evast_utils.exp_contains_volatile e1
+ || Evast_utils.exp_contains_volatile e2
+ || not (Cil.isArithmeticOrPointerType e1.typ)
|| (expr_is_cardinal_zero_or_one_loc valuation e1 &&
expr_cardinal_zero_or_one valuation e2)
|| (expr_is_cardinal_zero_or_one_loc valuation e2 &&
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 4fc078eb9d22f2fe0b19235dae08aa01cae1daee..6715362e5916a757a308c06631af26710138a50a 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
type function_calls =
@@ -547,7 +546,7 @@ module G = struct
"λ" Bounds.pretty i.nb MC.pretty i.coeffs
let pretty_loop_step fmt (stmt, ii) =
- Format.fprintf fmt "s%d: %a" stmt.sid pretty_iteration_info ii
+ Format.fprintf fmt "s%d: %a" stmt.Cil_types.sid pretty_iteration_info ii
let pretty_loop_info =
Pretty_utils.pp_list ~pre:"@[<v>" ~suf:"@]" ~sep:"@ " pretty_loop_step
@@ -768,7 +767,7 @@ module G = struct
(* This function returns [true] if [vi] _may_ be tracked. Variables for
which we return [false] will never be part of a state. *)
let tracked_variable vi =
- Cil.isIntegralOrPointerType vi.vtype &&
+ Cil.isIntegralOrPointerType vi.Cil_types.vtype &&
(match function_calls_handling with
| FullInterprocedural -> true
| IntraproceduralAll -> not vi.vglob
@@ -992,15 +991,15 @@ module G = struct
with Not_found -> raise Untranslatable
let translate_exp state to_loc to_v e =
- let ptr_size e =
- let typ_pointed = Cil.typeOf_pointed (Cil.typeOf e) in
+ let ptr_size (e : Evast.exp) =
+ let typ_pointed = Cil.typeOf_pointed e.typ in
try Integer.of_int (Cil.bytesSizeOf typ_pointed)
with Cil.SizeOfError _ -> raise Untranslatable
in
(* This function translates the expression as a precise gauge. For any
expression that cannot be handled, [Untranslatable] is raised. *)
let rec aux_gauge e =
- match e.enode with
+ match (e : Evast.exp).node with
| Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
| AddrOf _ | StartOf _ ->
raise Untranslatable (* constant: using linearization directly *)
@@ -1009,15 +1008,15 @@ module G = struct
fits_in_type ~is_cast:true typ_dst (aux e)
| Lval lv ->
- let b = loc_to_base (to_loc lv) (Cil.typeOfLval lv) in
+ let b = loc_to_base (to_loc lv) lv.typ in
gauge_from_state b state
| UnOp (Neg , e, _) ->
- fits_in_type (Cil.typeOf e) (Gauge.neg (aux e))
+ fits_in_type e.typ (Gauge.neg (aux e))
| UnOp ((BNot | LNot) ,_,_) -> raise Untranslatable
- | BinOp (op, e1, e2, _) -> aux_binop (Cil.typeOf e) op e1 e2
+ | BinOp (op, e1, e2, _) -> aux_binop e.typ op e1 e2
and aux_binop typ_res op e1 e2 =
let g = match op with
@@ -1097,7 +1096,7 @@ module G = struct
let assign to_loc to_v lv e state =
let loc = to_loc lv in
try
- let b = loc_to_base loc (Cil.typeOfLval lv) in
+ let b = loc_to_base loc lv.Evast.typ in
let g = translate_exp state to_loc to_v e in
store_gauge b g state
with Untranslatable ->
@@ -1155,14 +1154,14 @@ module D : Abstract_domain.Leaf
let assume_exp valuation e r state =
if r.reductness = Created || r.reductness = Reduced then
- match e.enode with
+ match (e : Evast.exp).node with
| Lval lv -> begin
match valuation.Abstract_domain.find_loc lv with
| `Top -> `Value state
| `Value {loc} ->
let loc = Precise_locs.imprecise_location loc in
try
- let b = loc_to_base loc (Cil.typeOfLval lv) in
+ let b = loc_to_base loc lv.typ in
match r.value.v with
| `Bottom -> `Value state
| `Value v ->
diff --git a/src/plugins/eva/domains/hcexprs.ml b/src/plugins/eva/domains/hcexprs.ml
index f698b1c9f0b531800ad42035310d404e877e538b..5d3de97c1f57538a7681f60fb525daa3649f6b47 100644
--- a/src/plugins/eva/domains/hcexprs.ml
+++ b/src/plugins/eva/domains/hcexprs.ml
@@ -20,22 +20,8 @@
(* *)
(**************************************************************************)
-open Cil_types
-
-(* The default comparison of Cil_datatype does not distinguish constants
- with different textual representations in the source code when they
- represent the same value.
- However, when option -eva-all-rounding-modes-constants is enabled, the
- evaluation of floating-point constants may differ according to their
- textual representation: when the constant is not exactly representable in the
- floating-point type, an interval is used instead of the nearest singleton
- value. In this case, two constants with the same nearest value but different
- textual representation may not be equal. We thus use the [compare_strict]
- comparison, which also compares the textual representation of constants. *)
-
-module Exp = Cil_datatype.ExpStructEqStrict
-
-module Lval = Cil_datatype.LvalStructEqStrict
+module Exp = Evast_datatype.Exp
+module Lval = Evast_datatype.Lval
(* lvalues are never stored under a constructor [E]. *)
type unhashconsed_exprs = E of Exp.t | LV of Lval.t
@@ -55,7 +41,7 @@ module E = struct
type t = unhashconsed_exprs
let name = "Value.Symbolic_exprs.key"
- let reprs = [ E Cil_datatype.Exp.dummy ]
+ let reprs = List.map (fun e -> E e) Evast_datatype.Exp.reprs
let structural_descr =
Structural_descr.t_sum
@@ -83,24 +69,21 @@ module E = struct
let copy c = c
end)
- let replace_visitor kind ~late ~heir = object
- inherit Visitor.frama_c_copy (Project.current ())
-
- method! vexpr expr =
- match expr.enode with
+ let replace kind ~late ~heir =
+ let open Evast_visitor.Rewrite in
+ let rewrite_exp ~visitor (exp : Evast.exp) =
+ match exp.node with
| Lval lval ->
- if Lval.equal lval late then Cil.ChangeTo heir else Cil.JustCopy
+ if Lval.equal lval late then heir else exp
| StartOf lval | AddrOf lval ->
if kind = Modified
- then Cil.JustCopy
- else if Lval.equal lval late then raise NonExchangeable else Cil.JustCopy
+ then exp
+ else if Lval.equal lval late then raise NonExchangeable else exp
| AlignOfE _ -> raise NonExchangeable
- | _ -> Cil.DoChildren
- end
-
- let replace kind ~late ~heir expr =
- let visitor = replace_visitor kind ~late ~heir in
- Visitor.visitFramacExpr visitor expr
+ | _ -> default.rewrite_exp ~visitor exp
+ in
+ let rewriter = { default with rewrite_exp } in
+ Evast_visitor.Rewrite.visit_exp rewriter
end
module HCE = struct
@@ -118,14 +101,14 @@ module HCE = struct
let of_lval lv = hashcons (LV lv)
- let of_exp exp =
- match exp.enode with
+ let of_exp (exp : Evast.exp) =
+ match exp.node with
| Lval lv -> of_lval lv
| _ -> hashcons (E exp)
let to_exp h = match get h with
| E e -> e
- | LV lv -> Eva_utils.lval_to_exp lv
+ | LV lv -> Evast_builder.lval lv
let to_lval h = match get h with
| E _ -> None
@@ -136,13 +119,13 @@ module HCE = struct
| LV _ -> true
let type_of h = match get h with
- | E e -> Cil.typeOf e
- | LV lv -> Cil.typeOfLval lv
+ | E e -> e.typ
+ | LV lv -> lv.typ
let replace kind ~late ~heir h = match get h with
| E e ->
let e = E.replace kind ~late ~heir e in
- if Eva_utils.height_expr e > height_limit
+ if Evast_utils.height_exp e > height_limit
then raise NonExchangeable
else of_exp e
| LV lval -> if Lval.equal lval late then of_exp heir else h
@@ -159,13 +142,13 @@ type lvalues = {
let empty_lvalues = { read = HCESet.empty; addr = HCESet.empty; }
let syntactic_lvalues expr =
- let rec gather expr lvalues =
- match expr.enode with
+ let rec gather (expr : Evast.exp) lvalues =
+ match expr.node with
| Lval lv ->
{ lvalues with read = HCESet.add (HCE.of_lval lv) lvalues.read }
| AddrOf lv | StartOf lv ->
{ lvalues with addr = HCESet.add (HCE.of_lval lv) lvalues.addr }
- | AlignOfE e | SizeOfE e ->
+ | AlignOfE (e,_) | SizeOfE (e,_) ->
(* The lvalues appearing in [e] are not read, and must all be in addr. *)
let new_lvalues = gather e empty_lvalues in
let new_addr = HCESet.union new_lvalues.read new_lvalues.addr in
diff --git a/src/plugins/eva/domains/hcexprs.mli b/src/plugins/eva/domains/hcexprs.mli
index 99d375fbd7049cfe349c86f1fb3db1bdcc750135..b22664907a460f02b79fcb079548a864902f8533 100644
--- a/src/plugins/eva/domains/hcexprs.mli
+++ b/src/plugins/eva/domains/hcexprs.mli
@@ -22,9 +22,7 @@
(** Hash-consed expressions and lvalues. *)
-open Cil_types
-
-type unhashconsed_exprs = private E of exp | LV of lval
+type unhashconsed_exprs = private E of Evast.exp | LV of Evast.lval
(** lvalues are never stored under a constructor [E], only [LV] *)
(** Raised when the replacement of an lvalue in an expression is impossible. *)
@@ -48,18 +46,18 @@ module HCE: sig
(** Conversions between type [t] and Cil lvalues and expressions. *)
- val of_lval: lval -> t
- val of_exp: exp -> t
+ val of_lval: Evast.lval -> t
+ val of_exp: Evast.exp -> t
val get: t -> unhashconsed_exprs
- val to_exp: t -> exp
- val to_lval: t -> lval option
+ val to_exp: t -> Evast.exp
+ val to_lval: t -> Evast.lval option
val is_lval: t -> bool
- val type_of: t -> typ
+ val type_of: t -> Cil_types.typ
(** Replaces all occurrences of the lvalue [late] by the expression [heir].
@raise NonExchangeable if the replacement is not feasible. *)
- val replace: kill_type -> late:lval -> heir:exp -> t -> t
+ val replace: kill_type -> late:Evast.lval -> heir:Evast.exp -> t -> t
end
@@ -84,7 +82,7 @@ val empty_lvalues: lvalues
removed. This function only computes the first lvalues of the expression,
and does not go through the lvalues (for the expression t[i]+1, only the
lvalue t[i] is returned). *)
-val syntactic_lvalues: Cil_types.exp -> lvalues
+val syntactic_lvalues: Evast.exp -> lvalues
(** Maps from symbolic expressions to their memory dependencies, expressed as a
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index db4680480a4b074883a7880ed930c2a71a9c64b7..65b07d9a9203b05f4c7c970b638e8e6b703eb527 100644
--- a/src/plugins/eva/domains/inout_domain.ml
+++ b/src/plugins/eva/domains/inout_domain.ml
@@ -162,7 +162,7 @@ module Transfer = struct
in [e] into locations. Nothing is written, the memory locations
present in [e] are read. *)
let effects_assume to_z e =
- let inputs = Eva_utils.zone_of_expr to_z e in
+ let inputs = Evast_utils.zone_of_exp to_z e in
{
over_outputs = Zone.bottom;
over_inputs = inputs;
@@ -173,8 +173,8 @@ module Transfer = struct
(* Effects of an assigment [lv = e]. [to_z] converts the lvalues present
in [lv] and [e] into locations. *)
let effects_assign to_z lv e =
- let inputs_e = Eva_utils.zone_of_expr to_z e in
- let inputs_lv = Eva_utils.indirect_zone_of_lval to_z lv.Eval.lval in
+ let inputs_e = Evast_utils.zone_of_exp to_z e in
+ let inputs_lv = Evast_utils.indirect_zone_of_lval to_z lv.Eval.lval in
let inputs = Zone.join inputs_e inputs_lv in
let outputs =
Precise_locs.enumerate_valid_bits Locations.Write lv.Eval.lloc
diff --git a/src/plugins/eva/domains/multidim/abstract_memory.ml b/src/plugins/eva/domains/multidim/abstract_memory.ml
index dbfe3bca992620573b8bb2e92a9c5c192ab7ec6c..ff77bb78a8fcb1cde0bf1bd9c5d5b23a4e270df2 100644
--- a/src/plugins/eva/domains/multidim/abstract_memory.ml
+++ b/src/plugins/eva/domains/multidim/abstract_memory.ml
@@ -157,7 +157,7 @@ end
type size = Integer.t
type side = Left | Right
-type oracle = Cil_types.exp -> Int_val.t
+type oracle = Evast.exp -> Int_val.t
type bioracle = side -> oracle
module type ProtoMemory =
@@ -190,5 +190,5 @@ sig
val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
t -> t
val add_segmentation_bounds : oracle:oracle -> typ:Cil_types.typ ->
- Cil_types.exp list -> t -> t
+ Evast.exp list -> t -> t
end
diff --git a/src/plugins/eva/domains/multidim/abstract_memory.mli b/src/plugins/eva/domains/multidim/abstract_memory.mli
index 3c14012af265875e4812a5db79d73d96f91f33b9..7b32e7e9636699b25a013950076ba081a9619f99 100644
--- a/src/plugins/eva/domains/multidim/abstract_memory.mli
+++ b/src/plugins/eva/domains/multidim/abstract_memory.mli
@@ -62,7 +62,7 @@ type size = Integer.t
(* Oracles for memory abstraction *)
type side = Left | Right
-type oracle = Cil_types.exp -> Int_val.t
+type oracle = Evast.exp -> Int_val.t
type bioracle = side -> oracle
(* Early stage of memory abstraction building *)
@@ -96,5 +96,5 @@ sig
val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
t -> t
val add_segmentation_bounds : oracle:oracle -> typ:Cil_types.typ ->
- Cil_types.exp list -> t -> t
+ Evast.exp list -> t -> t
end
diff --git a/src/plugins/eva/domains/multidim/abstract_offset.ml b/src/plugins/eva/domains/multidim/abstract_offset.ml
index 3821f6aaaa1bd6fcf7734261284d4c2fc85ff63c..193ca1a689b3f707387daf3e27e381669b1738e7 100644
--- a/src/plugins/eva/domains/multidim/abstract_offset.ml
+++ b/src/plugins/eva/domains/multidim/abstract_offset.ml
@@ -25,7 +25,7 @@ open Top.Operators
type t =
| NoOffset of Cil_types.typ
- | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * t
+ | Index of Evast.exp option * Int_val.t * Cil_types.typ * t
| Field of Cil_types.fieldinfo * t
let rec pretty fmt = function
@@ -37,7 +37,7 @@ let rec pretty fmt = function
pretty s
| Index (Some e, i, _t, s) ->
Format.fprintf fmt "[%a∈%a]%a"
- Cil_printer.pp_exp e
+ Evast_printer.pp_exp e
Int_val.pretty i
pretty s
@@ -59,14 +59,12 @@ let add_index oracle base exp =
Field (fi, sub')
| Index (e, i, t, (NoOffset _ as sub)) ->
let idx' = Int_val.add i (oracle exp) in
- let loc = Cil_datatype.Location.unknown in
let e = match e with (* If i is singleton, we can use this as the index expression *)
| None when Int_val.is_singleton i ->
- let loc = Cil_datatype.Location.unknown in
- Some (Cil.kinteger64 ~loc (Int_val.project_int i))
+ Some (Evast_builder.integer (Int_val.project_int i))
| e -> e
in
- let e' = Option.map (Fun.flip (Cil.mkBinOp ~loc Cil_types.PlusA) exp) e in
+ let e' = Option.map (Fun.flip (Evast_builder.add) exp) e in
(* TODO: is idx inside bounds ? *)
`Value (Index (e', idx', t, sub))
| Index (e, i, t, sub) ->
@@ -87,7 +85,7 @@ let rec join o1 o2 =
| Index (e1, i1, t, sub1), Index (e2, i2, t', sub2)
when Bit_utils.type_compatible t t' ->
let e = match e1, e2 with
- | Some e1, Some e2 when Cil_datatype.ExpStructEq.equal e1 e2 ->
+ | Some e1, Some e2 when Evast_datatype.Exp.equal e1 e2 ->
Some e1 (* keep expression only when equivalent from both offsets *)
| _ -> None
in
@@ -118,20 +116,20 @@ let assert_valid_index idx size =
let of_var_address vi =
NoOffset vi.Cil_types.vtype
-let rec of_cil_offset oracle base_typ = function
- | Cil_types.NoOffset -> `Value (NoOffset base_typ)
+let rec of_evast_offset (oracle : Evast.exp -> Int_val.t) base_typ = function
+ | Evast.NoOffset -> `Value (NoOffset base_typ)
| Field (fi, sub) ->
if Cil.typeHasQualifier "volatile" fi.ftype then
`Top
else
- let+ sub' = of_cil_offset oracle fi.ftype sub in
+ let+ sub' = of_evast_offset oracle fi.ftype sub in
Field (fi, sub')
| Index (exp, sub) ->
match Cil.unrollType base_typ with
| TArray (elem_typ, array_size, _) ->
let idx = oracle exp in
let+ () = assert_valid_index idx array_size
- and+ sub' = of_cil_offset oracle elem_typ sub in
+ and+ sub' = of_evast_offset oracle elem_typ sub in
Index (Some exp, idx, elem_typ, sub')
| _ -> assert false
@@ -248,7 +246,7 @@ let references =
| NoOffset _ -> acc
| Field (_, sub) | Index (None, _, _, sub) -> aux acc sub
| Index (Some e, _, _, sub) ->
- let r = Cil.extract_varinfos_from_exp e in
+ let r = Evast_utils.vars_in_exp e in
let acc = Cil_datatype.Varinfo.Set.union r acc in
aux acc sub
in
diff --git a/src/plugins/eva/domains/multidim/abstract_offset.mli b/src/plugins/eva/domains/multidim/abstract_offset.mli
index c8e44eeee4c76556cde12ca160facdcdbf17d55b..6608c1c1726ef5478a3107bc0430f7bbfe115d49 100644
--- a/src/plugins/eva/domains/multidim/abstract_offset.mli
+++ b/src/plugins/eva/domains/multidim/abstract_offset.mli
@@ -24,14 +24,14 @@ open Lattice_bounds
type t =
| NoOffset of Cil_types.typ
- | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * t
+ | Index of Evast.exp option * Int_val.t * Cil_types.typ * t
| Field of Cil_types.fieldinfo * t
val pretty : Format.formatter -> t -> unit
val of_var_address : Cil_types.varinfo -> t
-val of_cil_offset : (Cil_types.exp -> Int_val.t) ->
- Cil_types.typ -> Cil_types.offset -> t or_top
+val of_evast_offset : (Evast.exp -> Int_val.t) ->
+ Cil_types.typ -> Evast.offset -> t or_top
val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t or_top
val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t or_top
@@ -40,4 +40,4 @@ val references : t -> Cil_datatype.Varinfo.Set.t (* variables referenced in the
val append : t -> t -> t (* Does not check that the appened offset fits *)
val join : t -> t -> t or_top
-val add_index : (Cil_types.exp -> Int_val.t) -> t -> Cil_types.exp -> t or_top
+val add_index : (Evast.exp -> Int_val.t) -> t -> Evast.exp -> t or_top
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index c34c84acc994dd8348aba9af923a7058a7d03efb..0564edd184ee19aebe8dfe82c6c84b7d7b7ed334 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
open Lattice_bounds
@@ -175,19 +174,20 @@ struct
let of_var (vi : Cil_types.varinfo) : t =
Map.singleton (Base.of_varinfo vi) (`Value (Offset.of_var_address vi))
- let of_lval oracle ((host,offset) as lval : Cil_types.lval) : t or_top =
+ let of_lval oracle (lval : lval) : t or_top =
+ let (host,offset) = lval.node in
let oracle' = convert_oracle oracle in
- let base_typ = Cil.typeOfLhost host in
+ let base_typ = Evast_typing.type_of_lhost host in
let offset =
- if Cil.typeHasQualifier "volatile" (Cil.typeOfLval lval) then
+ if Evast_utils.lval_contains_volatile lval then
`Top
else
- Offset.of_cil_offset oracle' base_typ offset in
+ Offset.of_evast_offset oracle' base_typ offset in
match host with
| Var vi ->
`Value (Map.singleton (Base.of_varinfo vi) offset)
| Mem exp ->
- let exp, index = match exp.enode with
+ let exp, index = match exp.node with
| BinOp (PlusPI, e1, e2, _typ) ->
e1, Some e2
| _ -> exp, None
@@ -197,7 +197,7 @@ struct
match Base.typeof base with
| None -> `Top
| Some base_typ ->
- let typ = Cil.typeOf_pointed (Cil.typeOf exp) in
+ let typ = Cil.typeOf_pointed exp.typ in
let* base_offset = Offset.of_ival ~base_typ ~typ ival in
let* base_offset = match index with
| None -> `Value (base_offset)
@@ -217,7 +217,7 @@ struct
let of_term_lval env ((lhost, offset) as lval) =
let+ vi = match lhost with
- | TVar ({lv_origin=Some vi}) -> `Value (vi)
+ | Cil_types.TVar ({lv_origin=Some vi}) -> `Value (vi)
| TResult _ -> Top.of_option env.Abstract_domain.result
| _ -> `Top
in
@@ -225,7 +225,7 @@ struct
let offset' = Offset.of_term_offset vi.vtype offset in
Map.singleton base' offset', Cil.typeOfTermLval lval
- let of_term env t =
+ let of_term env (t : Cil_types.term) =
match t.term_node with
| TLval term_lval -> of_term_lval env term_lval
| _ -> `Top
@@ -413,18 +413,19 @@ struct
state referees
let update_var_references ~oracle (dst : Cil_types.varinfo)
- (src : Cil_types.exp option) (base_map,tracked : t) =
+ (src : Evast.exp option) (base_map,tracked : t) =
let incr = Option.bind src (fun expr ->
- match expr.Cil_types.enode with
- | BinOp ((PlusA|PlusPI), { enode=Lval (Var vi', NoOffset) }, exp, _typ)
- when Cil_datatype.Varinfo.equal dst vi' ->
- Cil.constFoldToInt exp
- | BinOp ((PlusA|PlusPI), exp, { enode=Lval (Var vi', NoOffset)}, _typ)
- when Cil_datatype.Varinfo.equal dst vi' ->
- Cil.constFoldToInt exp
- | BinOp ((MinusA|MinusPI), { enode=Lval (Var vi', NoOffset) }, exp, _typ)
- when Cil_datatype.Varinfo.equal dst vi' ->
- Option.map Integer.neg (Cil.constFoldToInt exp)
+ let is_dst (exp : Evast.exp) = match exp.node with
+ | Lval { node = Var v, NoOffset } -> Cil_datatype.Varinfo.equal dst v
+ | _ -> false
+ in
+ match expr.node with
+ | BinOp ((PlusA|PlusPI), e1, e2, _typ) when is_dst e1 ->
+ Evast_utils.fold_to_integer e2
+ | BinOp ((PlusA|PlusPI), e1, e2, _typ) when is_dst e2 ->
+ Evast_utils.fold_to_integer e1
+ | BinOp ((MinusA|MinusPI), e1, e2, _typ) when is_dst e1 ->
+ Option.map Integer.neg (Evast_utils.fold_to_integer e2)
| _ -> None)
in
(* [oracle] must be the oracle before the (non-invertible)
@@ -453,7 +454,7 @@ struct
base_map, tracked
let update_references ~oracle (dst : mdlocation)
- (src : Cil_types.exp option) (state : t) =
+ (src : Evast.exp option) (state : t) =
let remove_references b state =
match Base.to_varinfo b with
| exception Base.Not_a_C_variable -> state (* only references to variables are kept *)
@@ -484,11 +485,11 @@ struct
let oracle = convert_oracle oracle in
read (Memory.get ~oracle) Value_or_Uninitialized.join state src
- let mk_oracle (state : state) : Cil_types.exp -> value =
+ let mk_oracle (state : state) : Evast.exp -> value =
(* Until Eva gives access to good oracles, we use this poor stupid oracle
instead *)
- let rec oracle exp =
- match exp.enode with
+ let rec oracle (exp : Evast.exp) =
+ match exp.node with
| Lval lval ->
begin match Location.of_lval oracle lval with
| `Top -> Value.top
@@ -509,15 +510,15 @@ struct
Value.forward_binop_int ~typ (oracle e1) op (oracle e2)
| CastE (typ, e) ->
let scalar_type t = Option.get (Eval_typ.classify_as_scalar t) in
- let src_type = scalar_type (Cil.typeOf e)
+ let src_type = scalar_type e.typ
and dst_type = scalar_type typ in
Value.forward_cast ~src_type ~dst_type (oracle e)
| _ ->
Self.fatal
"This type of array index expression is not supported: %a"
- Cil_printer.pp_exp exp
+ Evast_printer.pp_exp exp
in
- fun exp -> oracle (Cil.constFold true exp)
+ fun exp -> oracle (Evast_utils.const_fold exp)
let mk_bioracle s1 s2 =
let oracle_left = mk_oracle s1
@@ -687,7 +688,9 @@ struct
| `Value v ->
Value_or_Uninitialized.get_v_normalized v >>-: (fun v -> v, None),
if Value_or_Uninitialized.is_initialized v
- then Alarmset.(set (Alarms.Uninitialized lv) True all)
+ then
+ let origin = Evast_utils.to_cil_lval lv in
+ Alarmset.(set (Alarms.Uninitialized origin) True all)
else Alarmset.all
else
`Value (Value.top, None), Alarmset.all
@@ -695,7 +698,7 @@ struct
(* Eva Transfer *)
- let valuation_to_oracle state valuation : Cil_types.exp -> value = fun exp ->
+ let valuation_to_oracle state valuation : Evast.exp -> value = fun exp ->
let multidim_oracle = mk_oracle state in
match valuation.Abstract_domain.find exp with
| `Top -> multidim_oracle exp
@@ -705,8 +708,8 @@ struct
let assume_exp valuation expr record state' =
let* state = state' in
let oracle = valuation_to_oracle state valuation in
- match expr.enode with
- | Lval lv when Cil.isScalarType (Cil.typeOfLval lv) ->
+ match (expr : Evast.exp).node with
+ | Lval lv when Cil.isScalarType lv.typ ->
let value = Value_or_Uninitialized.from_flagged record.value in
if not (Value.is_topint (Value_or_Uninitialized.get_v value)) then
match Location.of_lval oracle lv with
@@ -768,7 +771,7 @@ struct
let oracle = valuation_to_oracle state valuation in
let bind state arg =
state >>-:
- assign' ~oracle ~value:arg.avalue (Cil.var arg.formal) (Some arg.concrete)
+ assign' ~oracle ~value:arg.avalue (Evast_builder.var arg.formal) (Some arg.concrete)
in
List.fold_left bind (`Value state) call.arguments
@@ -779,10 +782,11 @@ struct
let args = List.map (fun arg -> arg.avalue) call.arguments in
let+ assigned_result = f args in
let oracle = mk_oracle post in
- assign' ~oracle ~value:assigned_result (Cil.var return) None post
+ let dst = Evast_builder.var return in
+ assign' ~oracle ~value:assigned_result dst None post
let show_expr valuation state fmt expr =
- match expr.enode with
+ match (expr : Evast.exp).node with
| Lval lval | StartOf lval ->
let oracle = valuation_to_oracle state valuation in
begin match Location.of_lval oracle lval with
@@ -820,7 +824,7 @@ struct
erase ~oracle ~weak:true state dst b
let reduce_by_papp env li _labels args positive state =
- match li.l_var_info.lv_name, args with
+ match li.Cil_types.l_var_info.lv_name, args with
| "\\are_finite", [arg] ->
begin match Location.of_term env arg with
| `Top -> `Value state (* can't resolve location, ignore *)
@@ -837,7 +841,7 @@ struct
let reduce_by_predicate env state predicate truth =
let rec reduce predicate truth state =
- match truth, predicate.pred_content with
+ match truth, predicate.Cil_types.pred_content with
| true, Pand (p1,p2) | false, Por (p1,p2) ->
state |> reduce p1 truth >>- reduce p2 truth
| _,Papp (li, labels, args) ->
@@ -847,12 +851,13 @@ struct
reduce predicate truth state
let interpret_acsl_extension extension _env state =
- match extension.ext_name with
+ match extension.Cil_types.ext_name with
| "array_partition" ->
let annotation = Eva_annotations.read_array_segmentation extension in
let vi,offset,bounds = annotation in
(* Update the segmentation *)
- let lval = Cil_types.Var vi, offset in
+ let bounds = List.map Evast_builder.translate_exp bounds in
+ let lval = Evast_builder.translate_lval (Var vi, offset) in
let oracle = mk_oracle state in
begin match Location.of_lval oracle lval with
| `Top -> state
@@ -864,7 +869,7 @@ struct
let state = write update state loc in
(* Update the references *)
let add acc e =
- let r = Cil.extract_varinfos_from_exp e in
+ let r = Evast_utils.vars_in_exp e in
(Cil_datatype.Varinfo.Set.to_seq r |> List.of_seq) @ acc
in
let references = List.fold_left add [] bounds in
@@ -900,7 +905,7 @@ struct
erase ~oracle state dst d
let initialize_variable_using_type _kind vi state =
- let lval = Cil.var vi in
+ let lval = Evast_builder.var vi in
let oracle = mk_oracle state in
match Location.of_lval oracle lval with
| `Top -> top
diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml
index 677366d0a3045bbbe39af0bf30c31e156c8629a9..3b24bf46366fb2669358c01646599e943fa74b7e 100644
--- a/src/plugins/eva/domains/multidim/segmentation.ml
+++ b/src/plugins/eva/domains/multidim/segmentation.ml
@@ -103,15 +103,15 @@ struct
module Var = Cil_datatype.Varinfo
module Exp =
struct
- include Cil_datatype.ExpStructEq
+ include Evast_datatype.Exp
let equal e1 e2 =
if e1 == e2 then true else equal e1 e2
end
type t =
| Const of Integer.t
- | Exp of Cil_types.exp * Integer.t (* x + c *)
- | Ptroffset of Cil_types.exp * Cil_types.offset * Integer.t (* (x - &b.offset) + c *)
+ | Exp of Evast.exp * Integer.t (* x + c *)
+ | Ptroffset of Evast.exp * Cil_types.offset * Integer.t (* (x - &b.offset) + c *)
let pretty fmt : t -> unit = function
| Const i -> Integer.pretty fmt i
@@ -153,12 +153,12 @@ struct
exception NonLinear
(* Find a coefficient before vi in exp *)
- let rec linearity vi exp =
- match exp.Cil_types.enode with
+ let rec linearity vi (exp : Evast.exp) =
+ match exp.node with
| Const _
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
| AddrOf _ | StartOf _ -> Integer.zero
- | Lval (Var vi', NoOffset) ->
+ | Lval {node = Var vi', NoOffset} ->
if Var.equal vi' vi
then Integer.one
else Integer.zero
@@ -183,21 +183,21 @@ struct
(* Check that the linearity of any variable is not hidden into a mem access *)
ignore (linearity Var.dummy exp)
- let of_exp exp =
+ let of_exp (exp : Evast.exp) =
check_support exp;
(* Normalizes x + c, c + x and x - c *)
- match Cil.constFoldToInt exp with
+ match Evast_utils.fold_to_integer exp with
| Some i -> Const i
| None ->
- match exp.Cil_types.enode with
+ match exp.node with
| BinOp ((PlusA|PlusPI), e1, e2, _typ) ->
- begin match Cil.constFoldToInt e1, Cil.constFoldToInt e2 with
+ begin match Evast_utils.(fold_to_integer e1, fold_to_integer e2) with
| None, Some i -> Exp (e1, i)
| Some i, None -> Exp (e2, i)
| _ -> Exp (exp, Integer.zero)
end
| BinOp ((MinusA|MinusPI), e1, e2, _typ) ->
- begin match Cil.constFoldToInt e2 with
+ begin match Evast_utils.fold_to_integer e2 with
| Some i -> Exp (e1, Integer.neg i)
| None -> Exp (exp, Integer.zero)
end
diff --git a/src/plugins/eva/domains/multidim/segmentation.mli b/src/plugins/eva/domains/multidim/segmentation.mli
index 39398f924e05fbb8c0ab17e923d824d0fa674105..6caad373072e0cdfee5b9cca915953dabfd9244c 100644
--- a/src/plugins/eva/domains/multidim/segmentation.mli
+++ b/src/plugins/eva/domains/multidim/segmentation.mli
@@ -34,7 +34,7 @@ module Bound :
sig
type t
exception UnsupportedBoundExpression
- val of_exp : Cil_types.exp -> t
+ val of_exp : Evast.exp -> t
val of_integer : Integer.t -> t
val succ : t -> t
end
diff --git a/src/plugins/eva/domains/multidim/typed_memory.mli b/src/plugins/eva/domains/multidim/typed_memory.mli
index 2044654bd3248cb29b305df7b969464ae2290713..4c6f64331a9612a7611c765b31d979459b9b6df9 100644
--- a/src/plugins/eva/domains/multidim/typed_memory.mli
+++ b/src/plugins/eva/domains/multidim/typed_memory.mli
@@ -121,5 +121,5 @@ sig
(* Update the array segmentation at the given offset so the given bound
expressions appear in the segmentation *)
val segmentation_hint : oracle:oracle ->
- t -> location -> Cil_types.exp list -> t
+ t -> location -> Evast.exp list -> t
end
diff --git a/src/plugins/eva/domains/numerors/numerors_value.ml b/src/plugins/eva/domains/numerors/numerors_value.ml
index 41380d779b7f4a475eb6dbe88c05ae52412594ac..37551cf346b6183bd9495ca23b0fe5796a863ef5 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.ml
+++ b/src/plugins/eva/domains/numerors/numerors_value.ml
@@ -20,8 +20,8 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
+open Evast
open Numerors_utils
module I = Numerors_interval
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 33be2920a29172dabe0ebf5c32eec98d07df2b46..500b474bb92acbb0b9f96f33f262193f007db6a8 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -20,8 +20,8 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
+open Evast
(* If [true], checks invariants of the states created by most functions. *)
let debug = false
@@ -61,19 +61,19 @@ type dependencies = Deps.t = {
indirect: Locations.Zone.t;
}
-type evaluator = Cil_types.exp -> Cvalue.V.t or_top
+type evaluator = exp -> Cvalue.V.t or_top
(* Abstract interface for the variables used by the octagons. *)
module type Variable = sig
include Datatype.S_with_collections
(* Creates a variable from a lvalue. *)
val make_lval: lval -> t
- val make_int: varinfo -> t
- val make_startof: varinfo -> t
+ val make_int: Cil_types.varinfo -> t
+ val make_startof: Cil_types.varinfo -> t
val kind: t -> kind (* The kind of the variable: integer or float. *)
val lval: t -> lval option (* The CIL lval corresponding to the variable. *)
val id: t -> int (* Unique id, needed to use variables as hptmap keys. *)
- val deps: eval_loc:(Cil_types.lval -> Precise_locs.precise_location) ->
+ val deps: eval_loc:(lval -> Precise_locs.precise_location) ->
t -> dependencies
end
@@ -83,9 +83,9 @@ module Variable : Variable = struct
module HCE = Hcexprs.HCE
type var =
- | Var of varinfo
- | Int of varinfo
- | StartOf of varinfo
+ | Var of Cil_types.varinfo
+ | Int of Cil_types.varinfo
+ | StartOf of Cil_types.varinfo
| Lval of HCE.t
type tt = var * int
@@ -125,9 +125,10 @@ module Variable : Variable = struct
let make var = var, make_id var
- let make_lval = function
- | Cil_types.Var vi, NoOffset -> make (Var vi)
- | lval -> make (Lval (HCE.of_lval lval))
+ let make_lval (lval : lval) =
+ match lval.node with
+ | Var vi, NoOffset -> make (Var vi)
+ | _ -> make (Lval (HCE.of_lval lval))
let make_int vi = make (Int vi)
let make_startof vi = make (StartOf vi)
@@ -140,7 +141,7 @@ module Variable : Variable = struct
let lval (var, _) =
match var with
- | Var vi -> Some (Cil_types.Var vi, NoOffset)
+ | Var vi -> Some (Evast_builder.var vi)
| Lval lval -> HCE.to_lval lval
| Int _ | StartOf _ -> None
@@ -154,7 +155,7 @@ module Variable : Variable = struct
| StartOf _ ->
{ data = Locations.Zone.bottom ; indirect = Locations.Zone.bottom }
| Lval lval ->
- Eva_utils.deps_of_lval eval_loc (Option.get (HCE.to_lval lval))
+ Evast_utils.deps_of_lval eval_loc (Option.get (HCE.to_lval lval))
end
module VarSet =
@@ -267,7 +268,7 @@ let _pretty_octagon fmt octagon =
request to the environment may return a new or an existing variable.
The abstract domain chooses which expressions are worth being represented
by a variable; the environment may return [None] otherwise. *)
-type environment = Cil_types.exp -> (Variable.t * Ival.t) option
+type environment = exp -> (Variable.t * Ival.t) option
(* Transforms Cil expressions into mathematical octagons.
Use Ival.t to evaluate expressions. *)
@@ -332,7 +333,7 @@ module Rewriting = struct
where [v1] and [v2] are the intervals for [e1] and [e2], and [typ] is
the type of [e1]. Returns the empty list otherwise. *)
let apply_binop f (eval : evaluator) typ e1 op e2 =
- let kind = typ_kind (Cil.typeOf e1) in
+ let kind = typ_kind e1.typ in
let v1 = eval e1 in
let v2 = eval e2 in
if Cil.isPointerType typ
@@ -358,7 +359,7 @@ module Rewriting = struct
match env expr with
| Some (var, ival) -> [ { var; sign = true; coeff = Ival.neg_int ival } ]
| None ->
- match expr.enode with
+ match expr.node with
| UnOp (Neg, e, typ) ->
let* v = project_ival (eval e) in
if may_overflow typ (Arith.neg v)
@@ -396,10 +397,10 @@ module Rewriting = struct
apply_binop rewrite_binop eval typ e1 op e2
| CastE (typ, e) ->
- if Cil.(isIntegralType typ && isIntegralType (typeOf e)) then
+ if Cil.(isIntegralType typ && isIntegralType e.typ) then
let* v = project_ival (eval e) in
if may_overflow ~cast:true typ v then [] else rewrite eval env e
- else if Cil.(isPointerType typ && isPointerType (typeOf e)) then
+ else if Cil.(isPointerType typ && isPointerType e.typ) then
rewrite eval env e
else
[]
@@ -408,7 +409,7 @@ module Rewriting = struct
(* Rewrites the operation [e1 ± e2] into equivalent octagons ±(X±Y-value). *)
let rewrite_binop (eval : evaluator) (env : environment) e1 binop e2 =
- let kind = typ_kind (Cil.typeOf e1) in
+ let kind = typ_kind e1.typ in
let vars1 = rewrite eval env e1 in
let vars2 = rewrite eval env e2 in
let vars2 = if binop = Sub then List.map neg vars2 else vars2 in
@@ -430,18 +431,18 @@ module Rewriting = struct
(* Returns the range of the expression X-Y when the comparison X#Y holds. *)
let comparison_range =
- let open Abstract_interp.Comp in
function
- | Lt -> Ival.inject_range None (Some Integer.minus_one)
+ | Evast.Lt -> Ival.inject_range None (Some Integer.minus_one)
| Gt -> Ival.inject_range (Some Integer.one) None
| Le -> Ival.inject_range None (Some Integer.zero)
| Ge -> Ival.inject_range (Some Integer.zero) None
| Eq -> Ival.zero
| Ne -> Ival.top
+ | _ -> assert false
(* Transforms the constraint [expr] ∈ [ival] into a list of octagonal
constraints. *)
- let make_octagons evaluate env expr ival =
+ let make_octagons evaluate env (expr : Evast.exp) ival =
let make_octagons_from_binop kind e1 op e2 ival =
(* equivalent octagonal forms ±(X±Y-v) for [e1 op e2]. *)
let rewritings = rewrite_binop evaluate env e1 op e2 in
@@ -453,23 +454,23 @@ module Rewriting = struct
in
List.map make_octagon rewritings
in
- match expr.enode with
+ match expr.node with
| BinOp (PlusA | MinusA | PlusPI | MinusPI | MinusPP as binop, e1, e2, typ) ->
let op = operation_of_binop binop in
let make_octagons typ _ _ = make_octagons_from_binop typ e1 op e2 ival in
apply_binop make_octagons evaluate typ e1 op e2
| BinOp ((Lt | Gt | Le | Ge | Eq | Ne as binop), e1, e2, _typ) ->
- let typ = Cil.typeOf e1 in
- if not (Cil.isIntegralOrPointerType typ)
+ if not (Cil.isIntegralOrPointerType e1.typ)
|| (Ival.contains_zero ival && Ival.contains_non_zero ival)
then []
else
- let comp = Eva_utils.conv_comp binop in
let comp =
- if Ival.is_zero ival then Abstract_interp.Comp.inv comp else comp
+ if Ival.is_zero ival
+ then Evast_utils.invert_relation binop
+ else binop
in
let range = comparison_range comp in
- make_octagons_from_binop (typ_kind typ) e1 Sub e2 range
+ make_octagons_from_binop (typ_kind e1.typ) e1 Sub e2 range
| _ -> []
let overflow_alarms typ expr ival =
@@ -483,7 +484,8 @@ module Rewriting = struct
let aux has_better_bound bound bound_kind alarms =
if Ival.is_bottom ival || has_better_bound ival ival_range >= 0
then
- let alarm = Alarms.Overflow (overflow, expr, bound, bound_kind) in
+ let cil_expr = Evast_utils.to_cil_exp expr in
+ let alarm = Alarms.Overflow (overflow, cil_expr, bound, bound_kind) in
Alarmset.set alarm Alarmset.True alarms
else alarms
in
@@ -497,7 +499,8 @@ module Rewriting = struct
(* Evaluates the Cil expression [expr], by rewriting it into octagonal
constraints using [evaluate_expr] to evaluate sub-expressions, and
then using [evaluate_octagon] to evaluate the octagons. *)
- let evaluate_through_octagons (eval : evaluator) evaluate_octagon env expr =
+ let evaluate_through_octagons (eval : evaluator) evaluate_octagon env
+ (expr : Evast.exp) =
let evaluate_octagon acc (sign, octagon) =
match evaluate_octagon octagon with
| None -> acc
@@ -509,13 +512,13 @@ module Rewriting = struct
List.fold_left evaluate_octagon Ival.top octagons
in
let default = Ival.top, Alarmset.all in
- match expr.enode with
+ match expr.node with
| BinOp ((PlusA | MinusA as binop), e1, e2, typ) ->
let op = if binop = PlusA then Add else Sub in
let octagons = rewrite_binop eval env e1 op e2 in
let ival = evaluate_octagons octagons in
if Ival.(equal top ival) then default else
- let kind = typ_kind (Cil.typeOf e1) in
+ let kind = typ_kind e1.typ in
let ival2 =
match
project_ival (eval e1), project_ival (eval e2)
@@ -528,11 +531,10 @@ module Rewriting = struct
then default
else ival, overflow_alarms typ expr ival
| BinOp ((Lt | Gt | Le | Ge | Eq as binop), e1, e2, _typ)
- when Cil.isIntegralOrPointerType (Cil.typeOf e1) ->
- let comp = Eva_utils.conv_comp binop in
+ when Cil.isIntegralOrPointerType e1.typ ->
(* Evaluate [e1 - e2] and compare the resulting interval to the interval
for which the comparison [e1 # e2] holds. *)
- let range = comparison_range comp in
+ let range = comparison_range binop in
let octagons = rewrite_binop eval env e1 Sub e2 in
let ival = evaluate_octagons octagons in
if Ival.is_included ival range then Ival.one, Alarmset.all
@@ -1264,7 +1266,7 @@ module State = struct
let rec offset_to_coeff (eval : evaluator) base_type offset =
let open Lattice_bounds.Top.Operators in
match offset with
- | Cil_types.NoOffset -> `Value (Ival.zero)
+ | NoOffset -> `Value (Ival.zero)
| Field (fi, sub) ->
let* sub_coeff = offset_to_coeff eval fi.ftype sub in
begin try
@@ -1295,21 +1297,21 @@ module State = struct
Top.fold ~top:false Cvalue.V.cardinal_zero_or_one
in
fun exp ->
- match exp.enode with
+ match exp.node with
| Lval lval
- when Cil.isIntegralOrPointerType (Cil.typeOfLval lval)
- && not (Eval_typ.lval_contains_volatile lval)
+ when Cil.isIntegralOrPointerType lval.typ
+ && not (Evast_utils.lval_contains_volatile lval)
&& not (is_singleton (eval exp)) ->
Some (Variable.make_lval lval, Ival.zero)
- | CastE (typ, { enode = Lval (Var vi, NoOffset) })
+ | CastE (typ, { node = Lval { node = Var vi, NoOffset } })
when Cil.isIntegralType typ
&& Cil.isFloatingType vi.vtype
&& not (Cil.typeHasQualifier "volatile" vi.vtype)
&& not (is_singleton (eval exp)) ->
Some (Variable.make_int vi, Ival.zero)
- | StartOf (Var vi, offset) | AddrOf (Var vi, offset) ->
+ | StartOf { node = Var vi, offset } | AddrOf { node = Var vi, offset } ->
let var = Variable.make_startof vi in
let* coeff = offset_to_coeff eval vi.vtype offset in
Some (var, coeff)
@@ -1655,8 +1657,9 @@ module Domain = struct
let extract_lval ~oracle:_ _context _t _lval _typ _loc = top_value
let reduce_further state expr value =
- match expr.enode with
- | Lval lval when Cil.(isIntegralOrPointerType (typeOfLval lval)) ->
+ match expr.node with
+ | Lval lval
+ when Cil.(isIntegralOrPointerType lval.typ) ->
begin
try
let x_ival = Cvalue.V.project_ival value in
@@ -1679,8 +1682,7 @@ module Domain = struct
in
let y_ival = Ival.narrow y_ival1 y_ival2 in
if Ival.(equal top y_ival) then acc else
- let y_enode = Lval lval in
- let y_expr = Cil.new_exp ~loc:expr.eloc y_enode in
+ let y_expr = Evast_builder.lval lval in
let y_cvalue = Cvalue.V.inject_ival y_ival in
(y_expr, y_cvalue) :: acc
in
@@ -1716,9 +1718,9 @@ module Domain = struct
if not infer_intervals
then state
else
- match expr.enode with
- | Lval lval when Cil.(isIntegralType (typeOfLval lval))
- && not (Eval_typ.lval_contains_volatile lval) ->
+ match expr.node with
+ | Lval lval when Cil.(isIntegralType lval.typ)
+ && not (Evast_utils.lval_contains_volatile lval) ->
let var = Variable.make_lval lval in
let deps = Deps.add var (eval_deps var) state.deps in
let intervals = Intervals.add var ival state.intervals in
@@ -1784,8 +1786,7 @@ module Domain = struct
with Not_found -> State.remove state variable
in
let state = assign_interval eval_deps variable assigned state in
- let enode = Lval lvalue in
- let left_expr = Cil.new_exp ~loc:expr.eloc enode in
+ let left_expr = Evast_builder.lval lvalue in
(* On the assignment X = E; if X-E can be rewritten as ±(X±Y-v),
then the octagonal constraint [X±Y ∈ v] holds. *)
let octagons = Rewriting.rewrite_binop eval_exp env left_expr Sub expr in
@@ -1799,9 +1800,9 @@ module Domain = struct
state >>-: check "precise assign"
let assign kinstr left_value expr assigned valuation state =
- if kinstr <> Kglobal
+ if kinstr <> Cil_types.Kglobal
&& Cil.isIntegralOrPointerType left_value.ltyp
- && not (Eval_typ.lval_contains_volatile left_value.lval)
+ && not (Evast_utils.lval_contains_volatile left_value.lval)
then assign_variable left_value.lval expr assigned valuation state
else
let written_loc = Precise_locs.imprecise_location left_value.lloc in
@@ -1833,7 +1834,7 @@ module Domain = struct
`Value (start_recursive_call recursion state)
| None ->
let assign_formal state { formal; concrete; avalue } =
- let lval = (Var formal, NoOffset) in
+ let lval = Evast_builder.var formal in
if Cil.isIntegralOrPointerType formal.vtype
then state >>- assign_variable lval concrete avalue valuation
else state
diff --git a/src/plugins/eva/domains/printer_domain.ml b/src/plugins/eva/domains/printer_domain.ml
index ff8e8cfaef064e43f2f5783b5e9573c8abaa41df..3dc5d69b088a416e15114c8320c2bb09dcf56c98 100644
--- a/src/plugins/eva/domains/printer_domain.ml
+++ b/src/plugins/eva/domains/printer_domain.ml
@@ -71,19 +71,19 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
let pp_arg fmt arg =
Format.fprintf fmt "%a = %a"
- Printer.pp_exp arg.concrete
+ Evast_printer.pp_exp arg.concrete
pp_cvalue_assigned arg.avalue
let assign _kinstr loc exp cvalue_assigned _valuation state =
feedback "assign %a with %a = %a"
- Printer.pp_lval loc.lval
- Printer.pp_exp exp
+ Evast_printer.pp_lval loc.lval
+ Evast_printer.pp_exp exp
pp_cvalue_assigned cvalue_assigned;
`Value state
let assume _stmt exp truth _valuation state =
feedback "assume %a is %b"
- Printer.pp_exp exp
+ Evast_printer.pp_exp exp
truth;
`Value state
@@ -112,7 +112,7 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
let initialize_variable lval ~initialized:_ init state =
feedback "initialize_variable %a with %a"
- Printer.pp_lval lval
+ Evast_printer.pp_lval lval
pp_init_val init;
state
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index d2c81be458b371f7f320c566d0d77ae53d6b2088..f094fd433cd20977aa509763866066ae3a4b4df7 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
type 'value builtin = 'value list -> 'value or_bottom
@@ -230,7 +229,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
location with the result of the evaluation of [exp]. Both the value and
the location are found in the [valuation]. *)
let assume_exp valuation expr record state =
- match expr.enode with
+ match (expr : Evast.exp).node with
| Lval lv -> begin
match valuation.Abstract_domain.find_loc lv with
| `Top -> state
@@ -309,7 +308,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
bind_loc return_loc return.vtype (`Value result) post
let show_expr valuation state fmt expr =
- match expr.enode with
+ match (expr : Evast.exp).node with
| Lval lval ->
begin
match valuation.Abstract_domain.find_loc lval with
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 0719ce81c897066c3a6302ec334dc68d85ae911a..4a6fe9d0095f7c3702a106dbcd34de7d835a3745 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -20,8 +20,8 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
+open Evast
open Locations
let dkey = Self.register_category "d-symblocs"
@@ -115,9 +115,10 @@ end
Otherwise, the value should be inferred by the cvalue domain, or can be
precisely computed from values inferred by the cvalue domain. *)
let interesting_exp get_locs get_val e =
- let is_comp = function Eq | Ne | Le | Ge | Lt | Gt -> true | _ -> false in
+ let is_comp = function Eq | Ne | Le | Ge | Lt | Gt -> true | _ -> false
+ in
let rec has_lvalue e =
- match e.enode with
+ match e.node with
| Lval _ ->
not (Cvalue.V.cardinal_zero_or_one (get_val e))
| CastE (_, e) | UnOp (_, e, _) ->
@@ -128,7 +129,7 @@ let interesting_exp get_locs get_val e =
| StartOf _ | AddrOf _ ->
false
in
- match e.enode with
+ match e.node with
| Lval lv ->
not (Precise_locs.cardinal_zero_or_one (get_locs lv))
| BinOp (op, e1, e2,_) ->
@@ -138,24 +139,19 @@ let interesting_exp get_locs get_val e =
false
(* Locals and formals syntactically present in an expression or lvalue *)
-let rec vars_lv (h, o) = Base.Set.union (vars_host h) (vars_offset o)
-and vars_exp (e: exp) = match e.enode with
- | Const _ | SizeOf _ | AlignOf _ | SizeOfStr _ ->
- Base.Set.empty
- | AddrOf lv | StartOf lv | Lval lv ->
- vars_lv lv
- | SizeOfE e | AlignOfE e | CastE (_,e) | UnOp (_,e,_) ->
- vars_exp e
- | BinOp (_,e1,e2,_) -> Base.Set.union (vars_exp e1) (vars_exp e2)
-and vars_host = function
- | Var vi ->
- (* Global variables never go out of scope, no need to track them *)
- if vi.vglob then Base.Set.empty else Base.(Set.singleton (of_varinfo vi))
- | Mem e -> vars_exp e
-and vars_offset = function
- | NoOffset -> Base.Set.empty
- | Field (_, o) -> vars_offset o
- | Index (e, o) -> Base.Set.union (vars_exp e) (vars_offset o)
+let vars_to_bases vi_set =
+ vi_set
+ |> Cil_datatype.Varinfo.Set.to_seq
+ (* Global variables never go out of scope, no need to track them *)
+ |> Seq.filter (fun vi -> not vi.Cil_types.vglob)
+ |> Seq.map Base.of_varinfo
+ |> Base.Set.of_seq
+
+let vars_lv lv =
+ vars_to_bases (Evast_utils.vars_in_lval lv)
+
+let vars_exp (e: exp) =
+ vars_to_bases (Evast_utils.vars_in_exp e)
(* Legacy names *)
module B2K = K.BaseToHCESet
@@ -373,12 +369,12 @@ module Memory = struct
(* Add the the mapping [lv --> v] to [state] when possible.
[get_z] is a function that computes dependencies. *)
let add_lv state get_z lv v =
- if Eval_typ.lval_contains_volatile lv then
+ if Evast_utils.lval_contains_volatile lv then
state
else
let k = K.HCE.of_lval lv in
let z_lv = Precise_locs.enumerate_valid_bits Locations.Read (get_z lv) in
- let z_lv_indirect = Eva_utils.indirect_zone_of_lval get_z lv in
+ let z_lv_indirect = Evast_utils.indirect_zone_of_lval get_z lv in
if Locations.Zone.intersects z_lv z_lv_indirect then
(* The location of [lv] intersects with the zones needed to compute
itself, the equality would not hold. *)
@@ -390,11 +386,11 @@ module Memory = struct
(* Add the mapping [e --> v] to [state] when possible and useful.
[get_z] is a function that computes dependencies. *)
let add_exp state get_z e v =
- if Eval_typ.expr_contains_volatile e then
+ if Evast_utils.exp_contains_volatile e then
state
else
let k = K.HCE.of_exp e in
- let z = Eva_utils.zone_of_expr get_z e in
+ let z = Evast_utils.zone_of_exp get_z e in
add_key k v z state
let find k state =
@@ -491,7 +487,7 @@ module D : Abstract_domain.Leaf
| `Value loc -> loc.Eval.loc
in
if Precise_locs.(equal_loc loc_top r) then
- Self.fatal "Unknown location for %a" Printer.pp_lval lv
+ Self.fatal "Unknown location for %a" Evast_printer.pp_lval lv
else r
let get_val valuation = fun lv ->
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index d20a13adf8ab68cf6ef4181c5b0d7bfe835b93a0..d55ffdc6050a3980b93cdcaee1130cc17bdfc22d 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -186,7 +186,7 @@ module TransferTaint = struct
- its indirect dependencies, i.e. the memory zone its location depends on;
- whether its location is a singleton. *)
let compute_zones lval to_loc =
- match lval with
+ match (lval : Evast.lval).node with
| Var vi, NoOffset ->
(* Special case for direct access to variable: do not use [to_loc] here,
as it will fail for the formal parameters of calls. *)
@@ -199,13 +199,13 @@ module TransferTaint = struct
let loc = Precise_locs.imprecise_location ploc in
Locations.enumerate_valid_bits Write loc
in
- let lv_indirect_zone = Eva_utils.indirect_zone_of_lval to_loc lval in
+ let lv_indirect_zone = Evast_utils.indirect_zone_of_lval to_loc lval in
lv_zone, lv_indirect_zone, singleton
(* Propagates data- and control-taints for an assignement [lval = exp]. *)
let assign_aux lval exp to_loc state =
let lv_zone, lv_indirect_zone, singleton = compute_zones lval to_loc in
- let exp_zone = Eva_utils.zone_of_expr to_loc exp in
+ let exp_zone = Evast_utils.zone_of_exp to_loc exp in
(* [lv] becomes data-tainted if a memory location on which the value of
[exp] depends on is data-tainted. *)
let data_tainted = Zone.intersects state.locs_data exp_zone in
@@ -246,7 +246,7 @@ module TransferTaint = struct
let state = filter_active_tainted_assumes stmt state in
(* Add [stmt] as assume statement in [state] as soon as [exp] is tainted. *)
let to_loc = loc_of_lval valuation in
- let exp_zone = Eva_utils.zone_of_expr to_loc exp in
+ let exp_zone = Evast_utils.zone_of_exp to_loc exp in
let state =
if not state.dependent_call && LatticeTaint.intersects state exp_zone
then { state with assume_stmts = Stmt.Set.add stmt state.assume_stmts; }
@@ -265,7 +265,7 @@ module TransferTaint = struct
let to_loc = loc_of_lval valuation in
List.fold_left
(fun s { Eval.concrete; formal; _ } ->
- assign_aux (Cil.var formal) concrete to_loc s)
+ assign_aux (Evast_builder.var formal) concrete to_loc s)
state
call.Eval.arguments
in
@@ -279,7 +279,7 @@ module TransferTaint = struct
let show_expr valuation state fmt exp =
let to_loc = loc_of_lval valuation in
- let exp_zone = Eva_utils.zone_of_expr to_loc exp in
+ let exp_zone = Evast_utils.zone_of_exp to_loc exp in
Format.fprintf fmt "%B" (LatticeTaint.intersects state exp_zone)
end
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index 53eb03a0032d1c1111ba34594b3f3ea6f61b3aaf..b427c440de0ef78378b1a53e0db11a23d48f8b2b 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1102,11 +1102,14 @@ module D = struct
let log_category = Self.register_category "d-traces"
let assign ki lv e _v _valuation state =
- let trans = Assign (ki, lv.Eval.lval, lv.Eval.ltyp, e) in
+ let cil_lval = Evast_utils.to_cil_lval lv.Eval.lval in
+ let cil_exp = Evast_utils.to_cil_exp e in
+ let trans = Assign (ki, cil_lval, lv.Eval.ltyp, cil_exp) in
`Value (Traces.add_trans state trans)
let assume stmt e pos _valuation state =
- let trans = Assume (stmt, e, pos) in
+ let cil_exp = Evast_utils.to_cil_exp e in
+ let trans = Assume (stmt, cil_exp, pos) in
`Value (Traces.add_trans state trans)
let start_call stmt call _recursion _valuation state =
@@ -1121,7 +1124,8 @@ module D = struct
Traces.add_trans state
(Assign (Kstmt stmt, Cil.var arg.Eval.formal,
arg.Eval.formal.Cil_types.vtype,
- arg.Eval.concrete))) state call.Eval.arguments in
+ Evast_utils.to_cil_exp arg.Eval.concrete)))
+ state call.Eval.arguments in
`Value state
else
(* enter the scope of the dumb result variable *)
@@ -1129,7 +1133,11 @@ module D = struct
let state = match var with
| Some var -> Traces.add_trans state (EnterScope (kf, [var]))
| None -> state in
- let exps = List.map (fun arg -> arg.Eval.concrete) call.Eval.arguments in
+ let exps =
+ List.map
+ (fun arg -> Evast_utils.to_cil_exp arg.Eval.concrete)
+ call.Eval.arguments
+ in
let state = Traces.add_trans state
(CallDeclared (call.Eval.kf, exps, Option.map Cil.var var))
in `Value {state with call_declared_function = true}
@@ -1150,7 +1158,7 @@ module D = struct
let empty () = Traces.empty
let initialize_variable lv _ ~initialized:_ _ state =
- Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Printer.pp_lval lv ))
+ Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Evast_printer.pp_lval lv ))
let initialize_variable_using_type var_kind varinfo state =
let kind_str =
match var_kind with
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index 81ac423fadbe17a0c3e6b94375473d531ba40f3d..43fa00b6e1bbe863d58b31117b057ad799f946c8 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -24,6 +24,7 @@
open Cil_types
open Eval
+open Evast
(* The forward evaluation of an expression [e] gives a value to each subterm
of [e], from its variables to the root expression [e]. It also computes the
@@ -128,7 +129,9 @@ let rec may_be_reduced_offset = function
| Field (_, offset) -> may_be_reduced_offset offset
| Index _ -> true
-let may_be_reduced_lval (host, offset) = match host with
+let may_be_reduced_lval lval =
+ let (host, offset) = lval.node in
+ match host with
| Var _ -> may_be_reduced_offset offset
| Mem _ -> true
@@ -166,22 +169,10 @@ let rec signed_counterpart typ =
| TPtr _ -> signed_counterpart Cil.(theMachine.upointType)
| _ -> assert false
-module MemoDowncastConvertedAlarm =
- State_builder.Hashtbl
- (Cil_datatype.Exp.Hashtbl)
- (Cil_datatype.Exp)
- (struct
- let name = "Value.Evaluation.MemoDowncastConvertedAlarm"
- let size = 16
- let dependencies = [ Ast.self ]
- end)
-let exp_alarm_signed_converted_downcast =
- MemoDowncastConvertedAlarm.memo
- (fun exp ->
- let src_typ = Cil.typeOf exp in
- let signed_typ = signed_counterpart src_typ in
- let signed_exp = Cil.new_exp ~loc:exp.eloc (CastE (signed_typ, exp)) in
- signed_exp)
+let exp_alarm_signed_converted_downcast exp =
+ let src_typ = exp.typ in
+ let signed_typ = signed_counterpart src_typ in
+ Evast_builder.(cast signed_typ exp)
let return t = `Value t, Alarmset.none
@@ -256,8 +247,8 @@ module Make
type origin = Domain.origin
type loc = Loc.location
- module ECache = Cil_datatype.ExpStructEq.Map
- module LCache = Cil_datatype.LvalStructEq.Map
+ module ECache = Evast_datatype.Exp.Map
+ module LCache = Evast_datatype.Lval.Map
(* Imperative cache for the evaluation:
all intermediate results of an evaluation are cached here.
@@ -402,7 +393,10 @@ module Make
| _ -> false
let truncate_bound overflow_kind bound bound_kind expr value =
- let alarm () = Alarms.Overflow (overflow_kind, expr, bound, bound_kind) in
+ let alarm () =
+ let cil_expr = Evast_utils.to_cil_exp expr in (* The expression does not necessary come from the original program *)
+ Alarms.Overflow (overflow_kind, cil_expr, bound, bound_kind)
+ in
let bound = Abstract_value.Int bound in
let truth = Value.assume_bounded bound_kind bound value in
interpret_truth ~alarm value truth
@@ -438,9 +432,10 @@ module Make
let restrict_float ?(reduce=false) ~assume_finite expr fkind value =
let truth = Value.assume_not_nan ~assume_finite fkind value in
let alarm () =
+ let cil_expr = Evast_utils.to_cil_exp expr in
if assume_finite
- then Alarms.Is_nan_or_infinite (expr, fkind)
- else Alarms.Is_nan (expr, fkind)
+ then Alarms.Is_nan_or_infinite (cil_expr, fkind)
+ else Alarms.Is_nan (cil_expr, fkind)
in
if reduce
then reduce_by_truth ~alarm (expr, value) truth
@@ -458,7 +453,8 @@ module Make
let+ value =
if Kernel.InvalidPointer.get () then
let truth = Value.assume_pointer value in
- let alarm () = Alarms.Invalid_pointer expr in
+ let cil_expr = Evast_utils.to_cil_exp expr in
+ let alarm () = Alarms.Invalid_pointer cil_expr in
interpret_truth ~alarm value truth
else return value
in
@@ -489,17 +485,17 @@ module Make
let* value, origin = res in
match typ with
| TFloat (fkind, _) ->
- let expr = Eva_utils.lval_to_exp lval in
+ let expr = Evast_builder.lval lval in
let+ new_value = remove_special_float expr fkind value in
new_value, origin
| TInt (IBool, _) when Kernel.InvalidBool.get () ->
let one = Abstract_value.Int Integer.one in
let truth = Value.assume_bounded Alarms.Upper_bound one value in
- let alarm () = Alarms.Invalid_bool lval in
+ let alarm () = Alarms.Invalid_bool (Evast_utils.to_cil_lval lval) in
let+ new_value = interpret_truth ~alarm value truth in
new_value, origin
| TPtr _ ->
- let expr = Eva_utils.lval_to_exp lval in
+ let expr = Evast_builder.lval lval in
let+ new_value = assume_pointer context expr value in
new_value, origin
| _ -> res
@@ -510,7 +506,9 @@ module Make
let size = Cil.bitsSizeOf typ in
let size_int = Abstract_value.Int (Integer.of_int (size - 1)) in
let zero_int = Abstract_value.Int Integer.zero in
- let alarm () = Alarms.Invalid_shift (expr, Some size) in
+ let alarm () =
+ Alarms.Invalid_shift (Evast_utils.to_cil_exp expr, Some size)
+ in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int value in
let* value = reduce_by_truth ~alarm (expr, value) truth in
let truth = Value.assume_bounded Alarms.Upper_bound size_int value in
@@ -524,7 +522,9 @@ module Make
if warn_negative && Bit_utils.is_signed_int_enum_pointer typ then
(* Cannot shift a negative value *)
let zero_int = Abstract_value.Int Integer.zero in
- let alarm () = Alarms.Invalid_shift (e1, None) in
+ let alarm () =
+ Alarms.Invalid_shift (Evast_utils.to_cil_exp e1, None)
+ in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int v1 in
let+ v1 = reduce_by_truth ~alarm (e1, v1) truth in
v1, v2
@@ -535,10 +535,13 @@ module Make
let open Evaluated.Operators in
let size_int = Abstract_value.Int (Integer.pred size) in
let zero_int = Abstract_value.Int Integer.zero in
- let alarm () = Alarms.Index_out_of_bound (index_expr, None) in
+ let alarm_index_expr () = Evast_utils.to_cil_exp index_expr in
+ let alarm () = Alarms.Index_out_of_bound (alarm_index_expr (), None) in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int value in
let* value = reduce_by_truth ~alarm (index_expr, value) truth in
- let alarm () = Alarms.Index_out_of_bound (index_expr, Some size_expr) in
+ let alarm () =
+ Alarms.Index_out_of_bound (alarm_index_expr (), Some size_expr)
+ in
let truth = Value.assume_bounded Alarms.Upper_bound size_int value in
reduce_by_truth ~alarm (index_expr, value) truth
@@ -548,7 +551,7 @@ module Make
match op with
| Div | Mod ->
let truth = Value.assume_non_zero v2 in
- let alarm () = Alarms.Division_by_zero e2 in
+ let alarm () = Alarms.Division_by_zero (Evast_utils.to_cil_exp e2) in
let+ v2 = reduce_by_truth ~alarm arg2 truth in
v1, v2
| Shiftrt ->
@@ -560,7 +563,11 @@ module Make
| MinusPP when Parameters.WarnPointerSubstraction.get () ->
let kind = Abstract_value.Subtraction in
let truth = Value.assume_comparable kind v1 v2 in
- let alarm () = Alarms.Differing_blocks (e1, e2) in
+ let alarm () =
+ Alarms.Differing_blocks (
+ Evast_utils.to_cil_exp e1,
+ Evast_utils.to_cil_exp e2)
+ in
let arg1 = Some e1, v1 in
reduce_by_double_truth ~alarm arg1 arg2 truth
| _ -> return (v1, v2)
@@ -576,7 +583,11 @@ module Make
let forward_comparison ~compute typ kind (e1, v1) (e2, v2) =
let truth = Value.assume_comparable kind v1 v2 in
- let alarm () = Alarms.Pointer_comparison (e1, e2) in
+ let alarm () =
+ Alarms.Pointer_comparison (
+ Option.map Evast_utils.to_cil_exp e1,
+ Evast_utils.to_cil_exp e2)
+ in
let propagate_all = propagate_all_pointer_comparison typ in
let args, alarms =
if warn_pointer_comparison typ then
@@ -603,19 +614,19 @@ module Make
let forward_binop context typ (e1, v1 as arg1) op arg2 =
let open Evaluated.Operators in
- let typ_e1 = Cil.unrollType (Cil.typeOf e1) in
+ let typ_e1 = Cil.unrollType e1.typ in
match comparison_kind op with
| Some kind ->
let compute v1 v2 = Value.forward_binop context typ_e1 op v1 v2 in
(* Detect zero expressions created by the evaluator *)
- let e1 = if Eva_utils.is_value_zero e1 then None else Some e1 in
+ let e1 = if Evast_utils.is_zero_ptr e1 then None else Some e1 in
forward_comparison ~compute typ_e1 kind (e1, v1) arg2
| None ->
let& v1, v2 = assume_valid_binop typ arg1 op arg2 in
Value.forward_binop context typ_e1 op v1 v2
let forward_unop context unop (e, v as arg) =
- let typ = Cil.unrollType (Cil.typeOf e) in
+ let typ = Cil.unrollType e.typ in
if unop = LNot then
let kind = Abstract_value.Equality in
let compute _ v = Value.forward_unop context typ unop v in
@@ -700,7 +711,8 @@ module Make
then prev_float (Fval.kind fkind) fbound
else fbound
in
- let alarm () = Alarms.Float_to_int (expr, bound, bound_kind) in
+ let cil_expr = Evast_utils.to_cil_exp expr in
+ let alarm () = Alarms.Float_to_int (cil_expr, bound, bound_kind) in
let bound = Abstract_value.Float (float_bound, fkind) in
let truth = Value.assume_bounded bound_kind bound value in
reduce_by_truth ~alarm (expr, value) truth
@@ -716,7 +728,7 @@ module Make
let forward_cast context ~dst expr value =
let open Evaluated.Operators in
- let src = Cil.typeOf expr in
+ let src = expr.typ in
match Eval_typ.(classify_as_scalar src, classify_as_scalar dst) with
| None, _ | _, None -> return value (* Unclear whether this happens. *)
| Some src_type, Some dst_type ->
@@ -821,7 +833,7 @@ module Make
and performs the narrowing with the abstractions computed by
[internal_forward_eval]. *)
and coop_forward_eval env expr =
- match expr.enode with
+ match expr.node with
| Lval lval -> eval_lval env lval
| BinOp _ | UnOp _ | CastE _ ->
let domain_query = make_domain_query Domain.extract_expr env in
@@ -868,7 +880,7 @@ module Make
let reduction = if Alarmset.is_empty a then Neither else Forward in
v, reduction, volatile
in
- match expr.enode with
+ match expr.node with
| Const constant -> internal_forward_eval_constant env expr constant
| Lval _lval -> assert false
@@ -903,16 +915,18 @@ module Make
in
compute_reduction v volatile
- | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
- match Cil.constFoldToInt expr with
- | Some v -> return (Value.inject_int (Cil.typeOf expr) v, Neither, false)
+ | SizeOf (_,s) | SizeOfE (_,s) | SizeOfStr (_,s)
+ | AlignOf (_,s) | AlignOfE (_,s) ->
+ match s with
+ | Some v -> return (Value.inject_int expr.typ v, Neither, false)
| _ -> return (Value.top_int, Neither, false)
and internal_forward_eval_constant env expr constant =
let open Evaluated.Operators in
let+ value =
match constant with
- | CEnum {eival = e} -> forward_eval env e
+ | CEnum (_, e) ->
+ forward_eval env e
| CReal (_f, fkind, _fstring) ->
let value = Value.constant env.context expr constant in
remove_special_float expr fkind value
@@ -965,10 +979,11 @@ module Make
let lval_to_loc = internal_lval_to_loc env ~for_writing ~reduction in
let* loc, typ, volatile = lval_to_loc lval in
if reduction then
- let bitfield = Cil.isBitfield lval in
+ let bitfield = Evast_utils.is_bitfield lval in
let truth = Loc.assume_valid_location ~for_writing ~bitfield loc in
let access = Alarms.(if for_writing then For_writing else For_reading) in
- let alarm () = Alarms.Memory_access (lval, access) in
+ let cil_lval = Evast_utils.to_cil_lval lval in
+ let alarm () = Alarms.Memory_access (cil_lval, access) in
let+ valid_loc = interpret_truth ~alarm loc truth in
let reduction = if Loc.equal_loc valid_loc loc then Neither else Forward in
valid_loc, typ, reduction, volatile
@@ -979,12 +994,13 @@ module Make
an offset, to obtain a location *)
and internal_lval_to_loc env ~for_writing ~reduction lval =
let open Evaluated.Operators in
- let host, offset = lval in
- let typ = Cil.typeOfLhost host in
+ let host, offset = lval.node in
+ let typ = Evast_typing.type_of_lhost host in
let evaluated = eval_offset env ~reduce_valid_index:reduction typ offset in
let* (offs, typ_offs, offset_volatile) = evaluated in
if for_writing && Eva_utils.is_const_write_invalid typ_offs then
- let alarm = Alarms.(Memory_access (lval, For_writing)) in
+ let cil_lval = Evast_utils.to_cil_lval lval in
+ let alarm = Alarms.(Memory_access (cil_lval, For_writing)) in
`Bottom, Alarmset.singleton ~status:Alarmset.False alarm
else
let+ loc, host_volatile = eval_host env typ_offs offs host in
@@ -1059,11 +1075,12 @@ module Make
- if it contains a sub-expression which is volatile (volatile_expr)
*)
let volatile = volatile_expr || Cil.typeHasQualifier "volatile" typ_lv in
+ let cil_lval = Evast_utils.to_cil_lval lval in
(* Find the value of the location, if not bottom. *)
let v, alarms = domain_query lval typ_lv loc in
- let alarms = close_dereference_alarms lval alarms in
+ let alarms = close_dereference_alarms cil_lval alarms in
if indeterminate then
- let record, alarms = indeterminate_copy lval v alarms in
+ let record, alarms = indeterminate_copy cil_lval v alarms in
`Value (record, Neither, volatile), alarms
else
let v, alarms = assume_valid_value env.context typ_lv lval (v, alarms) in
@@ -1246,7 +1263,7 @@ module Make
recursive_descent fuel context state expr
| Some (value, kind) ->
(* Otherwise, backward propagation to the subterms. *)
- match expr.enode with
+ match expr.node with
| Lval lval ->
begin
(* For a lvalue, we try to reduce its location according to the value;
@@ -1270,21 +1287,21 @@ module Make
(* Backward propagate the reduction [expr] = [value] to the subterms of the
compound expression [expr]. *)
and internal_backward fuel context state expr value =
- match expr.enode with
+ match expr.node with
| Lval _lv -> assert false
| UnOp (LNot, e, _) ->
- let cond = Eva_utils.normalize_as_cond e false in
+ let cond = Evast_builder.normalize_condition e false in
(* TODO: should we compute the meet with the result of the call to
Value.backward_unop? *)
backward_eval fuel context state cond (Some value)
| UnOp (op, e, _typ) ->
- let typ_arg = Cil.unrollType (Cil.typeOf e) in
+ let typ_arg = Cil.unrollType e.typ in
let* arg = find_val e in
let* v = Value.backward_unop context ~typ_arg op ~arg ~res:value in
backward_eval fuel context state e v
| BinOp (binop, e1, e2, typ) ->
let resulting_type = Cil.unrollType typ in
- let input_type = Cil.typeOf e1 in
+ let input_type = e1.typ in
let* left = find_val e1
and* right = find_val e2 in
let backward = Value.backward_binop context ~input_type ~resulting_type in
@@ -1294,7 +1311,7 @@ module Make
| CastE (typ, e) ->
begin
let dst_typ = Cil.unrollType typ in
- let src_typ = Cil.unrollType (Cil.typeOf e) in
+ let src_typ = Cil.unrollType e.typ in
let* src_val = find_val e in
let backward = Value.backward_cast context ~src_typ ~dst_typ in
let* v = backward ~src_val ~dst_val:value in
@@ -1303,7 +1320,7 @@ module Make
| _ -> `Value ()
and recursive_descent fuel context state expr =
- match expr.enode with
+ match expr.node with
| Lval lval -> backward_lval fuel context state lval
| UnOp (_, e, _)
| CastE (_, e) -> backward_eval fuel context state e None
@@ -1312,7 +1329,8 @@ module Make
backward_eval fuel context state e2 None
| _ -> `Value ()
- and recursive_descent_lval fuel context state (host, offset) =
+ and recursive_descent_lval fuel context state lval =
+ let (host, offset) = lval.node in
let* () = recursive_descent_host fuel context state host in
recursive_descent_offset fuel context state offset
@@ -1359,7 +1377,8 @@ module Make
then Some (loc, value)
else None
- and internal_backward_lval fuel context state location = function
+ and internal_backward_lval fuel context state location lval =
+ match lval.node with
| Var host, offset ->
let* loc_offset = Loc.backward_variable host location in
backward_offset fuel context state host.vtype offset loc_offset
@@ -1370,7 +1389,7 @@ module Make
backward_eval fuel context state expr (Some loc_value)
| _ ->
let reduce_valid_index = true in
- let typ_lval = Cil.typeOf_pointed (Cil.typeOf expr) in
+ let typ_lval = Cil.typeOf_pointed expr.typ in
let* env = fast_eval_environment state in
let eval = eval_offset env ~reduce_valid_index typ_lval offset in
let* loc_offset, _, _ = fst eval in
@@ -1427,7 +1446,7 @@ module Make
let* value = record.value.v in
let* () = recursive_descent state expr in
let new_value =
- match expr.enode with
+ match expr.node with
| Lval lval -> second_eval_lval state lval value
| _ ->
let* env = fast_eval_environment state in
@@ -1469,7 +1488,7 @@ module Make
else `Value value
and recursive_descent state expr =
- match expr.enode with
+ match expr.node with
| Lval lval -> recursive_descent_lval state lval
| UnOp (_, e, _)
| CastE (_, e) -> second_forward_eval state e
@@ -1478,7 +1497,8 @@ module Make
second_forward_eval state e2
| _ -> `Value ()
- and recursive_descent_lval state (host, offset) =
+ and recursive_descent_lval state lval =
+ let (host, offset) = lval.node in
let* () = recursive_descent_host state host in
recursive_descent_offset state offset
@@ -1522,7 +1542,7 @@ module Make
let copy_lvalue ?(valuation=Cache.empty) ?subdivnb state lval =
let open Evaluated.Operators in
- let expr = Eva_utils.lval_to_exp lval in
+ let expr = Evast_builder.lval lval in
let* env = root_environment ?subdivnb state, Alarmset.none in
try
let record, report = Cache.find' valuation expr in
@@ -1560,8 +1580,9 @@ module Make
(* If [for_writing] is true, the location of [lval] is reduced by removing
const bases. Use [for_writing:false] if const bases can be written
through a mutable field or an initializing function. *)
- let for_writing = for_writing && not (Cil.is_mutable_or_initialized lval) in
- let host, offset = lval in
+ let mutable_or_init = Evast_utils.(is_mutable lval || is_initialized lval) in
+ let for_writing = for_writing && not mutable_or_init in
+ let (host, offset) = lval.node in
let* valuation = evaluate_host valuation ?subdivnb state host in
let* valuation = evaluate_offsets valuation ?subdivnb state offset in
cache := valuation;
@@ -1576,7 +1597,7 @@ module Make
let reduce ?valuation:(valuation=Cache.empty) state expr positive =
let open Evaluated.Operators in
(* Generate [e == 0] *)
- let expr = Eva_utils.normalize_as_cond expr (not positive) in
+ let expr = Evast_builder.normalize_condition expr (not positive) in
cache := valuation;
(* Currently, no subdivisions are performed during the forward evaluation
in this function, which is used to evaluate the conditions of if(…)
@@ -1620,7 +1641,7 @@ module Make
else
Self.fatal ~current:true
"Function pointer evaluates to anything. function %a"
- Printer.pp_exp funcexp
+ Evast_printer.pp_exp funcexp
(* For pointer calls, we retro-propagate which function is being called
in the abstract state. This may be useful:
@@ -1631,15 +1652,14 @@ module Make
let backward_function_pointer valuation state expr kf =
(* Builds the expression [exp_f != &f], and assumes it is false. *)
let vi_f = Kernel_function.get_vi kf in
- let addr = Cil.mkAddrOfVi vi_f in
- let expr = Cil.mkBinOp ~loc:expr.eloc Ne expr addr in
+ let expr = Evast_builder.(ne expr (addr (var vi_f))) in
fst (reduce ~valuation state expr false)
let eval_function_exp ?subdivnb funcexp ?args state =
- match funcexp.enode with
- | Lval (Var vinfo, NoOffset) ->
+ match funcexp.node with
+ | Lval { node = (Var vinfo, NoOffset) } ->
`Value [Globals.Functions.get vinfo, Valuation.empty], Alarmset.none
- | Lval (Mem v, NoOffset) ->
+ | Lval { node = (Mem v, NoOffset) } ->
begin
let open Evaluated.Operators in
let* valuation, value = evaluate ?subdivnb state v in
@@ -1647,8 +1667,10 @@ module Make
match kfs with
| `Top -> top_function_pointer funcexp
| `Value kfs ->
- let typ = Cil.typeOf funcexp in
- let kfs, alarm' = Eval_typ.compatible_functions typ ?args kfs in
+ let args_types = Option.map (List.map (fun e -> e.typ)) args in
+ let kfs, alarm' =
+ Eval_typ.compatible_functions funcexp.typ ?args:args_types kfs
+ in
let reduce = backward_function_pointer valuation state v in
let process acc kf =
let res = reduce kf >>-: fun valuation -> kf, valuation in
@@ -1660,7 +1682,9 @@ module Make
else if alarm || alarm' then Alarmset.Unknown
else Alarmset.True
in
- let alarm = Alarms.Function_pointer (v, args) in
+ let cil_v = Evast_utils.to_cil_exp v in
+ let cil_args = Option.map (List.map (Evast_utils.to_cil_exp)) args in
+ let alarm = Alarms.Function_pointer (cil_v, cil_args) in
let alarms = Alarmset.singleton ~status alarm in
Bottom.bot_of_list list, alarms
end
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index 5dcd098943930ac6a881f473838176c6cb3df50a..a996a9922b129b1908a9e94cd8db6a0bd6235c16 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -24,13 +24,14 @@
open Cil_types
open Eval
+open Evast
module type S = sig
type state
val initial_state_with_formals :
lib_entry:bool -> kernel_function -> state or_bottom
val initialize_local_variable:
- stmt -> varinfo -> Cil_types.init -> state -> state or_bottom
+ stmt -> varinfo -> init -> state -> state or_bottom
end
type padding_initialization = [
@@ -106,7 +107,7 @@ module Make
(* Initializes an entire variable [vi], in particular padding bits,
according to [local] and [lib_entry] mode. *)
let initialize_var_padding ~local ~lib_entry vi state =
- let lval = Cil.var vi in
+ let lval = Evast_builder.var vi in
match padding_initialization ~local with
| `Uninitialized -> state
| `Initialized | `MaybeInitialized as i ->
@@ -127,37 +128,40 @@ module Make
(* Applies a single Cil initializer, using the standard transfer function on
assignments. Warns if the results is bottom. *)
- let apply_cil_single_initializer kinstr state lval expr =
+ let apply_evast_single_initializer ~source kinstr state lval expr =
match Transfer.assign state kinstr lval expr with
| `Bottom ->
if kinstr = Kglobal then
- Self.warning ~once:true ~source:(fst expr.eloc)
- "evaluation of initializer '%a' failed@." Printer.pp_exp expr;
+ Self.warning ~once:true ~source
+ "evaluation of initializer '%a' failed@." Evast_printer.pp_exp expr;
raise Initialization_failed
| `Value v -> v
(* Applies an initializer. If [top_volatile] is true, sets volatile locations
to top without applying the initializer. Otherwise, lets the standard
transfer function on assignments handle volatile locations. *)
- let rec apply_cil_initializer ~top_volatile kinstr lval init state =
- if top_volatile && Cil.typeHasQualifier "volatile" (Cil.typeOfLval lval)
+ let rec apply_evast_initializer ~top_volatile kinstr lval init state =
+ if top_volatile && Cil.typeHasQualifier "volatile" lval.typ
then initialize_top_volatile lval state
else
match init with
- | SingleInit exp -> apply_cil_single_initializer kinstr state lval exp
- | CompoundInit (typ, l) ->
- let doinit off init _typ state =
- let lval = Cil.addOffsetLval off lval in
- apply_cil_initializer ~top_volatile kinstr lval init state
+ | SingleInit (exp, loc) ->
+ let source = fst loc in
+ apply_evast_single_initializer ~source kinstr state lval exp
+ | CompoundInit (_typ, l) ->
+ let doinit state (off, init) =
+ let lval = Evast_builder.add_offset lval off in
+ apply_evast_initializer ~top_volatile kinstr lval init state
in
- Cil.foldLeftCompound ~implicit:false ~doinit ~ct:typ ~initl:l ~acc:state
+ List.fold_left doinit state l
(* Field by field initialization of a variable to zero, or top if volatile.
Very inefficient. *)
let initialize_var_zero_or_volatile kinstr vi state =
let loc = Cil_datatype.Location.unknown in
- let zero_init = Cil.makeZeroInit ~loc vi.vtype in
- apply_cil_initializer ~top_volatile:true kinstr (Cil.var vi) zero_init state
+ let init = Evast_builder.translate_init (Cil.makeZeroInit ~loc vi.vtype) in
+ let lval = Evast_builder.var vi in
+ apply_evast_initializer ~top_volatile:true kinstr lval init state
(* ----------------------- Non Lib-entry mode ----------------------------- *)
@@ -165,7 +169,7 @@ module Make
let initialize_var_not_lib_entry kinstr ~local vi init state =
ignore (warn_unknown_size vi);
let typ = vi.vtype in
- let lval = Cil.var vi in
+ let lval = Evast_builder.var vi in
let volatile_everywhere = Cil.typeHasQualifier "volatile" typ in
let state =
if volatile_everywhere && padding_initialization ~local = `Initialized
@@ -187,7 +191,7 @@ module Make
match init with
| None -> state
| Some init ->
- apply_cil_initializer ~top_volatile:false kinstr lval init state
+ apply_evast_initializer ~top_volatile:false kinstr lval init state
(* --------------------------- Lib-entry mode ----------------------------- *)
@@ -195,12 +199,16 @@ module Make
(* Special application of an initializer: only non-volatile lval with
attributes 'const' are initialized. *)
let rec apply_cil_const_initializer kinstr state lval = function
- | SingleInit exp ->
+ | Cil_types.SingleInit exp ->
let typ_lval = Cil.typeOfLval lval in
if Cil.typeHasQualifier "const" typ_lval &&
not (Cil.typeHasQualifier "volatile" typ_lval)
&& not (Cil.is_mutable_or_initialized lval)
- then apply_cil_single_initializer kinstr state lval exp
+ then
+ let lval = Evast_builder.translate_lval lval
+ and exp = Evast_builder.translate_exp exp
+ and source = fst exp.eloc in
+ apply_evast_single_initializer ~source kinstr state lval exp
else state
| CompoundInit (typ, l) ->
if Cil.typeHasQualifier "volatile" typ || not (Cil.isConstType typ)
@@ -219,13 +227,14 @@ module Make
if Cil.typeHasQualifier "const" vi.vtype && not (vi.vstorage = Extern)
&& not (Cil.typeHasAttributeMemoryBlock Cil.frama_c_mutable vi.vtype)
then (* Fully const base. Ignore -lib-entry altogether. *)
+ let init = Option.map Evast_builder.translate_init init in
initialize_var_not_lib_entry kinstr ~local:false vi init state
else
let unknown_size = warn_unknown_size vi in
let state =
if unknown_size then
(* the type is unknown, initialize everything to Top *)
- let lval = Cil.var vi in
+ let lval = Evast_builder.var vi in
let loc = lval_to_loc lval in
let v = Abstract_domain.Top in
Domain.initialize_variable lval loc ~initialized:true v state
@@ -320,8 +329,12 @@ module Make
let state = if vi.vsource then
let initialize =
if lib_entry || (vi.vstorage = Extern)
- then initialize_var_lib_entry
- else initialize_var_not_lib_entry ~local:false
+ then
+ initialize_var_lib_entry
+ else
+ fun ki vi init state ->
+ let init = Option.map Evast_builder.translate_init init in
+ initialize_var_not_lib_entry ki ~local:false vi init state
in
initialize Kglobal vi init.init state
else state
diff --git a/src/plugins/eva/engine/initialization.mli b/src/plugins/eva/engine/initialization.mli
index 761564adea6b7b838d743b2ea02ca551b39bb3d2..1fdfe47cdf94d8ba31c91512a274cfb6390ac9ae 100644
--- a/src/plugins/eva/engine/initialization.mli
+++ b/src/plugins/eva/engine/initialization.mli
@@ -22,7 +22,7 @@
(** Creation of the initial state of abstract domain. *)
-open Cil_types
+open Evast
open Lattice_bounds
module type S = sig
@@ -31,11 +31,11 @@ module type S = sig
(** Compute the initial state for an analysis (as in {!initial_state}),
but also bind the formal parameters of the function given as argument. *)
val initial_state_with_formals :
- lib_entry:bool -> kernel_function -> state or_bottom
+ lib_entry:bool -> Cil_types.kernel_function -> state or_bottom
(** Initializes a local variable in the current state. *)
val initialize_local_variable:
- stmt -> varinfo -> init -> state -> state or_bottom
+ Cil_types.stmt -> varinfo -> init -> state -> state or_bottom
end
module Make
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 211f101c4459ee53eb70367ddd9341a67b1218f6..ec006367e7678565bf0caa01f0526cff4139ed61 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -21,7 +21,8 @@
(**************************************************************************)
open Cil_types
-open Interpreted_automata
+open Evast
+open Eva_automata
open Lattice_bounds
open Bottom.Operators
@@ -125,7 +126,7 @@ module Make_Dataflow
(* --- Interpreted automata --- *)
- let automaton = get_automaton kf
+ let automaton = Eva_automata.get_automaton kf
let graph = automaton.graph
let control_point_count = G.nb_vertex graph
let transition_count = G.nb_edges graph
@@ -165,7 +166,7 @@ module Make_Dataflow
let current_ki = ref Kglobal
module VertexTable = struct
- include Interpreted_automata.Vertex.Hashtbl
+ include Eva_automata.Vertex.Hashtbl
let find_or_add (t : 'a t) (key : key) ~(default : unit -> 'a) : 'a =
try find t key
with Not_found ->
@@ -173,7 +174,7 @@ module Make_Dataflow
end
module EdgeTable = struct
- include Interpreted_automata.Edge.Hashtbl
+ include Eva_automata.Edge.Hashtbl
let find_or_add (t : 'a t) (key : key) ~(default : unit -> 'a) : 'a =
try find t key
with Not_found ->
@@ -201,7 +202,7 @@ module Make_Dataflow
VertexTable.find_or_add v_table v ~default:(default_vertex_store v)
let get_vertex_widening (v : vertex) : widening =
VertexTable.find_or_add w_table v ~default:(default_vertex_widening v)
- let get_edge_data (e : vertex edge) : tank =
+ let get_edge_data (e : edge) : tank =
EdgeTable.find_or_add e_table e ~default:default_edge_tank
let get_succ_tanks (v : vertex) : tank list =
List.map (fun (_,e,_) -> get_edge_data e) (G.succ_e graph v)
@@ -270,7 +271,7 @@ module Make_Dataflow
let positive = (kind = Then) in
lift' (fun s -> Transfer.assume s stmt exp positive)
- let transfer_assign (stmt : stmt) (dest : Cil_types.lval) (exp : exp)
+ let transfer_assign (stmt : stmt) (dest : lval) (exp : exp)
: transfer_function =
lift' (fun s -> Transfer.assign s (Kstmt stmt) dest exp)
@@ -300,33 +301,11 @@ module Make_Dataflow
(* Recombine callee partitioning keys with caller key *)
Partitioning.call_return ~caller:key result
- let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
- match instr with
- | Local_init (vi, AssignInit exp, _loc) ->
- let transfer state =
- Init.initialize_local_variable stmt vi exp state
- in
- lift' transfer
- | Local_init (vi, ConsInit (f, args, k), loc) ->
- let as_func dest callee args _loc (key, state) =
- transfer_call stmt dest callee args (key, state)
- in
- Cil.treat_constructor_as_func as_func vi f args k loc
- | Set (dest, exp, _loc) ->
- transfer_assign stmt dest exp
- | Call (dest, callee, args, _loc) ->
- transfer_call stmt dest callee args
- | Asm _ ->
- transfer_asm stmt
- | Skip _loc -> id
- | Code_annot (_,_loc) -> id (* already done in process_statement
- from the annotation table *)
-
let transfer_return (stmt : stmt) (return_exp : exp option)
: transfer_function =
(* Deconstruct return statement *)
let return_var = match return_exp with
- | Some {enode = Lval (Var v, NoOffset)} -> Some v
+ | Some {node = Lval {node = Var v, NoOffset}} -> Some v
| None -> None
| _ -> assert false (* Cil invariant *)
in
@@ -348,7 +327,7 @@ module Make_Dataflow
| None -> fun state -> [state]
| Some return_exp ->
let vi_ret = Option.get (Library_functions.get_retres_vi kf) in
- let return_lval = Var vi_ret, NoOffset in
+ let return_lval = Evast_builder.var vi_ret in
let kstmt = Kstmt stmt in
fun state ->
let kind = Abstract_domain.Result kf in
@@ -358,18 +337,27 @@ module Make_Dataflow
in
sequence (lift'' check_postconditions) (lift'' assign_retval)
- let transfer_transition (t : vertex transition) : transfer_function =
+ let transfer_transition (t : transition) : transfer_function =
match t with
| Skip -> id
| Return (return_exp,stmt) -> transfer_return stmt return_exp
| Guard (exp,kind,stmt) -> transfer_assume stmt exp kind
- | Instr (instr,stmt) -> transfer_instr stmt instr
+ | Init (vi, exp, stmt) ->
+ let transfer state =
+ Init.initialize_local_variable stmt vi exp state
+ in
+ lift' transfer
+ | Assign (dest, exp, stmt) ->
+ transfer_assign stmt dest exp
+ | Call (dest, callee, args, stmt) ->
+ transfer_call stmt dest callee args
+ | Asm (_,_,_,stmt) ->
+ transfer_asm stmt
| Enter (block) -> transfer_enter block
| Leave (block) when blocks_share_locals fundec.sbody block ->
(* The variables from the toplevel block will be removed by the caller *)
id
| Leave (block) -> transfer_leave block
- | Prop _ -> id (* Annotations are interpreted in [transfer_statement]. *)
let transfer_annotations (stmt : stmt) ~(record : bool)
: state -> state list =
@@ -397,6 +385,12 @@ module Make_Dataflow
(* Check unspecified sequences *)
match stmt.skind with
| UnspecifiedSequence seq when Kernel.UnspecifiedAccess.get () ->
+ let seq = List.map (fun (stmt, modified, writes, reads, refs) ->
+ stmt,
+ List.map Evast_builder.translate_lval modified,
+ List.map Evast_builder.translate_lval writes,
+ List.map Evast_builder.translate_lval reads,
+ refs) seq in
let check s =
Transfer.check_unspecified_sequence stmt s seq = `Value ()
in
@@ -407,7 +401,7 @@ module Make_Dataflow
(* --- Iteration strategy ---*)
let process_partitioning_transitions (v1 : vertex) (v2 : vertex)
- (transition : vertex transition) (flow : flow) : flow =
+ (transition : transition) (flow : flow) : flow =
(* Split return *)
let flow = match transition with
| Return (return_exp, _) -> Partitioning.split_return flow return_exp
@@ -426,9 +420,9 @@ module Make_Dataflow
Partitioning.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f
in
let loops_left, loops_entered =
- Interpreted_automata.get_wto_index_diff kf v1 v2
+ Eva_automata.wto_index_diff v1 v2
and loop_incr =
- Interpreted_automata.is_back_edge kf (v1,v2)
+ Eva_automata.is_back_edge (v1,v2)
in
let flow = List.fold_left leave_loop flow loops_left in
let flow = List.fold_left enter_loop flow loops_entered in
@@ -509,7 +503,7 @@ module Make_Dataflow
let sources = List.map process_source (G.pred_e graph v) in
(* Add initial source *)
let sources =
- if not (Interpreted_automata.Vertex.equal v automaton.entry_point)
+ if not (Eva_automata.Vertex.equal v automaton.entry_point)
then sources
else get_initial_flow () :: sources
in
@@ -611,10 +605,8 @@ module Make_Dataflow
let compute () : (key * state) list =
if interpreter_mode then
simulate automaton.entry_point (get_initial_flow ())
- else begin
- let wto = Interpreted_automata.get_wto kf in
- iterate_list wto
- end;
+ else
+ iterate_list automaton.wto;
if not !post_conditions then mark_postconds_as_true ();
let final_store = get_vertex_store automaton.return_point in
Partitioning.expanded final_store
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index f1c4e35e797a912ad6ecc5420e7ce75fee27ea8a..d485cceb90038141820e3ab8d0555a0668d49eb7 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -155,7 +155,7 @@ let make_recursion call depth =
let substitution = get_stack call.kf depth in
let add_if_copy acc argument =
match argument.avalue with
- | Copy ({ lval = Var vi, _ }, _) -> Varinfo.Set.add vi acc
+ | Copy ({ lval = { node = Var vi, _ } }, _) -> Varinfo.Set.add vi acc
| _ -> acc
in
let empty = Varinfo.Set.empty in
diff --git a/src/plugins/eva/engine/subdivided_evaluation.ml b/src/plugins/eva/engine/subdivided_evaluation.ml
index e4a15fdbfa44f8fc1f284c57ba4de2e36b6fb612..da6b0966ac90a90fb811e7a037565c4486f25b56 100644
--- a/src/plugins/eva/engine/subdivided_evaluation.ml
+++ b/src/plugins/eva/engine/subdivided_evaluation.ml
@@ -20,15 +20,14 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
let dkey = Self.register_category "nonlin"
(* ----------------- Occurrences of lvalues in expressions ------------------ *)
-module LvalMap = Cil_datatype.LvalStructEq.Map
-module LvalSet = Cil_datatype.LvalStructEq.Set
+module LvalMap = Evast_datatype.Lval.Map
+module LvalSet = Evast_datatype.Lval.Set
(* An expression [e] is non-linear on [x] if [x] appears multiple times in [e].
When evaluating such an expression, a disjunction over the possible values of
@@ -88,14 +87,14 @@ let union expr depth map1 map2 =
If a lvalue is bound to itself, then it appears only once in [expr].
Otherwise, we say that the expression is non linear on this lvalue. *)
let gather_non_linear expr =
- let rec compute depth expr =
- match expr.enode with
- | Lval (host, offset as lv) ->
+ let rec compute depth (expr : Evast.exp) =
+ match expr.node with
+ | Lval ({ node = host, offset } as lv) ->
let d = succ depth in
let map1 = compute_from_offset d expr offset in
let map2 = compute_from_host d host in
let map = union expr depth map1 map2 in
- if LvalMap.is_empty map && Cil.isArithmeticType (Cil.typeOfLval lv)
+ if LvalMap.is_empty map && Cil.isArithmeticType lv.typ
then LvalMap.singleton lv (expr, d, LvalSet.empty)
else map
| UnOp (_, e, _) | CastE (_, e) -> compute depth e
@@ -118,7 +117,7 @@ let gather_non_linear expr =
(* Map from subexpressions to the list of their non-linear lvalues. *)
module ExpMap = struct
- include Cil_datatype.ExpStructEq.Map
+ include Evast_datatype.Exp.Map
let add expr lv map =
try
let list = find expr map in
@@ -139,8 +138,8 @@ module DepthMap = struct
add depth expmap map
end
-let same lval expr = match expr.enode with
- | Lval lv -> Cil_datatype.LvalStructEq.equal lv lval
+let same lval (expr : Evast.exp) = match expr.node with
+ | Lval lv -> Evast_datatype.Lval.equal lv lval
| _ -> false
(* Converts a map from lvalues to expressions and depth into an association
@@ -156,12 +155,12 @@ let reverse_map map =
DepthMap.fold concat depthmap []
-module LvalList = Datatype.List (Cil_datatype.LvalStructEq)
-module NonLinear = Datatype.Pair (Cil_datatype.Exp) (LvalList)
+module LvalList = Datatype.List (Evast_datatype.Lval)
+module NonLinear = Datatype.Pair (Evast_datatype.Exp) (LvalList)
module NonLinears = Datatype.List (NonLinear)
module Non_linear_expressions =
- State_builder.Hashtbl (Cil_datatype.ExpStructEq.Hashtbl) (NonLinears)
+ State_builder.Hashtbl (Evast_datatype.Exp.Hashtbl) (NonLinears)
(struct
let name = "Value.Subdivided_evaluation.Non_linear_expressions"
let size = 16
@@ -180,8 +179,8 @@ let compute_non_linear expr =
List.iter
(fun (e, lval) ->
Self.result ~current:true ~once:true ~dkey
- "non-linear '%a', lv '%a'" Printer.pp_exp e
- (Pretty_utils.pp_list ~sep:", " Printer.pp_lval) lval)
+ "non-linear '%a', lv '%a'" Evast_printer.pp_exp e
+ (Pretty_utils.pp_list ~sep:", " Evast_printer.pp_lval) lval)
list;
Non_linear_expressions.replace expr list;
list
@@ -658,7 +657,7 @@ module Make
Clear.clear_englobing_exprs valuation ~expr ~subexpr:lv_info.lv_expr
in
let cleared_valuation = Hypotheses.fold clear variables valuation in
- let eq_equal_subexpr = Cil_datatype.ExpStructEq.equal expr subexpr in
+ let eq_equal_subexpr = Evast_datatype.Exp.equal expr subexpr in
(* Computes a disjunct from subvalues for [lvals]. *)
let compute subvalues =
(* Updates [variables] with their new [subvalues]. *)
@@ -708,7 +707,7 @@ module Make
(* Builds the information for an lvalue. *)
let get_info environment valuation lval =
- let lv_expr = Eva_utils.lval_to_exp lval in
+ let lv_expr = Evast_builder.lval lval in
(* Reevaluates the lvalue in the initial state, as its value could have
been reduced in the evaluation of the complete expression, and we cannot
omit the alarms for the removed values. *)
@@ -773,7 +772,7 @@ module Make
in
Self.result ~current:true ~once:true ~dkey
"subdividing on %a"
- (Pretty_utils.pp_list ~sep:", " Printer.pp_lval) lvals;
+ (Pretty_utils.pp_list ~sep:", " Evast_printer.pp_lval) lvals;
let subdivide =
subdivide_lvals environment valuation subdivnb lvals_info
in
@@ -849,10 +848,10 @@ module Make
(* Find locations on which it is interesting to proceed by case disjunction
to evaluate the expression: locations which are singletons (on which the
cvalue domain can reduce) and has an enumerable value. *)
- let rec get_influential_vars valuation exp acc =
- match exp.enode with
- | Lval (host, off as lval) ->
- if Cil.typeHasQualifier "volatile" (Cil.typeOfLval lval) then `Value acc
+ let rec get_influential_vars valuation (exp : Evast.exp) acc =
+ match exp.node with
+ | Lval ({ node = host, off } as lval) ->
+ if Cil.typeHasQualifier "volatile" lval.typ then `Value acc
else
Loc.to_value (find_loc valuation lval) >>- fun value ->
if Cvalue.V.cardinal_zero_or_one (get_cval value)
@@ -876,11 +875,11 @@ module Make
| CastE (_, exp) -> get_influential_vars valuation exp acc
| _ -> `Value acc
- and get_vars_host valuation host acc = match host with
+ and get_vars_host valuation (host : Evast.lhost) acc = match host with
| Var _v -> `Value acc
| Mem e -> get_influential_vars valuation e acc
- and get_vars_offset valuation offset acc = match offset with
+ and get_vars_offset valuation (offset : Evast.offset) acc = match offset with
| NoOffset -> `Value acc
| Field (_, off) -> get_vars_offset valuation off acc
| Index (ind, off) ->
diff --git a/src/plugins/eva/engine/subdivided_evaluation.mli b/src/plugins/eva/engine/subdivided_evaluation.mli
index a0fb79f594e37349401e516a37205eb864d49c09..198437485009d4e7af25717f182748ec658470b8 100644
--- a/src/plugins/eva/engine/subdivided_evaluation.mli
+++ b/src/plugins/eva/engine/subdivided_evaluation.mli
@@ -24,7 +24,6 @@
for expressions in which some l-values appear multiple times, proceed
by disjunction on their abstract value, in order to gain precision. *)
-open Cil_types
open Eval
module type Forward_Evaluation = sig
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 8579cfdd89ec56354ac1d078c3cde7dc93d31604..bb9502367c3da035f56a43406dae5659f39acfec 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -103,14 +103,13 @@ module DumpFileCounters =
module VarHashtbl = Cil_datatype.Varinfo.Hashtbl
-let substitution_visitor table = object
- inherit Visitor.frama_c_copy (Project.current ())
-
- method! vvrbl varinfo =
- match VarHashtbl.find_opt table varinfo with
- | None -> Cil.JustCopy
- | Some vi -> Cil.ChangeTo vi
-end
+let substitution_visitor table =
+ let rewrite_varinfo ~visitor:_ vi =
+ match VarHashtbl.find_opt table vi with
+ | None -> vi
+ | Some vi' -> vi'
+ in
+ { Evast_visitor.Rewrite.default with rewrite_varinfo }
module Make (Abstract: Abstractions.S_with_evaluation) = struct
@@ -163,17 +162,20 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let evaluate_and_check ?valuation ~subdivnb state expr =
let res = Eval.evaluate ?valuation ~subdivnb state expr in
- report_unreachability state res "the expression %a" Printer.pp_exp expr;
+ report_unreachability state res "the expression %a"
+ Evast_printer.pp_exp expr;
res
let lvaluate_and_check ?valuation ~subdivnb ~for_writing state lval =
let res = Eval.lvaluate ?valuation ~subdivnb ~for_writing state lval in
- report_unreachability state res "the lvalue %a" Printer.pp_lval lval;
+ report_unreachability state res "the lvalue %a"
+ Evast_printer.pp_lval lval;
res
let copy_lvalue_and_check ?valuation ~subdivnb state lval =
let res = Eval.copy_lvalue ?valuation ~subdivnb state lval in
- report_unreachability state res "the copy of %a" Printer.pp_lval lval;
+ report_unreachability state res "the copy of %a"
+ Evast_printer.pp_lval lval;
res
(* ------------------------------------------------------------------------ *)
@@ -205,10 +207,10 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Find a lvalue hidden under identity casts. This function correctly detects
bitfields (thanks to [need_cast]) and will never expose the underlying
field. *)
- let rec find_lval expr = match expr.enode with
+ let rec find_lval (expr : Evast.exp) = match expr.node with
| Lval lv -> Some lv
| CastE (typ, e) ->
- if Eval_typ.need_cast typ (Cil.typeOf e) then None else find_lval e
+ if Eval_typ.need_cast typ e.typ then None else find_lval e
| _ -> None
(* Emits an alarm if the left and right locations of a struct or union copy
@@ -217,7 +219,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
if Cil.isStructOrUnionType typ
then
let truth = Location.assume_no_overlap ~partial:true loc right_loc in
- let alarm () = Alarms.Overlap (lval, right_lval) in
+ let lval' = Evast_utils.to_cil_lval lval in
+ let right_lval' = Evast_utils.to_cil_lval right_lval in
+ let alarm () = Alarms.Overlap (lval', right_lval') in
Eval.interpret_truth ~alarm (loc, right_loc) truth
else `Value (loc, right_loc), Alarmset.none
@@ -351,7 +355,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| `Top -> Precise_locs.loc_top
| `Value record -> get record.loc
in
- let expr_zone = Eva_utils.zone_of_expr find_loc expr in
+ let expr_zone = Evast_utils.zone_of_exp find_loc expr in
let written_zone = inout.Inout_type.over_outputs_if_termination in
not (Locations.Zone.intersects expr_zone written_zone)
@@ -387,7 +391,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| Assign pre_value -> `Value pre_value
| Copy (_lv, pre_value) -> pre_value.v
in
- let lval = Cil.var argument.formal in
+ let lval = Evast_builder.var argument.formal in
(* We use copy_lvalue instead of evaluate to get the escaping flag:
if a formal is escaping at the end of the called function, it may
have been freed, which is not detected as a write. We prevent the
@@ -428,7 +432,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| None, Some vi_ret -> `Value (Domain.leave_scope kf_callee [vi_ret] state)
| Some _, None -> assert false
| Some lval, Some vi_ret ->
- let exp_ret_caller = Eva_utils.lval_to_exp (Var vi_ret, NoOffset) in
+ let exp_ret_caller = Evast_builder.var_exp vi_ret in
let+ state = assign_ret state (Kstmt stmt) lval exp_ret_caller in
Domain.leave_scope kf_callee [vi_ret] state
@@ -484,7 +488,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
[valuation]. Returns the value assigned, and the updated valuation.
TODO: share more code with [assign]. *)
let evaluate_actual ~subdivnb ~determinate valuation state expr =
- match expr.enode with
+ match (expr : Evast.exp).node with
| Lval lv ->
lvaluate_and_check ~for_writing:false ~subdivnb ~valuation state lv
>>= fun (valuation, loc, typ) ->
@@ -492,8 +496,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
then
Self.abort ~current:true
"Function argument %a has unknown size. Aborting"
- Printer.pp_exp expr;
- if determinate && Cil.isArithmeticOrPointerType (Cil.typeOfLval lv)
+ Evast_printer.pp_exp expr;
+ if determinate && Cil.isArithmeticOrPointerType lv.typ
then assign_by_eval ~subdivnb state valuation expr
else assign_by_copy ~subdivnb state valuation lv loc typ
| _ -> assign_by_eval ~subdivnb state valuation expr
@@ -537,7 +541,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let v = flagged.v >>-: Value.replace_base substitution in
let flagged = { flagged with v } in
let lloc = Location.replace_base substitution loc.lloc in
- let lval = Visitor.visitFramacLval visitor loc.lval in
+ let lval = Evast_visitor.Rewrite.visit_lval visitor loc.lval in
let loc = { loc with lval; lloc } in
Copy (loc, flagged)
@@ -547,7 +551,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let visitor = substitution_visitor tbl in
let base_substitution = recursion.base_substitution in
let replace_arg argument =
- let concrete = Visitor.visitFramacExpr visitor argument.concrete in
+ let concrete = Evast_visitor.Rewrite.visit_exp visitor argument.concrete in
let avalue = replace_value visitor base_substitution argument.avalue in
{ argument with concrete; avalue }
in
@@ -606,7 +610,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| `Value (valuation, _v) ->
show_expr (Eval.to_domain_valuation valuation) state fmt expr
in
- Format.fprintf fmt "%a : @[<h>%t@]" Printer.pp_exp expr pp
+ Format.fprintf fmt "%a : @[<h>%t@]" Evast_printer.pp_exp expr pp
in
let pp = Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@ " ~suf:"@]" pretty in
Self.result ~current:true
@@ -626,8 +630,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
fst (Eval.lvaluate ~for_writing:false ~subdivnb state lval) in
Eval_op.offsetmap_of_loc (get_ploc loc) (get_cvalue state)
in
- let typ = Cil.typeOfLval lval in
- (Bottom.pretty (Eval_op.pretty_offsetmap typ)) fmt offsm
+ (Bottom.pretty (Eval_op.pretty_offsetmap lval.typ)) fmt offsm
with Abstract_interp.Error_Top ->
Format.fprintf fmt "%s" (Unicode.top_string ())
@@ -643,9 +646,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(Bottom.pretty Cvalue.V.pretty) fmt value
let pretty_arguments ~subdivnb state arguments =
- let is_scalar lval = Cil.isArithmeticOrPointerType (Cil.typeOfLval lval) in
- let pretty fmt expr =
- match expr.enode with
+ let is_scalar lval = Cil.isArithmeticOrPointerType lval.Evast.typ in
+ let pretty fmt (expr : Evast.exp) =
+ match expr.node with
| Lval lval | StartOf lval when not (is_scalar lval) ->
show_offsm fmt subdivnb lval state
| _ -> show_value fmt subdivnb expr state
@@ -794,7 +797,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let list2, _ = eval_list valuation lvs2 in
let check acc (lval1, loc1) (lval2, loc2) =
let truth = Location.assume_no_overlap ~partial:false loc1 loc2 in
- let alarm () = Alarms.Not_separated (lval1, lval2) in
+ let lval1' = Evast_utils.to_cil_lval lval1
+ and lval2' = Evast_utils.to_cil_lval lval2 in
+ let alarm () = Alarms.Not_separated (lval1', lval2') in
let alarm = process_truth ~alarm truth in
Alarmset.combine alarm acc
in
@@ -812,7 +817,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let unauthorized_reads =
List.filter
(fun x -> List.for_all
- (fun y -> not (LvalStructEq.equal x y)) modified2)
+ (fun y -> not (Evast_datatype.Lval.equal x y)) modified2)
writes1
in
let alarms1 = check_non_overlapping state unauthorized_reads reads2 in
@@ -845,7 +850,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let initialized = false in
let init_value = Abstract_domain.Top in
let initialize_volatile state varinfo =
- let lval = Cil.var varinfo in
+ let lval = Evast_builder.var varinfo in
let location = Location.eval_varinfo varinfo in
Domain.initialize_variable lval location ~initialized init_value state
in
diff --git a/src/plugins/eva/eval.ml b/src/plugins/eva/eval.ml
index 3aa5c768e8eab5bee45d6f12f9f86e63baeafba0..090d6861db82922eace75159421cedab9b1fbdf3 100644
--- a/src/plugins/eva/eval.ml
+++ b/src/plugins/eva/eval.ml
@@ -22,6 +22,9 @@
open Cil_types
+type lval = Evast.lval
+type exp = Evast.exp
+
(** *)
(* -------------------------------------------------------------------------- *)
@@ -153,16 +156,16 @@ let compute_englobing_subexpr ~subexpr ~expr =
[subexpr], apart [subexpr] itself, or [None] if [subexpr] does not appear
in [expr]. *)
let rec compute expr =
- if Cil_datatype.ExpStructEq.equal expr subexpr
+ if Evast_datatype.Exp.equal expr subexpr
then Some []
else
- let sublist = match expr.enode with
+ let sublist = match expr.node with
| UnOp (_, e, _)
| CastE (_, e) ->
compute e
| BinOp (_, e1, e2, _) ->
merge (compute e1) (compute e2)
- | Lval (host, offset) ->
+ | Lval {node = (host, offset)} ->
merge (compute_host host) (compute_offset offset)
| _ -> None
in
@@ -179,9 +182,9 @@ let compute_englobing_subexpr ~subexpr ~expr =
Option.value ~default:[] (compute expr)
module Englobing =
- Datatype.Pair_with_collections (Cil_datatype.ExpStructEq) (Cil_datatype.ExpStructEq)
+ Datatype.Pair_with_collections (Evast_datatype.Exp) (Evast_datatype.Exp)
(struct let module_name = "Subexpressions" end)
-module SubExprs = Datatype.List (Cil_datatype.Exp)
+module SubExprs = Datatype.List (Evast_datatype.Exp)
module EnglobingSubexpr =
State_builder.Hashtbl (Englobing.Hashtbl) (SubExprs)
@@ -201,7 +204,7 @@ module Clear_Valuation (Valuation : Valuation) = struct
let englobing = compute_englobing_subexpr ~subexpr ~expr in
let remove valuation expr =
let valuation = Valuation.remove valuation expr in
- match expr.enode with
+ match expr.node with
| Lval lval -> Valuation.remove_loc valuation lval
| _ -> valuation
in
diff --git a/src/plugins/eva/eval.mli b/src/plugins/eva/eval.mli
index 91acacbbd63d9a3ed265eff60f59bdc8c4eeeab2..a31535df4ed8c7c360254e003b049e6a69984a7b 100644
--- a/src/plugins/eva/eval.mli
+++ b/src/plugins/eva/eval.mli
@@ -22,6 +22,9 @@
open Cil_types
+type lval = Evast.lval
+type exp = Evast.exp
+
(** Types and functions related to evaluations.
Heavily used by abstract values and domains, evaluation of expressions,
transfer functions of instructions and the dataflow analysis. *)
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index d522356bfe7982b879dd8b7e8d96f2eb1ae95022..9dd1badcc8aa3fbebf07b6f7b4ea86ff46a412d2 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -201,12 +201,13 @@ module Make (X: Analysis.S) = struct
GO_Bottom, true
let lval_to_offsetmap state lv =
+ let lv = Evast_builder.translate_lval lv in
let loc, alarms = X.eval_lval_to_loc state lv in
let ok = Alarmset.is_empty alarms in
let state = get_cvalue_or_top state in
let aux loc (acc_res, acc_ok) =
let res, ok =
- match lv with (* catch simplest pattern *)
+ match lv.node with (* catch simplest pattern *)
| Var vi, NoOffset -> extract_single_var state vi
| _ -> reduce_loc_and_eval state loc
in
@@ -248,6 +249,7 @@ module Make (X: Analysis.S) = struct
let lval_zone_ev =
let lv_to_zone state lv =
+ let lv = Evast_builder.translate_lval lv in
let loc, _alarms = X.eval_lval_to_loc state lv in
match loc with
| `Bottom -> Locations.Zone.bottom, false, false
@@ -284,6 +286,7 @@ module Make (X: Analysis.S) = struct
let exp_ev =
let eval_exp_and_warn state e =
+ let e = Evast_builder.translate_exp e in
let r = X.eval_expr state e in
fst r, Alarmset.is_empty (snd r), false
in
@@ -302,6 +305,7 @@ module Make (X: Analysis.S) = struct
let lval_ev =
let eval_and_warn state lval =
+ let lval = Evast_builder.translate_lval lval in
let r = X.copy_lvalue state lval in
let flagged_value = match fst r with
| `Bottom -> Eval.Flagged_Value.bottom
diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
index cc7ea0e3b8c01155c93a6b21b8f888dd871173ac..c0e855471ae880a99344f0213e7dc131916f9489 100644
--- a/src/plugins/eva/gui/register_gui.ml
+++ b/src/plugins/eva/gui/register_gui.ml
@@ -518,7 +518,7 @@ module Select (Eval: Eval) = struct
| Mem _, NoOffset when Cil.isFunctionType ty -> begin
(* Function pointers *)
(* get the list of functions in the values *)
- let e = Eva_utils.lval_to_exp lv in
+ let e = Evast_builder.(lval (translate_lval lv)) in
let state =
match ki with
| Kglobal -> Eval.Analysis.get_global_state ()
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 8977c3258ad885768eeb44910362628f82ed6aa9..e5a69c6f41e7a58f277738bba67422ff1e69369a 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -995,8 +995,8 @@ let forward_binop_by_type typ =
let forward_binop typ v1 op v2 =
match op with
- | Eq | Ne | Le | Lt | Ge | Gt ->
- let comp = Eva_utils.conv_comp op in
+ | Evast.Eq | Ne | Le | Lt | Ge | Gt ->
+ let comp = Evast_utils.conv_relation op in
if Cil.isPointerType typ || Cvalue_forward.are_comparable comp v1 v2
then forward_binop_by_type typ v1 op v2
else Cvalue.V.zero_or_one
@@ -1097,6 +1097,7 @@ let rec eval_term ~alarm_mode env t =
| BNot -> r.etype (* can only be used on an integer type *)
| LNot -> Cil.intType
in
+ let op = Evast_builder.translate_unop op in
let v = Cvalue_forward.forward_unop r.etype op r.eover in
let eover = v in
{ etype = typ';
@@ -1363,6 +1364,7 @@ and eval_binop ~alarm_mode env op t1 t2 =
let te1 = Cil.unrollType r1.etype in
check_logic_alarms ~alarm_mode te1 r1 op r2;
let typ_res = infer_binop_res_type op te1 in
+ let op = Evast_builder.translate_binop op in
let eover = forward_binop te1 r1.eover op r2.eover in
let default _r1 _r2 = under_from_over eover in
let add_untyped_op factor =
diff --git a/src/plugins/eva/partitioning/auto_loop_unroll.ml b/src/plugins/eva/partitioning/auto_loop_unroll.ml
index 7fa874f64bd0a34625c0b16633be632466eedb51..73da9d5434c9e32b6c00de9bcb5b54a15cdd9f1a 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.ml
@@ -56,15 +56,13 @@
normalization.
Any other assignment of [v] cancels the heuristic. *)
-open Cil_types
-
let is_true = function
| `True | `TrueReduced _ -> true
| _ -> false
(* Module for auxiliary functions manipulating interpreted automata. *)
module Graph = struct
- open Interpreted_automata
+ open Eva_automata
type loop =
{ graph: G.t; (* The complete graph of the englobing function. *)
@@ -78,7 +76,7 @@ module Graph = struct
let automaton = get_automaton kf in
let graph = automaton.graph in
let vertex, _ = Cil_datatype.Stmt.Hashtbl.find automaton.stmt_table stmt in
- match get_wto_index kf vertex with
+ match vertex.vertex_wto_index with
| [] -> raise Not_found
| head :: _ ->
(* Find in the wto the component whose head is [head]. *)
@@ -88,14 +86,12 @@ module Graph = struct
| Wto.Component (h, l) :: tl ->
if Vertex.equal h head then {graph; head; wto = l} else find (l @ tl)
in
- find (get_wto kf)
+ find automaton.wto
(* Applies [f acc instr] to all instructions [instr] in the [loop]. *)
- let fold_instr f loop acc =
+ let fold_transitions f loop acc =
let transfer (_v1, edge, _v2) acc =
- match edge.edge_transition with
- | Instr (instr, _stmt) -> f acc instr
- | _ -> acc
+ f acc edge.edge_transition
in
let compute_vertex = G.fold_pred_e transfer loop.graph in
let wto = Wto.flatten loop.wto in
@@ -145,7 +141,7 @@ module Graph = struct
(* A loop exit condition is an expression and a boolean expression whether the
expression must be zero or not-zero to exit the loop. *)
module Condition = struct
- module Exp = Cil_datatype.ExpStructEq
+ module Exp = Evast_datatype.Exp
module Info = struct let module_name = "Condition" end
include Datatype.Pair_with_collections (Exp) (Datatype.Bool) (Info)
end
@@ -175,17 +171,20 @@ let add_written_var vi effect =
let written_vars = Cil_datatype.Varinfo.Set.add vi effect.written_vars in
{ effect with written_vars }
-let is_frama_c_builtin exp =
- match exp.enode with
- | Lval (Var vi, NoOffset) -> Ast_info.start_with_frama_c_builtin vi.vname
+let is_frama_c_builtin (exp : Evast.exp) =
+ match exp.node with
+ | Lval { node = Var vi, NoOffset } ->
+ Ast_info.start_with_frama_c_builtin vi.vname
| _ -> false
-let compute_instr_effect effect = function
- | Set ((Var varinfo, _), _, _) -> add_written_var varinfo effect
- | Set ((Mem _, _), _, _) -> { effect with pointer_writes = true }
- | Call (Some (Var varinfo, _), _, _, _) ->
+let compute_transition_effect effect = function
+ | Eva_automata.Assign ({node = (Var varinfo, _)}, _, _) ->
+ add_written_var varinfo effect
+ | Assign ({node = (Mem _, _)}, _, _) ->
+ { effect with pointer_writes = true }
+ | Call (Some {node = Var varinfo, _}, _, _, _) ->
{ (add_written_var varinfo effect) with call = true; }
- | Call (Some (Mem _, _), _, _, _) ->
+ | Call (Some {node = Mem _, _}, _, _, _) ->
{ effect with pointer_writes = true; call = true; }
| Call (None, exp, _, _) when not (is_frama_c_builtin exp) ->
{ effect with call = true }
@@ -202,7 +201,7 @@ let compute_loop_effect loop =
call = false;
assembly = false; }
in
- let effect = Graph.fold_instr compute_instr_effect loop acc in
+ let effect = Graph.fold_transitions compute_transition_effect loop acc in
if effect.assembly then None else Some effect
(* The status of a lvalue for the automatic loop unroll heuristic. *)
@@ -214,23 +213,23 @@ type var_status =
in the loop. *)
| Unsuitable (* Cannot be used for the heuristic. *)
-let is_integer lval = Cil.isIntegralType (Cil.typeOfLval lval)
+let is_integer lval = Cil.isIntegralType lval.Evast.typ
(* Computes the status of a lvalue for the heuristic, according to the
loop effects. Uses [eval_ptr] to compute the bases pointed by pointer
expressions. *)
-let classify eval_ptr loop_effect lval =
+let classify eval_ptr loop_effect (lval : Evast.lval) =
let is_written varinfo =
Cil_datatype.Varinfo.Set.mem varinfo loop_effect.written_vars
in
- let rec is_const_expr expr =
- match expr.enode with
+ let rec is_const_expr (expr : Evast.exp) =
+ match expr.node with
| Lval lval -> classify_lval lval = Constant
| UnOp (_, e, _) | CastE (_, e) -> is_const_expr e
| BinOp (_, e1, e2, _) -> is_const_expr e1 && is_const_expr e2
| Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
| AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> true
- and classify_lval = function
+ and classify_lval lv = match lv.node with
| Var varinfo, offset ->
if (varinfo.vglob && loop_effect.call)
|| not (is_const_offset offset)
@@ -259,8 +258,8 @@ let classify eval_ptr loop_effect lval =
classify_lval lval
(* Returns the list of all lvalues appearing in an expression. *)
-let rec get_lvalues expr =
- match expr.enode with
+let rec get_lvalues (expr : Evast.exp) =
+ match expr.node with
| Lval lval -> [ lval ]
| UnOp (_, e, _) | CastE (_, e) -> get_lvalues e
| BinOp (_op, e1, e2, _typ) -> get_lvalues e1 @ get_lvalues e2
@@ -286,38 +285,35 @@ let find_lonely_candidate eval_ptr loop_effect expr =
except on assignemnts of [lval]:
- to the value of an expression [expr], it applies [f expr acc];
- to a function call, or if [inner_loop] is true, it raises [exn]. *)
-let transfer_assign lval exn f ~inner_loop acc instr =
- let is_lval = Cil_datatype.LvalStructEq.equal lval in
- let transfer_instr ~inner_loop acc = function
- | Set (lv, expr, _loc) when is_lval lv ->
- if inner_loop then raise exn else f expr acc
- | Local_init (vi, AssignInit (SingleInit expr), _loc)
- when is_lval (Cil.var vi) && not inner_loop ->
- f expr acc
- | Local_init (vi, _, _) when is_lval (Cil.var vi) -> raise exn
- | Call (Some lv, _, _, _) when is_lval lv -> raise exn
- | _ -> acc
- in
- match instr with
- | Interpreted_automata.Instr (instr, _stmt) ->
- transfer_instr ~inner_loop acc instr
+let transfer_assign lval exn f ~inner_loop acc transition =
+ let is_lval = Evast_datatype.Lval.equal lval in
+ match transition with
+ | Eva_automata.Assign (lv, expr, _loc)
+ when is_lval lv ->
+ if inner_loop then raise exn else f expr acc
+ | Init (vi, SingleInit (expr, _loc), _loc')
+ when is_lval (Evast_builder.var vi) && not inner_loop ->
+ f expr acc
+ | Init (vi, _, _) when is_lval (Evast_builder.var vi) -> raise exn
+ | Call (Some lv, _, _, _) when is_lval lv ->
+ raise exn
| _ -> acc
(* If in the [loop], [lval] is always assigned to the value of another
lvalue, returns this new lvalue. Otherwise, returns [lval]. *)
-let cross_equality loop lval =
+let cross_equality loop (lval : Evast.lval) =
(* If no such single equality can be found, return [lval] unchanged. *)
let exception No_equality in
- let find_lval expr _x =
- match expr.enode with
+ let find_lval (expr : Evast.exp) _x =
+ match expr.node with
| Lval lval -> lval
| _ -> raise No_equality
in
- let transfer ~inner_loop lval instr =
- transfer_assign lval No_equality find_lval ~inner_loop lval instr
+ let transfer ~inner_loop lval transition =
+ transfer_assign lval No_equality find_lval ~inner_loop lval transition
in
let join lv1 lv2 =
- if Cil_datatype.LvalStructEq.equal lv1 lv2 then lv1 else raise No_equality
+ if Evast_datatype.Lval.equal lv1 lv2 then lv1 else raise No_equality
in
match Graph.compute ~backward:true loop transfer join lval with
| Some lval -> lval
@@ -349,9 +345,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Adds or subtracts the integer value of [expr] to the current increment
[acc.delta], according to [binop] which can be PlusA or MinusA.
Raises NoIncrement if [expr] is not a constant integer expression. *)
- let add_to_delta context binop acc expr =
- let typ = Cil.typeOf expr in
- match Cil.constFoldToInt expr with
+ let add_to_delta context binop acc (expr : Evast.exp) =
+ let typ = expr.typ in
+ match Evast_utils.fold_to_integer expr with
| None -> raise NoIncrement
| Some i ->
let inject i = Val.inject_int typ i in
@@ -362,17 +358,17 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
of [expr]. Raises NoIncrement if this is not an increment of [lval]. *)
let rec delta_assign context lval expr acc =
(* Is the expression [e] equal to the lvalue [lval] (modulo cast)? *)
- let rec is_lval e = match e.enode with
- | Lval lv -> Cil_datatype.LvalStructEq.equal lval lv
+ let rec is_lval (e : Evast.exp) = match e.node with
+ | Lval lv -> Evast_datatype.Lval.equal lval lv
| CastE (typ, e) -> Cil.isIntegralType typ && is_lval e
| _ -> false
in
- match Cil.constFoldToInt expr with
+ match Evast_utils.fold_to_integer expr with
| Some i ->
- let v = Val.inject_int (Cil.typeOf expr) i in
+ let v = Val.inject_int expr.typ i in
{ value = `Value v; delta = `Bottom; }
| None ->
- match expr.enode with
+ match expr.node with
| BinOp ((PlusA | MinusA) as binop, e1, e2, _) ->
if is_lval e1
then add_to_delta context binop acc e2
@@ -450,12 +446,13 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
[condition] is NOT positive; its complement is an under-approximation
of the values for which [condition] is positive. *)
let cvalue = get_cvalue value in
- cvalue_complement (Cil.typeOf expr) cvalue >>= fun cvalue ->
+ cvalue_complement expr.typ cvalue >>= fun cvalue ->
Some (Val.set Main_values.CVal.key cvalue Val.top)
(* If [lval] is a varinfo out-of-scope at statement [stmt] of function [kf],
introduces it to the [state]. *)
- let enter_scope state kf stmt = function
+ let enter_scope state kf stmt (lval : Evast.lval) =
+ match lval.node with
| Var vi, _ ->
let state =
if vi.vglob || vi.vformal || Kernel_function.var_is_in_scope stmt vi
@@ -475,7 +472,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* If [lval] is not in scope at [stmt], introduces it into [state] so that
the [condition] can be properly evaluated in [state]. *)
let state = enter_scope state kf stmt lval in
- let expr = Cil.new_exp ~loc:condition.eloc (Lval lval) in
+ let expr = Evast_builder.lval lval in
(* Evaluate the [condition] in the given [state]. *)
fst (Eval.evaluate state condition) >> fun (valuation, _v) ->
(* In the resulting valuation, replace the value of [expr] by [top_int]
@@ -541,7 +538,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Computes an over-approximation [v_incr] of the value update of [lval]
in one iteration of the loop. *)
compute_delta context lval loop >>: fun v_incr ->
- let typ = Cil.typeOfLval lval in
+ let typ = lval.typ in
let forward_binop op v1 v2 = Val.forward_binop context typ op v1 v2 in
let binop op v1 v2 = Bottom.non_bottom (forward_binop op v1 v2) in
(* Computes the possible values of [lval] after n loop iterations. *)
diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml
index de5b74d641785d5f68b4a1b73e3692de6f88a9c5..b6cd69abc53f98ab60927ffebffc65d3d19b18b6 100644
--- a/src/plugins/eva/partitioning/partition.ml
+++ b/src/plugins/eva/partitioning/partition.ml
@@ -313,7 +313,7 @@ type action =
| Incr_loop
| Branch of branch * int
| Ration of rationing
- | Restrict of Cil_types.exp * Integer.t list
+ | Restrict of Evast.exp * Integer.t list
| Split of split_term * split_kind * split_monitor
| Merge of split_term
| Update_dynamic_splits
@@ -370,47 +370,46 @@ struct
exception Operation_failed
- let fail ~exp message =
- let source = fst exp.Cil_types.eloc in
+ let fail ~source message =
let warn_and_raise message =
Self.warning ~source ~once:true "%s" message;
raise Operation_failed
in
Pretty_utils.ksfprintf warn_and_raise message
- let evaluate_exp_to_ival state exp =
+ let evaluate_exp_to_ival ~source state exp =
(* Evaluate the expression *)
let valuation, value =
match evaluate state exp with
| `Value (valuation, value), alarms when Alarmset.is_empty alarms ->
valuation, value
| _ ->
- fail ~exp "this partitioning parameter cannot be evaluated safely on \
- all states"
+ fail ~source "this partitioning parameter cannot be evaluated safely on \
+ all states"
in
(* Get the cvalue *)
let cvalue = match Abstract.Val.get Main_values.CVal.key with
| Some get_cvalue -> get_cvalue value
- | None -> fail ~exp "partitioning is disabled when the CValue domain is \
- not active"
+ | None -> fail ~source "partitioning is disabled when the CValue domain is \
+ not active"
in
(* Extract the ival *)
let ival =
try
Cvalue.V.project_ival cvalue
with Cvalue.V.Not_based_on_null ->
- fail ~exp "this partitioning parameter must evaluate to an integer"
+ fail ~source "this partitioning parameter must evaluate to an integer"
in
valuation, ival
exception Split_limit of Integer.t option
- let split_by_value ~monitor state exp =
+ let split_by_value ~monitor ~source state exp =
let module SplitValues = Datatype.Integer.Set in
- let valuation, ival = evaluate_exp_to_ival state exp in
+ let valuation, ival = evaluate_exp_to_ival ~source state exp in
(* Build a state with the lvalue set to a singleton *)
let build i acc =
- let value = Abstract.Val.inject_int (Cil.typeOf exp) i in
+ let value = Abstract.Val.inject_int exp.typ i in
let state =
let* valuation = Abstract.Eval.assume ~valuation state exp value in
(* Check the reduction *)
@@ -418,9 +417,9 @@ struct
in
match state with
| `Value state ->
- let _,new_ival = evaluate_exp_to_ival state exp in
+ let _,new_ival = evaluate_exp_to_ival ~source state exp in
if not (Ival.is_singleton_int new_ival) then
- fail ~exp "failing to learn perfectly from split" ;
+ fail ~source "failing to learn perfectly from split" ;
monitor.split_values <-
SplitValues.add i monitor.split_values;
(i, state) :: acc
@@ -452,18 +451,18 @@ struct
| None -> ()
| Some c -> Format.fprintf fmt " (%a)" Integer.pretty c
in
- fail ~exp "split on more than %d values%t prevented ; try to improve \
- the analysis precision or look at the option -eva-split-limit \
- to increase this limit."
+ fail ~source "split on more than %d values%t prevented ; try to improve \
+ the analysis precision or look at the option -eva-split-limit \
+ to increase this limit."
monitor.split_limit pp_count
- let eval_exp_to_int state exp =
- let _valuation, ival = evaluate_exp_to_ival state exp in
+ let eval_exp_to_int ~source state exp =
+ let _valuation, ival = evaluate_exp_to_ival ~source state exp in
try Integer.to_int_exn (Ival.project_int ival)
with
| Ival.Not_Singleton_Int ->
- fail ~exp "this partitioning parameter must evaluate to a singleton"
- | Z.Overflow -> fail ~exp "this partitioning parameter overflows an integer"
+ fail ~source "this partitioning parameter must evaluate to a singleton"
+ | Z.Overflow -> fail ~source "this partitioning parameter overflows an integer"
let split_by_predicate state predicate =
let env =
@@ -494,7 +493,7 @@ struct
let stamp_by_value = match Abstract.Val.get Main_values.CVal.key with
| None -> fun _ _ _ -> None
| Some get -> fun expr expected_values state ->
- let typ = Cil.typeOf expr in
+ let typ = expr.Evast.typ in
let make stamp i = stamp, i, Abstract.Val.inject_int typ i in
let expected_values = List.mapi make expected_values in
match fst (evaluate state expr) with
@@ -520,8 +519,12 @@ struct
in
let states =
match term with
- | Expression exp -> split_by_value ~monitor state exp
- | Predicate pred -> split_by_predicate state pred
+ | Expression cil_exp ->
+ let exp = Evast_builder.translate_exp cil_exp
+ and source = fst cil_exp.eloc in
+ split_by_value ~monitor ~source state exp
+ | Predicate pred ->
+ split_by_predicate state pred
in
List.map update_key states
with Operation_failed -> [(key,state)]
@@ -567,7 +570,10 @@ struct
| Enter_loop limit_kind -> fun k x ->
let limit = try match limit_kind with
- | ExpLimit exp -> eval_exp_to_int x exp
+ | ExpLimit cil_exp ->
+ let exp = Evast_builder.translate_exp cil_exp
+ and source = fst cil_exp.eloc in
+ eval_exp_to_int ~source x exp
| IntLimit i -> i
| AutoUnroll (stmt, min_unroll, max_unroll) ->
match AutoLoopUnroll.compute ~max_unroll x stmt with
diff --git a/src/plugins/eva/partitioning/partition.mli b/src/plugins/eva/partitioning/partition.mli
index d4a97bcb6f2b2204553d37e7080980a1836b7ede..6c4ae05ecbc97dcb707d22fed8312defb3127849 100644
--- a/src/plugins/eva/partitioning/partition.mli
+++ b/src/plugins/eva/partitioning/partition.mli
@@ -143,7 +143,7 @@ type action =
If the rationing has been created with [merge:true], all the states from
each flow receive the same stamp, but states from different flows receive
different stamps, until [limit] states have been tagged. *)
- | Restrict of Cil_types.exp * Integer.t list
+ | Restrict of Evast.exp * Integer.t list
(** [Restrict (exp, list)] restricts the rationing according to the evaluation
of the expression [exp]:
– for each integer [i] in [list], states in which [exp] evaluates exactly
diff --git a/src/plugins/eva/partitioning/partitioning_parameters.ml b/src/plugins/eva/partitioning/partitioning_parameters.ml
index bb6fc8393032bd801effb4761aff2f5543d356d5..47f76fcbc435925a57d1d06f53e1f97d1ee5d4bf 100644
--- a/src/plugins/eva/partitioning/partitioning_parameters.ml
+++ b/src/plugins/eva/partitioning/partitioning_parameters.ml
@@ -93,7 +93,9 @@ struct
try
match Logic_utils.constFoldTermToInt t with
| Some n -> Partition.IntLimit (Integer.to_int_exn n)
- | None -> Partition.ExpLimit (Logic_to_c.term_to_exp t)
+ | None ->
+ let cil_exp = Logic_to_c.term_to_exp t in
+ Partition.ExpLimit (cil_exp)
with Z.Overflow | Logic_to_c.No_conversion ->
warn "invalid loop unrolling parameter; ignoring";
default
diff --git a/src/plugins/eva/partitioning/trace_partitioning.ml b/src/plugins/eva/partitioning/trace_partitioning.ml
index 35c48ebab9791687e1a9e9d38c09c704aea41bc3..99d87b42ce9ac104a664951a061ab4284cfb9fdf 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.ml
+++ b/src/plugins/eva/partitioning/trace_partitioning.ml
@@ -173,7 +173,7 @@ struct
let empty_rationing = new_rationing ~limit:0 ~merge:false
- let split_return (flow : flow) (return_exp : exp option) : flow =
+ let split_return (flow : flow) (return_exp : Evast.exp option) : flow =
let strategy = Split_return.kf_strategy kf in
if strategy = Split_strategy.FullSplit
then flow
@@ -189,7 +189,7 @@ struct
match return_exp with
| None -> apply (Ration empty_rationing)
| Some return_exp ->
- if Cil.isIntegralOrPointerType (Cil.typeOf return_exp)
+ if Cil.isIntegralOrPointerType return_exp.typ
then apply (Restrict (return_exp, i))
else apply (Ration empty_rationing)
diff --git a/src/plugins/eva/partitioning/trace_partitioning.mli b/src/plugins/eva/partitioning/trace_partitioning.mli
index e8bae0463bd426533cfcd26a5ace15e3e21817ee..8b93fd07da9b62cd884ee77084aaeaa6b0537c25 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.mli
+++ b/src/plugins/eva/partitioning/trace_partitioning.mli
@@ -85,7 +85,7 @@ sig
val enter_loop : flow -> Cil_types.stmt -> flow
val leave_loop : flow -> Cil_types.stmt -> flow
val next_loop_iteration : flow -> Cil_types.stmt -> flow
- val split_return : flow -> Cil_types.exp option -> flow
+ val split_return : flow -> Evast.exp option -> flow
(** After the analysis of a function call, recombines callee partitioning keys
with the caller key. *)
diff --git a/src/plugins/eva/utils/backward_formals.ml b/src/plugins/eva/utils/backward_formals.ml
index ba00c3ed430fab670dcccc768da5ee89fd3239b0..69fd2da65a6b74b06a2b5ca57b44c9ea6b89b3cd 100644
--- a/src/plugins/eva/utils/backward_formals.ml
+++ b/src/plugins/eva/utils/backward_formals.ml
@@ -22,30 +22,24 @@
open Cil_types
-exception Unsafe
-(* This visitor checks that an expression is guaranteed to evaluate in
+(* This function checks that an expression is guaranteed to evaluate in
the same way before and after a call. We restrict ourselves to
lvalues that are unreferenced locals or formals, because they cannot
be changed by the callee. *)
-let safe_argument_visitor = object(self)
- inherit Visitor.frama_c_inplace
-
- method! vlval = function
+let safe_argument expr =
+ let exception Unsafe in
+ let f (lv : Evast.lval) =
+ match lv.node with
| Var vi, NoOffset ->
if vi.vaddrof || Cil.typeHasQualifier "volatile" vi.vtype || vi.vglob
- then raise Unsafe;
- Cil.DoChildren
+ then raise Unsafe
| _, _ -> raise Unsafe
-
- method inspect expr =
- try
- ignore (Visitor.visitFramacExpr (self:>Visitor.frama_c_inplace) expr);
- true
- with Unsafe -> false
-end
-
-let safe_argument = safe_argument_visitor#inspect
+ in
+ try
+ Evast_utils.iter_lvals f expr;
+ true
+ with Unsafe -> false
let written_formals kf =
diff --git a/src/plugins/eva/utils/backward_formals.mli b/src/plugins/eva/utils/backward_formals.mli
index a9675d8b607c2b69a355e7933c7d1987aa56baa1..204928a5ff32126c95fd8b49071c6cdbcdb73bf7 100644
--- a/src/plugins/eva/utils/backward_formals.mli
+++ b/src/plugins/eva/utils/backward_formals.mli
@@ -30,7 +30,7 @@ val written_formals: Cil_types.kernel_function -> Cil_datatype.Varinfo.Set.t
which may be internally overwritten by [kf] during its call. *)
-val safe_argument: Cil_types.exp -> bool
+val safe_argument: Evast.exp -> bool
(** [safe_argument e] returns [true] if [e] (which is supposed to be
an actual parameter) is guaranteed to evaluate in the same way before and
after the call. *)
diff --git a/src/plugins/eva/utils/eval_typ.ml b/src/plugins/eva/utils/eval_typ.ml
index 4f4f00068f4f788642f276789cf077ea4c93ba6b..20152b08f674ad06c2ce8320390bb3d46b4c1f38 100644
--- a/src/plugins/eva/utils/eval_typ.ml
+++ b/src/plugins/eva/utils/eval_typ.ml
@@ -114,7 +114,7 @@ let refine_fun_ptr typ args =
match Cil.unrollType typ, args with
| TFun (_, Some _, _, _), _ | _, None -> typ
| TFun (ret, None, var, attrs), Some l ->
- let ltyps = List.map (fun arg -> "", Cil.typeOf arg, []) l in
+ let ltyps = List.map (fun arg -> "", arg, []) l in
TFun (ret, Some ltyps, var, attrs)
| _ -> assert false
diff --git a/src/plugins/eva/utils/eval_typ.mli b/src/plugins/eva/utils/eval_typ.mli
index bff63934fa58375714700d5afa4a93c2c5cd0af3..18a6aebfee3a7863d5e8dde392bb45d69a5f769f 100644
--- a/src/plugins/eva/utils/eval_typ.mli
+++ b/src/plugins/eva/utils/eval_typ.mli
@@ -54,7 +54,7 @@ val need_cast: typ -> typ -> bool
ignore more or less safely the incompatibility in the types (which is however
reported in the returned boolean). *)
val compatible_functions:
- typ -> ?args:exp list -> Kernel_function.t list ->
+ typ -> ?args:typ list -> Kernel_function.t list ->
Kernel_function.t list * bool
val expr_contains_volatile: exp -> bool
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index dd3d5c7c6d70b84f617c202e693bbf962b92b797..d04c0a92b44d682fe3742528c80b12b9a5052546 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -43,6 +43,10 @@ module Eval_annots = Eval_annots
module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
+module Evast = Evast
+module Evast_builder = Evast_builder
+module Evast_datatype = Evast_datatype
+module Evast_utils = Evast_utils
module Function_calls = Function_calls
module Logic_inout = Logic_inout
module Main_locations = Main_locations
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index a00af9b2d37525e367ddedfb7549a967ed2b14bc..cd349fd58b24a68718ad076c84467caa3c00e76b 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -47,6 +47,10 @@ module Eval_annots = Eval_annots
module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
+module Evast = Evast
+module Evast_builder = Evast_builder
+module Evast_datatype = Evast_datatype
+module Evast_utils = Evast_utils
module Function_calls = Function_calls
module Logic_inout = Logic_inout
module Main_locations = Main_locations
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index cf551e2b0d146022e6886a25cf7b6c6ac4db027a..d1bad3190eb01961d46e62162442298d5f4c9b88 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -286,31 +286,6 @@ struct
| Bottom -> false
| _ -> true
- let equality_class exp req =
- let open Equality in
- match A.Dom.get Equality_domain.key with
- | None ->
- Result.error DisabledDomain
- | Some extract ->
- let hce = Hcexprs.HCE.of_exp exp in
- let extract' state =
- let equalities = Equality_domain.project (extract state) in
- try NonTrivial (Set.find hce equalities)
- with Not_found -> Trivial
- and reduce e1 e2 =
- match e1, e2 with
- | Trivial, _ | _, Trivial -> Trivial
- | NonTrivial e1, NonTrivial e2 -> Equality.inter e1 e2
- in
- let r = match Response.map_join extract' reduce (get req) with
- | (`Top | `Bottom) as r -> r
- | `Value Trivial -> `Top
- | `Value (NonTrivial e) ->
- let l = Equality.elements e in
- `Value (List.map Hcexprs.HCE.to_exp l)
- in
- convert r
-
let get_cvalue_model req =
match A.Dom.get Cvalue_domain.State.key with
| None ->
@@ -527,10 +502,6 @@ let by_callstack req =
(* State requests *)
-let equality_class exp req =
- let module E = Make () in
- E.equality_class exp req
-
let get_cvalue_model_result req =
let module E = Make () in
E.get_cvalue_model req
@@ -576,13 +547,17 @@ let build_eval_lval_and_exp () =
let eval_exp exp req = build @@ M.eval_exp exp req in
eval_lval, eval_exp
-let eval_lval lval req = Value ((fst @@ build_eval_lval_and_exp ()) lval req)
+let eval_lval lval req =
+ let lval = Evast_builder.translate_lval lval in
+ Value ((fst @@ build_eval_lval_and_exp ()) lval req)
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_exp exp req =
+ let exp = Evast_builder.translate_exp exp in
+ Value ((snd @@ build_eval_lval_and_exp ()) exp req)
-let eval_address ?(for_writing=false) lval req =
+let eval_address' ?(for_writing=false) lval req =
let module M = Make () in
let v = M.eval_address ~for_writing lval req in
Address
@@ -591,6 +566,10 @@ let eval_address ?(for_writing=false) lval req =
let v = v
end : Lvaluation)
+let eval_address ?(for_writing=false) lval req =
+ let lval = Evast_builder.translate_lval lval in
+ eval_address' ~for_writing lval req
+
let eval_callee exp req =
(* Check the validity of exp *)
begin match exp with
@@ -599,6 +578,7 @@ let eval_callee exp req =
invalid_arg "The callee must be an lvalue with no offset"
end;
let module M = Make () in
+ let exp = Evast_builder.translate_exp exp in
M.eval_callee exp req
let callee stmt =
@@ -722,20 +702,21 @@ let alarms : type a. a evaluation -> Alarms.t list =
(* Dependencies *)
let expr_deps expr request =
- let lval_to_loc lv = eval_address lv request |> as_precise_loc in
- Eva_utils.zone_of_expr lval_to_loc expr
+ let lval_to_loc lv = eval_address' lv request |> as_precise_loc in
+ Evast_utils.zone_of_exp lval_to_loc (Evast_builder.translate_exp expr)
let lval_deps lval request =
- let lval_to_loc lv = eval_address lv request |> as_precise_loc in
- Eva_utils.zone_of_expr lval_to_loc (Cil.dummy_exp (Lval lval))
+ let lval_to_loc lv = eval_address' lv request |> as_precise_loc in
+ Evast_utils.zone_of_lval lval_to_loc (Evast_builder.translate_lval lval)
let address_deps lval request =
- let lval_to_loc lv = eval_address lv request |> as_precise_loc in
- Eva_utils.indirect_zone_of_lval lval_to_loc lval
+ let lval_to_loc lv = eval_address' lv request |> as_precise_loc in
+ Evast_utils.indirect_zone_of_lval lval_to_loc
+ (Evast_builder.translate_lval lval)
let expr_dependencies expr request =
- let lval_to_loc lv = eval_address lv request |> as_precise_loc in
- Eva_utils.deps_of_expr lval_to_loc expr
+ let lval_to_loc lv = eval_address' lv request |> as_precise_loc in
+ Evast_utils.deps_of_exp lval_to_loc (Evast_builder.translate_exp expr)
(* Taint *)
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index 60965a2fa111758342eec3dba15942a069433589..5686ce1670135fb2c6cd384e89254838098417f3 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -146,10 +146,6 @@ val by_callstack : request -> (Callstack.t * request) list
(** State requests *)
-(** Returns the list of expressions which have been inferred to be equal to
- the given expression by the Equality domain. *)
-val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
-
(** Returns the Cvalue state. Error cases are converted into the bottom or top
cvalue state accordingly. *)
val get_cvalue_model : request -> Cvalue.Model.t
diff --git a/src/plugins/eva/utils/unit_tests.ml b/src/plugins/eva/utils/unit_tests.ml
index 2b3ab6fc5273e0dc3223c8cee2fba39485846e1b..813ed5ad781c5181ef2e7567efe2790fc7c932d5 100644
--- a/src/plugins/eva/utils/unit_tests.ml
+++ b/src/plugins/eva/utils/unit_tests.ml
@@ -99,8 +99,8 @@ module Sign = struct
let sign_res = Sign.forward_unop context typ unop sign in
let bug = not (Bottom.is_included is_included cval_res sign_res) in
report bug "%a %a = %a while %a %a = %a"
- Printer.pp_unop unop Cval.pretty cval (Bottom.pretty Cval.pretty) cval_res
- Printer.pp_unop unop Sign.pretty sign (Bottom.pretty Sign.pretty) sign_res
+ Evast_printer.pp_unop unop Cval.pretty cval (Bottom.pretty Cval.pretty) cval_res
+ Evast_printer.pp_unop unop Sign.pretty sign (Bottom.pretty Sign.pretty) sign_res
in
List.iter test values
@@ -111,9 +111,9 @@ module Sign = struct
let sign_res = Sign.forward_binop context typ binop sign1 sign2 in
let bug = not (Bottom.is_included is_included cval_res sign_res) in
report bug "%a %a %a = %a while %a %a %a = %a"
- Cval.pretty cval1 Printer.pp_binop binop Cval.pretty cval2
+ Cval.pretty cval1 Evast_printer.pp_binop binop Cval.pretty cval2
(Bottom.pretty Cval.pretty) cval_res
- Sign.pretty sign1 Printer.pp_binop binop Sign.pretty sign2
+ Sign.pretty sign1 Evast_printer.pp_binop binop Sign.pretty sign2
(Bottom.pretty Sign.pretty) sign_res
in
List.iter (fun x -> List.iter (test x) values) values
diff --git a/src/plugins/eva/utils/widen.ml b/src/plugins/eva/utils/widen.ml
index 40c6b225e8d874e242ca0c494e134fab204b3098..5335d863a60572cc281943e4937ae222661b197e 100644
--- a/src/plugins/eva/utils/widen.ml
+++ b/src/plugins/eva/utils/widen.ml
@@ -437,7 +437,7 @@ module Parsed_Dynamic_Hints =
end)
let dynamic_bases_of_lval states e offset =
- let lv = (Mem e, offset) in
+ let lv = Evast_builder.mk_lval (Mem e, offset) in
List.fold_left (fun acc' state ->
let location = Cvalue_queries.lval_to_loc state lv in
Locations.Location_Bits.fold_bases
@@ -510,6 +510,8 @@ let dynamic_widen_hints_hook _callstack stmt states =
List.fold_right (fun dhint (_acc_modified, acc_hints as acc) ->
let old_bases = dhint.bases in
let exp, offset = dhint.lv in
+ let exp = Evast_builder.translate_exp exp
+ and offset = Evast_builder.translate_offset offset in
let bases = dynamic_bases_of_lval states exp offset in
let new_bases = Base.Hptset.diff bases old_bases in
if Base.Hptset.is_empty new_bases then
diff --git a/src/plugins/eva/values/abstract_value.ml b/src/plugins/eva/values/abstract_value.ml
index 2f82d4852466d2fa7bb47e4a50974f7a5fc5bd59..8643761001a0abe7ed6fccb1d4bdde2ccffded8f 100644
--- a/src/plugins/eva/values/abstract_value.ml
+++ b/src/plugins/eva/values/abstract_value.ml
@@ -25,6 +25,8 @@
open Cil_types
open Eval
+type constant = Evast.constant
+
(** Type for the truth value of an assertion in a value abstraction. The two
last tags should be used only for a product of value abstractions. *)
type 'v truth =
@@ -138,12 +140,13 @@ module type S = sig
(** [forward_unop typ unop v] evaluates the value [unop v], resulting from the
application of the unary operator [unop] to the value [v]. [typ] is the
type of [v]. *)
- val forward_unop : context enriched -> typ -> unop -> t -> t or_bottom
+ val forward_unop : context enriched -> typ -> Evast.unop -> t -> t or_bottom
(** [forward_binop typ binop v1 v2] evaluates the value [v1 binop v2],
resulting from the application of the binary operator [binop] to the
values [v1] and [v2]. [typ] is the type of [v1]. *)
- val forward_binop : context enriched -> typ -> binop -> t -> t -> t or_bottom
+ val forward_binop :
+ context enriched -> typ -> Evast.binop -> t -> t -> t or_bottom
(** [rewrap_integer irange t] wraps around the abstract value [t] to fit the
integer range [irange], assuming 2's complement. Also used on absolute
@@ -180,14 +183,14 @@ module type S = sig
[input_type] is the type of [left], [resulting_type] the type of [result]. *)
val backward_binop :
context enriched -> input_type:typ -> resulting_type:typ ->
- binop -> left:t -> right:t -> result:t ->
+ Evast.binop -> left:t -> right:t -> result:t ->
(t option * t option) or_bottom
(** Backward evaluation of the unary operation [unop arg = res];
tries to reduce the argument [arg] according to [res].
[typ_arg] is the type of [arg]. *)
val backward_unop :
- context enriched -> typ_arg:typ -> unop ->
+ context enriched -> typ_arg:typ -> Evast.unop ->
arg:t -> res:t -> t option or_bottom
(** Backward evaluation of the cast of the value [src_val] of type [src_typ]
diff --git a/src/plugins/eva/values/cvalue_backward.ml b/src/plugins/eva/values/cvalue_backward.ml
index 657f312f89bc2fa57948829a176782a10bd19300..05f33f98825069303398d9f3acbf3c09caba25f3 100644
--- a/src/plugins/eva/values/cvalue_backward.ml
+++ b/src/plugins/eva/values/cvalue_backward.ml
@@ -260,7 +260,7 @@ let backward_lor ~v1 ~v2 ~res =
let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
let typ = Cil.unrollType typ_res in
match binop, typ with
- | PlusA, TInt _ -> backward_add_int typ ~res_value ~v1 ~v2 true
+ | Evast.PlusA, TInt _ -> backward_add_int typ ~res_value ~v1 ~v2 true
| MinusA, TInt _ -> backward_add_int typ ~res_value ~v1 ~v2 false
| PlusA, TFloat (fk, _) -> backward_add_float (Fval.kind fk) ~res_value ~v1 ~v2 `Add
@@ -277,7 +277,7 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
(* comparison operators *)
| (Eq | Ne | Le | Lt | Ge | Gt), _ -> begin
- let binop = Eva_utils.conv_comp binop in
+ let binop = Evast_utils.conv_relation binop in
match V.is_included V.singleton_zero res_value,
V.is_included V.singleton_one res_value with
| true, true ->
@@ -339,7 +339,7 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
let backward_unop ~typ_arg op ~arg:_ ~res =
match op with
- | LNot -> None (* handled by the generic mechanism *)
+ | Evast.LNot -> None (* handled by the generic mechanism *)
| BNot -> None (* No real idea of what should be done *)
| Neg ->
try
diff --git a/src/plugins/eva/values/cvalue_backward.mli b/src/plugins/eva/values/cvalue_backward.mli
index cf2580fa362ebc65637b523906a6178cf5aef014..a965e6f21e4b095f3c687cb7743ca8f7770f2086 100644
--- a/src/plugins/eva/values/cvalue_backward.mli
+++ b/src/plugins/eva/values/cvalue_backward.mli
@@ -34,13 +34,13 @@ val backward_binop:
typ_res:typ ->
res_value: V.t ->
typ_e1:typ ->
- V.t -> binop -> V.t -> (V.t * V.t) option
+ V.t -> Evast.binop -> V.t -> (V.t * V.t) option
(** This function tries to reduce the argument value of an unary operation,
given its result. [typ_arg] is the type of [arg]. *)
val backward_unop:
typ_arg:typ ->
- unop ->
+ Evast.unop ->
arg: V.t ->
res: V.t ->
V.t option
diff --git a/src/plugins/eva/values/cvalue_forward.ml b/src/plugins/eva/values/cvalue_forward.ml
index 58bd04d51691187edecf79c941f99518028f112f..29d864229ac34a313085bf1292c9dff6fc9d65af 100644
--- a/src/plugins/eva/values/cvalue_forward.ml
+++ b/src/plugins/eva/values/cvalue_forward.ml
@@ -377,7 +377,7 @@ let forward_minus_pp ~typ ev1 ev2 =
The function must behave as if it was acting on unbounded integers *)
let forward_binop_int ~typ ev1 op ev2 =
match op with
- | PlusPI -> V.add_untyped ~factor:(Bit_utils.osizeof_pointed typ) ev1 ev2
+ | Evast.PlusPI -> V.add_untyped ~factor:(Bit_utils.osizeof_pointed typ) ev1 ev2
| MinusPI ->
let int_base = Int_Base.neg (Bit_utils.osizeof_pointed typ) in
V.add_untyped ~factor:int_base ev1 ev2
@@ -403,7 +403,7 @@ let forward_binop_int ~typ ev1 op ev2 =
~contains_zero: (V.contains_zero ev1 || V.contains_zero ev2)
~contains_non_zero:(V.contains_non_zero ev1 && V.contains_non_zero ev2)
| Eq | Ne | Ge | Le | Gt | Lt ->
- let op = Eva_utils.conv_comp op in
+ let op = Evast_utils.conv_relation op in
let signed = Bit_utils.is_signed_int_enum_pointer (Cil.unrollType typ) in
V.inject_comp_result (V.forward_comp_int ~signed op ev1 ev2)
@@ -416,12 +416,12 @@ let forward_binop_float fkind ev1 op ev2 =
V.inject_float (f fkind f1 f2)
in
match op with
- | PlusA -> binary_float_floats "+." Fval.add
+ | Evast.PlusA -> binary_float_floats "+." Fval.add
| MinusA -> binary_float_floats "-." Fval.sub
| Mult -> binary_float_floats "*." Fval.mul
| Div -> binary_float_floats "/." Fval.div
| Eq | Ne | Lt | Gt | Le | Ge ->
- let op = Eva_utils.conv_comp op in
+ let op = Evast_utils.conv_relation op in
V.inject_comp_result (Fval.forward_comp op f1 f2)
| _ -> assert false
@@ -448,7 +448,7 @@ let forward_uneg v t =
let forward_unop typ op value =
match op with
- | Neg -> forward_uneg value typ
+ | Evast.Neg -> forward_uneg value typ
| BNot -> begin
match Cil.unrollType typ with
| TInt (ik, _) | TEnum ({ekind=ik}, _) ->
diff --git a/src/plugins/eva/values/cvalue_forward.mli b/src/plugins/eva/values/cvalue_forward.mli
index 2aa6f9d0fbe1e58772d3e2780a5657a1813a41fa..ddc38eeff7406d0b4a95cfc8dfa9174eeca0f90f 100644
--- a/src/plugins/eva/values/cvalue_forward.mli
+++ b/src/plugins/eva/values/cvalue_forward.mli
@@ -34,11 +34,11 @@ val assume_not_nan: assume_finite:bool -> fkind -> V.t -> V.t truth
val assume_pointer: V.t -> V.t truth
val assume_comparable: pointer_comparison -> V.t -> V.t -> (V.t * V.t) truth
-val forward_binop_int: typ: typ -> V.t -> binop -> V.t -> V.t
+val forward_binop_int: typ: typ -> V.t -> Evast.binop -> V.t -> V.t
-val forward_binop_float: Fval.kind -> V.t -> binop -> V.t -> V.t
+val forward_binop_float: Fval.kind -> V.t -> Evast.binop -> V.t -> V.t
-val forward_unop: typ -> unop -> V.t -> V.t
+val forward_unop: typ -> Evast.unop -> V.t -> V.t
val rewrap_integer: Eval_typ.integer_range -> V.t -> V.t
diff --git a/src/plugins/eva/values/main_values.ml b/src/plugins/eva/values/main_values.ml
index d2602ce3480a3dc14e00bbea9e43d7477c5ea7cc..dd492866f09497df0a48aeba494d267c609fed41 100644
--- a/src/plugins/eva/values/main_values.ml
+++ b/src/plugins/eva/values/main_values.ml
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
-
module CVal = struct
include Cvalue.V
@@ -50,10 +48,11 @@ module CVal = struct
let assume_pointer = Cvalue_forward.assume_pointer
let assume_comparable = Cvalue_forward.assume_comparable
- let constant _context exp = function
- | CInt64 (i,_k,_s) -> Cvalue.V.inject_int i
+ let constant _context _exp = function
+ | Evast.CInt64 (i,_k,_s) -> Cvalue.V.inject_int i
| CChr c -> Cvalue.V.inject_int (Cil.charConstToInt c)
- | CWStr _ | CStr _ -> Cvalue.V.inject (Base.of_string_exp exp) Ival.zero
+ | CString base ->
+ Cvalue.V.inject base Ival.zero
| CReal (f, fkind, fstring) ->
Cvalue_forward.eval_float_constant f fkind fstring
| CEnum _ -> assert false
@@ -66,7 +65,7 @@ module CVal = struct
let forward_binop _context typ binop v1 v2 =
let value =
match typ with
- | TFloat (fkind, _) ->
+ | Cil_types.TFloat (fkind, _) ->
Cvalue_forward.forward_binop_float (Fval.kind fkind) v1 binop v2
| TInt _ | TPtr _ | _ as typ ->
Cvalue_forward.forward_binop_int ~typ v1 binop v2
diff --git a/src/plugins/eva/values/offsm_value.ml b/src/plugins/eva/values/offsm_value.ml
index 0ce2bed1fc5bade5c7b8a5b059df7989d9ae1e6b..84f1fa6f6bfd51ced363483407ecfab47c22e506 100644
--- a/src/plugins/eva/values/offsm_value.ml
+++ b/src/plugins/eva/values/offsm_value.ml
@@ -419,8 +419,8 @@ module Offsm
let constant _context e _c =
if store_redundant then
- match Cil.constFoldToInt e with
- | Some i -> inject_int (Cil.typeOf e) i
+ match Evast_utils.fold_to_integer e with
+ | Some i -> inject_int e.typ i
| None -> Top
else Top
@@ -433,7 +433,7 @@ module Offsm
let forward_unop _context _typ op o =
let o' = match o, op with
- | Top, _ | _, (Neg | LNot) -> Top
+ | Top, _ | _, (Evast.Neg | LNot) -> Top
| O o, BNot -> O (bnot o)
in
`Value o'
@@ -441,7 +441,7 @@ module Offsm
let forward_binop _context _typ op o1 o2 =
let o' =
match o1, o2, op with
- | O _o1, O _o2, (Shiftlt | Shiftrt) ->
+ | O _o1, O _o2, (Evast.Shiftlt | Shiftrt) ->
(* It is inconvenient to handle shift here, because we need a
constant for o2 *)
Top
@@ -523,7 +523,7 @@ let () = Abstractions.Hooks.register @@ fun (module Abstraction) ->
let forward_unop context typ op t =
match op with
- | BNot ->
+ | Evast.BNot ->
let t = strengthen_offsm typ t in
let* t = forward_unop context typ op t in
strengthen_v typ t
@@ -531,7 +531,7 @@ let () = Abstractions.Hooks.register @@ fun (module Abstraction) ->
let forward_binop context typ op l r =
match op with
- | BAnd | BOr | BXor ->
+ | Evast.BAnd | BOr | BXor ->
let l = strengthen_offsm typ l
and r = strengthen_offsm typ r in
let* t = forward_binop context typ op l r in
diff --git a/src/plugins/eva/values/sign_value.ml b/src/plugins/eva/values/sign_value.ml
index 89371844af7776c2bf9b786112fe302605c6d5a7..d29ca292ba665e780425c8fffe505501fd1cb73f 100644
--- a/src/plugins/eva/values/sign_value.ml
+++ b/src/plugins/eva/values/sign_value.ml
@@ -103,7 +103,7 @@ let inject_int _ i =
else zero
let constant _context _expr = function
- | CInt64 (i, _, _) -> inject_int () i
+ | Evast.CInt64 (i, _, _) -> inject_int () i
| _ -> top
(* Extracting function pointers from an abstraction. Not implemented
@@ -149,7 +149,7 @@ let logical_not v = { pos = v.zero; neg = false; zero = v.pos || v.neg }
let forward_unop _context typ op v =
match op with
- | Neg -> `Value (neg_unop v)
+ | Evast.Neg -> `Value (neg_unop v)
| BNot -> `Value (bitwise_not typ v)
| LNot -> `Value (logical_not v)
@@ -228,7 +228,7 @@ let logical_or v1 v2 =
let forward_binop _context _typ op v1 v2 =
match op with
- | PlusA -> `Value (plus v1 v2)
+ | Evast.PlusA -> `Value (plus v1 v2)
| MinusA -> `Value (plus v1 (neg_unop v2))
| Mult -> `Value (mul v1 v2)
| Div -> if equal zero v2 then `Bottom else `Value (div v1 v2)
@@ -317,8 +317,8 @@ let backward_comp_right op ~left ~right =
for comparison operators. *)
let backward_binop _ctx ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
match op with
- | Ne | Eq | Le | Lt | Ge | Gt ->
- let op = Eva_utils.conv_comp op in
+ | Evast.Ne | Eq | Le | Lt | Ge | Gt ->
+ let op = Evast_utils.conv_relation op in
if equal zero result then
(* The comparison is false, as it always evaluate to false. Reduce by the
fact that the inverse comparison is true. *)
diff --git a/tests/saveload/oracle/bool.0.res.oracle b/tests/saveload/oracle/bool.0.res.oracle
index d193e342d69221b4cb1adb9cae3f0f96141e6d86..ced50c36135d6d78cf9ee5f883e63852705a49f7 100644
--- a/tests/saveload/oracle/bool.0.res.oracle
+++ b/tests/saveload/oracle/bool.0.res.oracle
@@ -41,8 +41,8 @@
x FROM \nothing
y FROM \nothing
S___fc_stdout[0].__fc_FILE_data
- FROM S___fc_stdout[0]; "%d\n"; "%d\n";
- "%d,%d\n"[bits 0 to 55]; "%d\n"; "%d\n" (and SELF)
+ FROM S___fc_stdout[0]; "%d\n"; "%d\n"; "%d\n"; "%d\n";
+ "%d,%d\n"[bits 0 to 55] (and SELF)
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function f:
@@ -52,5 +52,5 @@
[inout] Out (internal) for function main:
x; y; S___fc_stdout[0].__fc_FILE_data
[inout] Inputs for function main:
- x; y; S___fc_stdout[0]; "%d\n"; "%d\n"; "%d,%d\n"[bits 0 to 55]; "%d\n";
- "%d\n"
+ x; y; S___fc_stdout[0]; "%d\n"; "%d\n"; "%d\n"; "%d\n";
+ "%d,%d\n"[bits 0 to 55]