From 60587cdae80e5612d48e25c4143c1c129b7fc8ce Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 22 Mar 2024 23:47:14 +0100
Subject: [PATCH] [Eva] evast: reorganize the interface to simplify usages
---
src/plugins/eva/api/values_request.ml | 6 +-
src/plugins/eva/ast/eva_automata.ml | 25 +-
src/plugins/eva/ast/evast.ml | 95 +----
src/plugins/eva/ast/evast.mli | 333 ++++++++++++++++++
src/plugins/eva/ast/evast_builder.ml | 194 +++++-----
src/plugins/eva/ast/evast_builder.mli | 63 ----
src/plugins/eva/ast/evast_datatype.ml | 2 +-
src/plugins/eva/ast/evast_datatype.mli | 27 --
src/plugins/eva/ast/evast_printer.ml | 2 +-
src/plugins/eva/ast/evast_printer.mli | 30 --
src/plugins/eva/ast/evast_types.ml | 110 ++++++
src/plugins/eva/ast/evast_typing.ml | 5 +-
src/plugins/eva/ast/evast_typing.mli | 27 --
src/plugins/eva/ast/evast_utils.ml | 97 ++---
src/plugins/eva/ast/evast_utils.mli | 114 ------
src/plugins/eva/ast/evast_visitor.ml | 2 +-
src/plugins/eva/ast/evast_visitor.mli | 69 ----
src/plugins/eva/domains/apron/apron_domain.ml | 4 +-
src/plugins/eva/domains/cvalue/builtins.ml | 4 +-
.../eva/domains/cvalue/builtins_memory.ml | 4 +-
.../eva/domains/cvalue/builtins_misc.ml | 2 +-
.../eva/domains/cvalue/builtins_split.ml | 2 +-
.../eva/domains/cvalue/cvalue_queries.ml | 2 +-
.../eva/domains/cvalue/cvalue_transfer.ml | 4 +-
src/plugins/eva/domains/domain_builder.ml | 4 +-
src/plugins/eva/domains/equality/equality.ml | 4 +-
.../eva/domains/equality/equality_domain.ml | 28 +-
src/plugins/eva/domains/hcexprs.ml | 14 +-
src/plugins/eva/domains/inout_domain.ml | 6 +-
.../eva/domains/multidim/abstract_offset.ml | 10 +-
.../eva/domains/multidim/multidim_domain.ml | 28 +-
.../eva/domains/multidim/segmentation.ml | 8 +-
src/plugins/eva/domains/octagons.ml | 20 +-
src/plugins/eva/domains/printer_domain.ml | 10 +-
src/plugins/eva/domains/symbolic_locs.ml | 14 +-
src/plugins/eva/domains/taint_domain.ml | 10 +-
src/plugins/eva/domains/traces_domain.ml | 12 +-
src/plugins/eva/engine/evaluation.ml | 64 ++--
src/plugins/eva/engine/initialization.ml | 22 +-
src/plugins/eva/engine/iterator.ml | 8 +-
.../eva/engine/subdivided_evaluation.ml | 24 +-
src/plugins/eva/engine/transfer_stmt.ml | 40 +--
src/plugins/eva/eval.ml | 6 +-
src/plugins/eva/gui/gui_eval.ml | 8 +-
src/plugins/eva/gui/register_gui.ml | 2 +-
src/plugins/eva/legacy/eval_terms.ml | 6 +-
.../eva/partitioning/auto_loop_unroll.ml | 19 +-
src/plugins/eva/partitioning/partition.ml | 12 +-
src/plugins/eva/utils/backward_formals.ml | 2 +-
src/plugins/eva/utils/private.ml | 3 -
src/plugins/eva/utils/private.mli | 3 -
src/plugins/eva/utils/results.ml | 17 +-
src/plugins/eva/utils/unit_tests.ml | 8 +-
src/plugins/eva/utils/widen.ml | 6 +-
src/plugins/eva/values/cvalue_backward.ml | 2 +-
src/plugins/eva/values/cvalue_forward.ml | 4 +-
src/plugins/eva/values/offsm_value.ml | 2 +-
src/plugins/eva/values/sign_value.ml | 2 +-
58 files changed, 836 insertions(+), 815 deletions(-)
create mode 100644 src/plugins/eva/ast/evast.mli
delete mode 100644 src/plugins/eva/ast/evast_builder.mli
delete mode 100644 src/plugins/eva/ast/evast_datatype.mli
delete mode 100644 src/plugins/eva/ast/evast_printer.mli
create mode 100644 src/plugins/eva/ast/evast_types.ml
delete mode 100644 src/plugins/eva/ast/evast_typing.mli
delete mode 100644 src/plugins/eva/ast/evast_utils.mli
delete mode 100644 src/plugins/eva/ast/evast_visitor.mli
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 635e56b8847..ac42855caf9 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -489,7 +489,7 @@ 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 cond' = Evast_builder.translate_exp cond in
+ let cond' = Evast.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)
@@ -517,10 +517,10 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let evaluate (term, eval_point) callstack =
match term with
| Plval lval ->
- let lval' = Evast_builder.translate_lval lval in
+ let lval' = Evast.translate_lval lval in
eval_steps lval'.typ (eval_lval lval') eval_point callstack
| Pexpr expr ->
- let expr' = Evast_builder.translate_exp expr in
+ let expr' = Evast.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
diff --git a/src/plugins/eva/ast/eva_automata.ml b/src/plugins/eva/ast/eva_automata.ml
index 85bddc745ac..9762ef0f660 100644
--- a/src/plugins/eva/ast/eva_automata.ml
+++ b/src/plugins/eva/ast/eva_automata.ml
@@ -88,9 +88,9 @@ module Transition = Datatype.Make (struct
function
| Skip -> ()
| Return (None,_) -> fprintf fmt "return"
- | Return (Some exp,_) -> fprintf fmt "return %a" Evast_printer.pp_exp exp
- | Guard (exp,Then,_) -> Evast_printer.pp_exp fmt exp
- | Guard (exp,Else,_) -> fprintf fmt "!(%a)" Evast_printer.pp_exp exp
+ | Return (Some exp,_) -> fprintf fmt "return %a" Evast.pp_exp exp
+ | Guard (exp,Then,_) -> Evast.pp_exp fmt exp
+ | Guard (exp,Else,_) -> fprintf fmt "!(%a)" Evast.pp_exp exp
| Assign (_,_,stmt)
| Call (_,_,_,stmt)
| Init (_,_,stmt)
@@ -182,34 +182,35 @@ let build_wto graph entry_point =
let translate_instr stmt instr =
let translate_call dest callee args _loc =
- let dest' = Option.map Evast_builder.translate_lval dest in
- let callee' = Evast_builder.translate_exp callee in
- let args' = List.map Evast_builder.translate_exp args in
+ let dest' = Option.map translate_lval dest in
+ let callee' = translate_exp callee in
+ let args' = List.map translate_exp args in
Call (dest', callee', args', stmt)
in
match instr with
| Cil_types.Set (lval, exp, _loc) ->
- let lval' = Evast_builder.translate_lval lval in
- let exp' = Evast_builder.translate_exp exp in
+ let lval' = translate_lval lval in
+ let exp' = translate_exp exp in
Assign (lval', exp', stmt)
| Call (dest, callee, args, loc) ->
translate_call dest callee args loc
| Local_init (dest, Cil_types.ConsInit (callee, args, k), loc) ->
Cil.treat_constructor_as_func translate_call dest callee args k loc
| Local_init (vi, Cil_types.AssignInit init, _loc) ->
- let init' = Evast_builder.translate_init init in
+ let init' = translate_init init in
Init (vi, init', stmt)
| Asm (attributes, string_list, ext_asm_opt, _loc) ->
Asm (attributes, string_list, ext_asm_opt, stmt)
| Skip (_loc) | Code_annot (_, _loc) ->
Skip
-let translate_transition = function
+let translate_transition transition =
+ match transition with
| Interpreted_automata.Skip -> Skip
| Return (exp_opt, stmt) ->
- Return (Option.map Evast_builder.translate_exp exp_opt, stmt)
+ Return (Option.map translate_exp exp_opt, stmt)
| Guard (exp, guard_kind, stmt) ->
- Guard (Evast_builder.translate_exp exp, guard_kind, stmt)
+ Guard (translate_exp exp, guard_kind, stmt)
| Prop _ ->
Skip
| Instr (inst, stmt) ->
diff --git a/src/plugins/eva/ast/evast.ml b/src/plugins/eva/ast/evast.ml
index abbb9efed38..c6ad8d675bf 100644
--- a/src/plugins/eva/ast/evast.ml
+++ b/src/plugins/eva/ast/evast.ml
@@ -20,91 +20,10 @@
(* *)
(**************************************************************************)
-open Cil_datatype
-
-(** Eva AST. *)
-
-type origin =
- | Lval of Cil_types.lval
- | Exp of Cil_types.exp
- | Term of Cil_types.identified_term
- | Built (* Not present in the original source code *)
-
-type 'a tag = {
- node: 'a;
- typ: Cil_types.typ;
- origin: origin;
-}
-
-let equal_tag equal_node t1 t2 = equal_node t1.node t2.node
-let compare_tag compare_node t1 t2 = compare_node t1.node t2.node
-
-type typ = Typ.t [@@deriving eq,ord]
-type varinfo = Varinfo.t [@@deriving eq,ord]
-
-type exp = exp_node tag
-
-and exp_node =
- | Const of constant
- | Lval of lval
- | UnOp of unop * exp * typ
- | BinOp of binop * exp * exp * typ
- | CastE of typ * exp
- | AddrOf of lval
- | StartOf of lval
-
-(** Literal constants *)
-and constant =
- | CTopInt of typ (* an unknown integer; currently introduced when sizeof/alignof cannot be evaluated as a constant *)
- | CInt64 of Integer.t * ikind * string option
- | CString of Base.t (* the base must be [Base.String _] *)
- | CChr of char
- | CReal of float * fkind * string option
- | CEnum of Enumitem.t * exp (* the translated expression that this enumitem refers to *)
-
-and lval_node = lhost * offset
-
-and lval = lval_node tag
-
-and lhost =
- | Var of varinfo
- | Mem of exp
-
-and offset =
- | NoOffset
- | Field of Fieldinfo.t * offset
- | Index of exp * offset
-
-and ikind = Cil_types.ikind [@equal (=)] [@compare Stdlib.compare]
-and fkind = Cil_types.fkind [@equal (=)] [@compare Stdlib.compare]
-[@@deriving eq,ord]
-
-
-and unop = Neg | BNot | LNot
-
-and binop =
- | PlusA
- | PlusPI
- | MinusA
- | MinusPI
- | MinusPP
- | Mult
- | Div
- | Mod
- | Shiftlt
- | Shiftrt
- | Lt
- | Gt
- | Le
- | Ge
- | Eq
- | Ne
- | BAnd
- | BXor
- | BOr
- | LAnd
- | LOr
-
-type init =
- | SingleInit of (exp * Cil_types.location)
- | CompoundInit of typ * (offset * init) list
+include Evast_types
+include Evast_typing
+include Evast_printer
+include Evast_datatype
+include Evast_builder
+include Evast_utils
+include Evast_visitor
diff --git a/src/plugins/eva/ast/evast.mli b/src/plugins/eva/ast/evast.mli
new file mode 100644
index 00000000000..cca0eb9a326
--- /dev/null
+++ b/src/plugins/eva/ast/evast.mli
@@ -0,0 +1,333 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Eva Syntax Tree. *)
+
+type origin =
+ | Lval of Cil_types.lval
+ | Exp of Cil_types.exp
+ | Term of Cil_types.identified_term
+ | Built (* Not present in the original source code *)
+
+type 'a tag = private {
+ node: 'a;
+ typ: Cil_types.typ;
+ origin: origin;
+}
+
+type typ = Cil_types.typ
+type varinfo = Cil_types.varinfo
+
+type exp = exp_node tag
+
+and exp_node =
+ | Const of constant
+ | Lval of lval
+ | UnOp of unop * exp * typ
+ | BinOp of binop * exp * exp * typ
+ | CastE of typ * exp
+ | AddrOf of lval
+ | StartOf of lval
+
+(** Literal constants *)
+and constant =
+ | CTopInt of typ (* an unknown integer; currently introduced when sizeof/alignof cannot be evaluated as a constant *)
+ | CInt64 of Integer.t * ikind * string option
+ | CString of Base.t (* the base must be [Base.String _] *)
+ | CChr of char
+ | CReal of float * fkind * string option
+ | CEnum of Cil_types.enumitem * exp (* the translated expression that this enumitem refers to *)
+
+and lval_node = lhost * offset
+
+and lval = lval_node tag
+
+and lhost =
+ | Var of varinfo
+ | Mem of exp
+
+and offset =
+ | NoOffset
+ | Field of Cil_types.fieldinfo * offset
+ | Index of exp * offset
+
+and ikind = Cil_types.ikind
+and fkind = Cil_types.fkind
+
+and unop = Neg | BNot | LNot
+
+and binop =
+ | PlusA
+ | PlusPI
+ | MinusA
+ | MinusPI
+ | MinusPP
+ | Mult
+ | Div
+ | Mod
+ | Shiftlt
+ | Shiftrt
+ | Lt
+ | Gt
+ | Le
+ | Ge
+ | Eq
+ | Ne
+ | BAnd
+ | BXor
+ | BOr
+ | LAnd
+ | LOr
+
+type init =
+ | SingleInit of (exp * Cil_types.location)
+ | CompoundInit of typ * (offset * init) list
+
+
+(* Typing *)
+
+val type_of : 'a tag -> typ
+val type_of_exp_node : exp_node -> typ
+val type_of_lval_node : lval_node -> typ
+val type_of_lhost : lhost -> typ
+
+
+(* Pretty printing *)
+
+val pp_lval : Format.formatter -> lval -> unit
+val pp_offset : Format.formatter -> offset -> unit
+val pp_exp : Format.formatter -> exp -> unit
+val pp_constant : Format.formatter -> constant -> unit
+val pp_unop : Format.formatter -> unop -> unit
+val pp_binop : Format.formatter -> binop -> unit
+
+
+(* Datatypes *)
+
+module Lhost : Datatype.S_with_collections with type t = lhost
+module Offset : Datatype.S_with_collections with type t = offset
+module Lval : Datatype.S_with_collections with type t = lval
+module Exp : Datatype.S_with_collections with type t = exp
+module Constant : Datatype.S_with_collections with type t = constant
+
+
+(* Constructors *)
+
+val mk_exp : exp_node -> exp
+val mk_lval : lval_node -> lval
+
+
+(* Translation from Cil *)
+
+val translate_exp : Cil_types.exp -> exp
+val translate_lval : Cil_types.lval -> lval
+val translate_offset : Cil_types.offset -> offset
+val translate_unop : Cil_types.unop -> unop
+val translate_binop : Cil_types.binop -> binop
+val translate_init : Cil_types.init -> init
+
+
+(** Conversion to Cil *)
+
+val to_cil_exp : exp -> Cil_types.exp
+val to_cil_lval : lval -> Cil_types.lval
+
+
+(* Relations *)
+
+(** Inverse a relation, op must be a comparison operator *)
+val invert_relation : binop -> binop
+
+(** Convert a relation to Abstract_interp.Comp, op must be a comparison
+ operator *)
+val conv_relation : binop -> Abstract_interp.Comp.t
+
+(** [normalize_condition e positive] returns the expression corresponding to
+ [e != 0] when [positive] is true, and [e == 0] otherwise. The
+ resulting expression will always have a comparison operation at its
+ root. *)
+val normalize_condition: exp -> bool -> exp
+
+
+(* Offsets *)
+
+val add_offset: lval -> offset -> lval
+
+
+(* Smart constructors *)
+
+module Build :
+sig
+ val zero: exp
+ val one: exp
+
+ val int: ?kind:Cil_types.ikind -> int -> exp
+ val float: kind:Cil_types.fkind -> float -> exp
+ val integer: ?kind:Cil_types.ikind -> Integer.t -> exp
+ val bool: bool -> exp (* convert booleans to an expression 0 or 1 *)
+
+ val cast: typ -> exp -> exp (* (typ)x *)
+ val binop: binop -> exp -> exp -> exp (* x op y *)
+ val add: exp -> exp -> exp (* x + y *)
+ val eq: exp -> exp -> exp (* x == y *)
+ val ne: exp -> exp -> exp (* x != y *)
+
+ val index: lval -> exp -> lval (* x[y] *)
+ val field: lval -> Cil_types.fieldinfo -> lval (* x.field *)
+ val addr: lval -> exp (* &x *)
+ val mem: exp -> lval (* *x *)
+
+ val var: Cil_types.varinfo -> lval
+ val var_exp: Cil_types.varinfo -> exp
+ val lval: lval -> exp
+end
+
+
+(** Queries *)
+
+val is_mutable : lval -> bool
+val is_initialized : lval -> bool
+
+
+(** Expressions/Lvalue heights *)
+
+(** Computes the height of an expression, that is the maximum number of nested
+ operations in this expression. *)
+val height_exp : exp -> int
+
+(** Computes the height of an lvalue. *)
+val height_lval : lval -> int
+
+
+(** Specialized visitors *)
+
+(** [iter_lvals f exp] calls [f] from every lvalue contained in [exp] *)
+val iter_lvals : (lval -> unit) -> exp -> unit
+
+(** [exp_contains_volatile e] (resp. [lval_contains_volatile lv] is true
+ whenever one l-value contained inside the expression [e] (resp. the lvalue
+ [lv]) has volatile qualifier. Relational analyses should not learn
+ anything on such values. *)
+val exp_contains_volatile : exp -> bool
+val lval_contains_volatile : lval -> bool
+
+val vars_in_exp : exp -> Cil_datatype.Varinfo.Set.t
+val vars_in_lval : lval -> Cil_datatype.Varinfo.Set.t
+
+
+(** Dependences of expressions and lvalues. *)
+
+val zone_of_exp:
+ (lval -> Precise_locs.precise_location) -> exp -> Locations.Zone.t
+(** Given a function computing the location of lvalues, computes the memory zone
+ on which the value of an expression depends. *)
+
+val zone_of_lval:
+ (lval -> Precise_locs.precise_location) -> lval -> Locations.Zone.t
+(** Given a function computing the location of lvalues, computes the memory zone
+ on which the value of an lvalue depends. *)
+
+val indirect_zone_of_lval:
+ (lval -> Precise_locs.precise_location) -> lval -> Locations.Zone.t
+(** Given a function computing the location of lvalues, computes the memory zone
+ on which the offset and the pointer expression (if any) of an lvalue depend.
+*)
+
+val deps_of_exp:
+ (lval -> Precise_locs.precise_location) -> exp -> Deps.t
+(** Given a function computing the location of lvalues, computes the memory
+ dependencies of an expression. *)
+
+val deps_of_lval: (lval -> Precise_locs.precise_location) -> lval -> Deps.t
+(** Given a function computing the location of lvalues, computes the memory
+ dependencies of an lvalue. *)
+
+
+(** Constant conversion and folding. *)
+
+val to_integer : exp -> Integer.t option
+val to_float : exp -> float option
+val is_zero : exp -> bool
+val is_zero_ptr : exp -> bool
+val const_fold: exp -> exp
+val fold_to_integer: exp -> Integer.t option
+
+
+(** Offsets *)
+
+(** Returns the last offset in the chain. *)
+val last_offset: offset -> offset
+
+(** Is an lvalue a bitfield? *)
+val is_bitfield: lval -> bool
+
+
+(** Rewriting visitor *)
+
+module Rewrite :
+sig
+ type visitor = {
+ exp : exp -> exp;
+ lval : lval -> lval;
+ varinfo : varinfo -> varinfo;
+ offset : offset -> offset;
+ }
+
+ type rewriter = {
+ rewrite_exp : visitor:visitor -> exp -> exp;
+ rewrite_lval : visitor:visitor -> lval -> lval;
+ rewrite_varinfo : visitor:visitor -> varinfo -> varinfo;
+ rewrite_offset : visitor:visitor -> offset -> offset;
+ }
+
+ val default : rewriter
+ val visit_exp : rewriter -> exp -> exp
+ val visit_lval : rewriter -> lval -> lval
+end
+
+
+(** Folding visitor *)
+
+module Fold :
+sig
+ type 'a visitor = {
+ neutral : 'a;
+ combine : 'a -> 'a -> 'a;
+ exp : exp -> 'a;
+ lval : lval -> 'a;
+ varinfo : varinfo -> 'a;
+ offset : offset -> 'a;
+ }
+
+ type 'a folder = {
+ fold_exp : visitor:'a visitor -> exp -> 'a;
+ fold_lval : visitor:'a visitor -> lval -> 'a;
+ fold_varinfo : visitor:'a visitor -> varinfo -> 'a;
+ fold_offset : visitor:'a visitor -> offset -> 'a;
+ }
+
+ val default : 'a folder
+ val visit_exp : neutral:'a -> combine:('a -> 'a -> 'a) ->
+ 'a folder -> exp -> 'a
+ val visit_lval : neutral:'a -> combine:('a -> 'a -> 'a) ->
+ 'a folder -> lval -> 'a
+end
diff --git a/src/plugins/eva/ast/evast_builder.ml b/src/plugins/eva/ast/evast_builder.ml
index f63b72009b4..8cbf92119cb 100644
--- a/src/plugins/eva/ast/evast_builder.ml
+++ b/src/plugins/eva/ast/evast_builder.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast
+open Evast_types
(* --- Constructors --- *)
@@ -119,65 +119,29 @@ let rec translate_init = function
CompoundInit (t, List.map translate_field_init l)
-(* --- Smart constructors --- *)
-
-let integer ?kind i = (* TODO: mathematical unbounded integer *)
- let kind = match kind with
- | Some k -> k
- | None ->
- if Cil.fitsInInt IInt i
- then Cil_types.IInt
- else Cil.intKindForValue i false
- in
- let i', _truncated = Cil.truncateInteger64 kind i in
- mk_exp (Const (CInt64 (i', kind, None)))
+(* --- Relations --- *)
-let int ?kind i =
- integer ?kind (Integer.of_int i)
-
-let zero = int 0
-let one = int 1
-let bool = function false -> zero | true -> one
+let invert_relation : binop -> binop = function
+ | Gt -> Le
+ | Lt -> Ge
+ | Le -> Gt
+ | Ge -> Lt
+ | Eq -> Ne
+ | Ne -> Eq
+ | _ -> invalid_arg "invert_relation: must be given a comparison operator"
-let float ~kind f =
- let f =
- if kind = Cil_types.FFloat
- then Floating_point.round_to_single_precision_float f
- else f
- in
- mk_exp (Const (CReal(f,kind,None)))
-
-let cast typ exp =
- if Cil.need_cast exp.typ typ
- then mk_exp (CastE (Cil.type_remove_qualifier_attributes typ, exp))
- else exp
-
-let binop op e1 e2 =
- (* TODO: const folding *)
- match op with
- | PlusA | MinusA | Mult | Div ->
- let t = Cil.arithmeticConversion e1.typ e2.typ in
- mk_exp (BinOp (op,e1,e2,t))
-
- | Eq | Ne | Lt | Le | Ge |Gt ->
- let t =
- if Cil.isArithmeticType e1.typ && Cil.isArithmeticType e2.typ then
- Cil.arithmeticConversion e1.typ e2.typ
- else if Cil.isPointerType e1.typ && Cil.isPointerType e2.typ then
- if Cil.need_cast ~force:true e1.typ e2.typ then
- Cil.theMachine.upointType
- else
- e1.typ
- else
- invalid_arg "unsupported construction"
- in
- mk_exp (BinOp (op, cast t e1, cast t e2, Cil.intType))
+let conv_relation : binop -> Abstract_interp.Comp.t =
+ function
+ | Eq -> Eq
+ | Ne -> Ne
+ | Le -> Le
+ | Lt -> Lt
+ | Ge -> Ge
+ | Gt -> Gt
+ | _ -> invalid_arg "conv_relation: must be given a comparison operator"
- | _ -> invalid_arg "unsupported construction"
-let add = binop PlusA
-let eq = binop Eq
-let ne = binop Ne
+(* --- Offsets --- *)
let rec concat_offset (o1 : offset) (o2 : offset) : offset =
match o1 with
@@ -189,32 +153,96 @@ let add_offset (lval : lval) (offset : offset) : lval =
let (lval_host, lval_offset) = lval.node in
mk_lval (lval_host, concat_offset lval_offset offset)
-let index (base : lval) (index : exp) : lval =
- assert(Cil.isArrayType base.typ);
- add_offset base (Index (index, NoOffset))
-let field (base : lval) (field : Cil_types.fieldinfo) : lval =
- let field_belongs_to_typ fi typ =
- match typ with
- | Cil_types.TComp (ci,_attr) -> ci == fi.Cil_types.fcomp
- | _ -> false
- in
- assert(field_belongs_to_typ field base.typ);
- add_offset base (Field (field, NoOffset))
+(* --- Smart constructors --- *)
-let addr (lval : lval) : exp =
- mk_exp (AddrOf lval)
+module Build =
+struct
+ let integer ?kind i = (* TODO: mathematical unbounded integer *)
+ let kind = match kind with
+ | Some k -> k
+ | None ->
+ if Cil.fitsInInt IInt i
+ then Cil_types.IInt
+ else Cil.intKindForValue i false
+ in
+ let i', _truncated = Cil.truncateInteger64 kind i in
+ mk_exp (Const (CInt64 (i', kind, None)))
-let mem (exp : exp) : lval =
- match exp.node with
- | AddrOf lv -> lv
- | StartOf lv -> index lv zero (* Must be an array *)
- | _ -> mk_lval (Mem exp, NoOffset)
+ let int ?kind i =
+ integer ?kind (Integer.of_int i)
-let var vi = mk_lval (Var vi, NoOffset)
-let var_exp vi = mk_exp (Lval (var vi))
+ let zero = int 0
+ let one = int 1
+ let bool = function false -> zero | true -> one
-let lval lv = { lv with node=Lval lv }
+ let float ~kind f =
+ let f =
+ if kind = Cil_types.FFloat
+ then Floating_point.round_to_single_precision_float f
+ else f
+ in
+ mk_exp (Const (CReal(f,kind,None)))
+
+ let cast typ exp =
+ if Cil.need_cast exp.typ typ
+ then mk_exp (CastE (Cil.type_remove_qualifier_attributes typ, exp))
+ else exp
+
+ let binop op e1 e2 =
+ (* TODO: const folding *)
+ match op with
+ | PlusA | MinusA | Mult | Div ->
+ let t = Cil.arithmeticConversion e1.typ e2.typ in
+ mk_exp (BinOp (op,e1,e2,t))
+
+ | Eq | Ne | Lt | Le | Ge |Gt ->
+ let t =
+ if Cil.isArithmeticType e1.typ && Cil.isArithmeticType e2.typ then
+ Cil.arithmeticConversion e1.typ e2.typ
+ else if Cil.isPointerType e1.typ && Cil.isPointerType e2.typ then
+ if Cil.need_cast ~force:true e1.typ e2.typ then
+ Cil.theMachine.upointType
+ else
+ e1.typ
+ else
+ invalid_arg "unsupported construction"
+ in
+ mk_exp (BinOp (op, cast t e1, cast t e2, Cil.intType))
+
+ | _ -> invalid_arg "unsupported construction"
+
+ let add = binop PlusA
+ let eq = binop Eq
+ let ne = binop Ne
+
+ let index (base : lval) (index : exp) : lval =
+ assert(Cil.isArrayType base.typ);
+ add_offset base (Index (index, NoOffset))
+
+ let field (base : lval) (field : Cil_types.fieldinfo) : lval =
+ let field_belongs_to_typ fi typ =
+ match typ with
+ | Cil_types.TComp (ci,_attr) -> ci == fi.Cil_types.fcomp
+ | _ -> false
+ in
+ assert(field_belongs_to_typ field base.typ);
+ add_offset base (Field (field, NoOffset))
+
+ let addr (lval : lval) : exp =
+ mk_exp (AddrOf lval)
+
+ let mem (exp : exp) : lval =
+ match exp.node with
+ | AddrOf lv -> lv
+ | StartOf lv -> index lv zero (* Must be an array *)
+ | _ -> mk_lval (Mem exp, NoOffset)
+
+ let var vi = mk_lval (Var vi, NoOffset)
+ let var_exp vi = mk_exp (Lval (var vi))
+
+ let lval lv = { lv with node=Lval lv }
+end
(* --- Condition normalization --- *)
@@ -227,20 +255,10 @@ let zero_typed (typ : Cil_types.typ) =
| TPtr _ ->
let ik = Cil.(theMachine.upointKind) in
let zero = mk_exp (Const (CInt64 (Integer.zero, ik, None))) in
- cast typ zero
+ Build.cast typ zero
| typ ->
Self.fatal ~current:true "non-scalar type %a" Printer.pp_typ typ
-(* duplicate of Evast_utils.invert_relation; needs to be removed *)
-let invert_relation : binop -> binop = function
- | Gt -> Le
- | Lt -> Ge
- | Le -> Gt
- | Ge -> Lt
- | Eq -> Ne
- | Ne -> Eq
- | _ -> invalid_arg "invert_relation: must be given a comparison operator"
-
(* Transform an expression supposed to be [positive] into an equivalent
one in which the root expression is a comparison operator. *)
let rec normalize_condition exp positive =
diff --git a/src/plugins/eva/ast/evast_builder.mli b/src/plugins/eva/ast/evast_builder.mli
deleted file mode 100644
index e6351438f61..00000000000
--- a/src/plugins/eva/ast/evast_builder.mli
+++ /dev/null
@@ -1,63 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Evast
-
-val translate_exp: Cil_types.exp -> exp
-val translate_lval: Cil_types.lval -> lval
-val translate_offset: Cil_types.offset -> offset
-val translate_unop: Cil_types.unop -> unop
-val translate_binop: Cil_types.binop -> binop
-val translate_init: Cil_types.init -> init
-
-val mk_exp: exp_node -> exp (* Does not assign origin. Should not be used. *)
-val mk_lval: lval_node -> lval
-
-val zero: exp
-val one: exp
-
-val int: ?kind:Cil_types.ikind -> int -> exp
-val float: kind:Cil_types.fkind -> float -> exp
-val integer: ?kind:Cil_types.ikind -> Integer.t -> exp
-val bool: bool -> exp (* convert booleans to an expression 0 or 1 *)
-
-val cast: typ -> exp -> exp (* (typ)x *)
-val binop: binop -> exp -> exp -> exp (* x op y *)
-val add: exp -> exp -> exp (* x + y *)
-val eq: exp -> exp -> exp (* x == y *)
-val ne: exp -> exp -> exp (* x != y *)
-
-val add_offset: lval -> offset -> lval
-val index: lval -> exp -> lval (* x[y] *)
-val field: lval -> Cil_types.fieldinfo -> lval (* x.field *)
-val addr: lval -> exp (* &x *)
-val mem: exp -> lval (* *x *)
-
-val var: Cil_types.varinfo -> lval
-val var_exp: Cil_types.varinfo -> exp
-val lval: lval -> exp
-
-val normalize_condition: exp -> bool -> exp
-(** [normalize_condition e positive] returns the expression corresponding to
- [e != 0] when [positive] is true, and [e == 0] otherwise. The
- resulting expression will always have a comparison operation at its
- root. *)
diff --git a/src/plugins/eva/ast/evast_datatype.ml b/src/plugins/eva/ast/evast_datatype.ml
index 59da247861d..4bdceeb4ff4 100644
--- a/src/plugins/eva/ast/evast_datatype.ml
+++ b/src/plugins/eva/ast/evast_datatype.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast
+open Evast_types
module Typ = Cil_datatype.Typ
module Varinfo = Cil_datatype.Varinfo
diff --git a/src/plugins/eva/ast/evast_datatype.mli b/src/plugins/eva/ast/evast_datatype.mli
deleted file mode 100644
index c0b889388a4..00000000000
--- a/src/plugins/eva/ast/evast_datatype.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-module Lhost : Datatype.S_with_collections with type t = Evast.lhost
-module Offset : Datatype.S_with_collections with type t = Evast.offset
-module Lval : Datatype.S_with_collections with type t = Evast.lval
-module Exp : Datatype.S_with_collections with type t = Evast.exp
-module Constant : Datatype.S_with_collections with type t = Evast.constant
diff --git a/src/plugins/eva/ast/evast_printer.ml b/src/plugins/eva/ast/evast_printer.ml
index b5fcf76e70f..c1031160c96 100644
--- a/src/plugins/eva/ast/evast_printer.ml
+++ b/src/plugins/eva/ast/evast_printer.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast
+open Evast_types
module Precedence =
struct
diff --git a/src/plugins/eva/ast/evast_printer.mli b/src/plugins/eva/ast/evast_printer.mli
deleted file mode 100644
index e0fb7d530bd..00000000000
--- a/src/plugins/eva/ast/evast_printer.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Evast
-
-val pp_lval : Format.formatter -> lval -> unit
-val pp_offset : Format.formatter -> offset -> unit
-val pp_exp : Format.formatter -> exp -> unit
-val pp_constant : Format.formatter -> constant -> unit
-val pp_unop : Format.formatter -> unop -> unit
-val pp_binop : Format.formatter -> binop -> unit
diff --git a/src/plugins/eva/ast/evast_types.ml b/src/plugins/eva/ast/evast_types.ml
new file mode 100644
index 00000000000..01d839c3df9
--- /dev/null
+++ b/src/plugins/eva/ast/evast_types.ml
@@ -0,0 +1,110 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_datatype
+
+(** Eva AST. *)
+
+type origin =
+ | Lval of Cil_types.lval
+ | Exp of Cil_types.exp
+ | Term of Cil_types.identified_term
+ | Built (* Not present in the original source code *)
+
+type 'a tag = {
+ node: 'a;
+ typ: Cil_types.typ;
+ origin: origin;
+}
+
+let equal_tag equal_node t1 t2 = equal_node t1.node t2.node
+let compare_tag compare_node t1 t2 = compare_node t1.node t2.node
+
+type typ = Typ.t [@@deriving eq,ord]
+type varinfo = Varinfo.t [@@deriving eq,ord]
+
+type exp = exp_node tag
+
+and exp_node =
+ | Const of constant
+ | Lval of lval
+ | UnOp of unop * exp * typ
+ | BinOp of binop * exp * exp * typ
+ | CastE of typ * exp
+ | AddrOf of lval
+ | StartOf of lval
+
+(** Literal constants *)
+and constant =
+ | CTopInt of typ (* an unknown integer; currently introduced when sizeof/alignof cannot be evaluated as a constant *)
+ | CInt64 of Integer.t * ikind * string option
+ | CString of Base.t (* the base must be [Base.String _] *)
+ | CChr of char
+ | CReal of float * fkind * string option
+ | CEnum of Enumitem.t * exp (* the translated expression that this enumitem refers to *)
+
+and lval_node = lhost * offset
+
+and lval = lval_node tag
+
+and lhost =
+ | Var of varinfo
+ | Mem of exp
+
+and offset =
+ | NoOffset
+ | Field of Fieldinfo.t * offset
+ | Index of exp * offset
+
+and ikind = Cil_types.ikind [@equal (=)] [@compare Stdlib.compare]
+and fkind = Cil_types.fkind [@equal (=)] [@compare Stdlib.compare]
+[@@deriving eq,ord]
+
+
+and unop = Neg | BNot | LNot
+
+and binop =
+ | PlusA
+ | PlusPI
+ | MinusA
+ | MinusPI
+ | MinusPP
+ | Mult
+ | Div
+ | Mod
+ | Shiftlt
+ | Shiftrt
+ | Lt
+ | Gt
+ | Le
+ | Ge
+ | Eq
+ | Ne
+ | BAnd
+ | BXor
+ | BOr
+ | LAnd
+ | LOr
+
+type init =
+ | SingleInit of (exp * Cil_types.location)
+ | CompoundInit of typ * (offset * init) list
diff --git a/src/plugins/eva/ast/evast_typing.ml b/src/plugins/eva/ast/evast_typing.ml
index 6b1f3bd6422..549fe90b2fe 100644
--- a/src/plugins/eva/ast/evast_typing.ml
+++ b/src/plugins/eva/ast/evast_typing.ml
@@ -20,7 +20,10 @@
(* *)
(**************************************************************************)
-open Evast
+open Evast_types
+
+let type_of node =
+ node.typ
let type_of_const : constant -> typ = function
| CTopInt t -> t
diff --git a/src/plugins/eva/ast/evast_typing.mli b/src/plugins/eva/ast/evast_typing.mli
deleted file mode 100644
index 685903992ff..00000000000
--- a/src/plugins/eva/ast/evast_typing.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Evast
-
-val type_of_exp_node : exp_node -> typ
-val type_of_lval_node : lval_node -> typ
-val type_of_lhost : lhost -> typ
diff --git a/src/plugins/eva/ast/evast_utils.ml b/src/plugins/eva/ast/evast_utils.ml
index 9dcf3289310..044e19099fb 100644
--- a/src/plugins/eva/ast/evast_utils.ml
+++ b/src/plugins/eva/ast/evast_utils.ml
@@ -20,7 +20,8 @@
(* *)
(**************************************************************************)
-open Evast
+open Evast_types
+open Evast_builder
(* --- Conversion to Cil --- *)
@@ -173,28 +174,6 @@ and height_offset = function
| Index (e,r) -> max (height_exp e) (height_offset r) + 1
-(* --- Relation inversion --- *)
-
-let invert_relation : binop -> binop = function
- | Gt -> Le
- | Lt -> Ge
- | Le -> Gt
- | Ge -> Lt
- | Eq -> Ne
- | Ne -> Eq
- | _ -> invalid_arg "invert_relation: must be given a comparison operator"
-
-let conv_relation : binop -> Abstract_interp.Comp.t =
- function
- | Eq -> Eq
- | Ne -> Ne
- | Le -> Le
- | Lt -> Lt
- | Ge -> Ge
- | Gt -> Gt
- | _ -> invalid_arg "conv_relation: must be given a comparison operator"
-
-
(* --- Specialized visitors --- *)
let iter_lvals f =
@@ -312,9 +291,8 @@ let is_zero_ptr exp =
(* These functions are largely based on Cil.constFold. See there for details. *)
let rec const_fold (exp: exp) : exp =
- let open Evast_builder in
match exp.node with
- | Const (CChr c) -> integer (Cil.charConstToInt c)
+ | Const (CChr c) -> Build.integer (Cil.charConstToInt c)
| Const (CEnum(_ei, e)) -> const_fold e
| Const (CTopInt _ | CReal _ | CString _ | CInt64 _) -> exp
| Lval lv -> mk_exp (Lval (const_fold_lval lv))
@@ -325,7 +303,6 @@ let rec const_fold (exp: exp) : exp =
| BinOp (op, e1, e2, t) -> const_fold_binop op e1 e2 t
and const_fold_cast (t : typ) (e : exp) : exp =
- let open Evast_builder in
let e' = const_fold e in
let t' = Cil.(type_remove_attributes_for_c_cast (unrollType t)) in
let default () = mk_exp (CastE (t, e')) in
@@ -333,38 +310,37 @@ and const_fold_cast (t : typ) (e : exp) : exp =
(* integer -> integer *)
| Const (CInt64 (i,_k,_)), (TInt (ik, a) | TEnum ({ekind = ik}, a))
when a = [] ->
- integer ~kind:ik i
+ Build.integer ~kind:ik i
(* real -> integer *)
| Const (CReal (f,_,_)), (TInt(kind, a) | TEnum ({ekind = kind}, a))
when a = [] ->
begin try
let i = Floating_point.truncate_to_integer f in
if Cil.fitsInInt kind i
- then integer ~kind i
+ then Build.integer ~kind i
else default ()
with Floating_point.Float_Non_representable_as_Int64 _ ->
default ()
end
(* real -> float *)
| Const (CReal (f,_,_)), TFloat (kind, a) when a = [] ->
- float ~kind f
+ Build.float ~kind f
(* int -> float *)
| Const (CInt64(i,_,_)), (TFloat (kind, a)) when a = [] ->
let f = Integer.to_float i in
- float ~kind f
+ Build.float ~kind f
| _, _ -> default ()
and const_fold_unop (op : unop) (e : exp) (t : typ) : exp =
- let open Evast_builder in
let e' = const_fold e in
let default () = mk_exp (UnOp (op, e', t)) in
match e'.node, Cil.unrollType t with
(* Integer operations *)
| Const (CInt64 (i,_ik,_repr)), (TInt (ik, _) | TEnum ({ekind=ik},_)) ->
begin match op with
- | Neg -> integer ~kind:ik (Integer.neg i)
- | BNot -> integer ~kind:ik (Integer.lognot i)
- | LNot -> if Integer.(equal i zero) then int 1 else int 0
+ | Neg -> Build.integer ~kind:ik (Integer.neg i)
+ | BNot -> Build.integer ~kind:ik (Integer.lognot i)
+ | LNot -> if Integer.(equal i zero) then Build.int 1 else Build.int 0
end
(* Float operations*)
| Const (CReal(f,_,_)), TFloat (fk,_) ->
@@ -382,7 +358,6 @@ and const_fold_unop (op : unop) (e : exp) (t : typ) : exp =
and const_fold_binop (op : binop) (e1 : exp) (e2 : exp) (t : typ) : exp =
(* TODO: float comparisons *)
- let open Evast_builder in
let e1' = const_fold e1 in
let e2' = const_fold e2 in
let default () = mk_exp (BinOp (op, e1', e2', t)) in
@@ -402,87 +377,87 @@ and const_fold_binop (op : binop) (e1 : exp) (e2 : exp) (t : typ) : exp =
| PlusPI, _, Some z when Integer.is_zero z -> e1'
| MinusPI, _, Some z when Integer.is_zero z -> e1'
| PlusA, Some i1, Some i2 ->
- integer ~kind (Integer.add i1 i2)
+ Build.integer ~kind (Integer.add i1 i2)
| MinusA, Some i1, Some i2 ->
- integer ~kind (Integer.sub i1 i2)
+ Build.integer ~kind (Integer.sub i1 i2)
| Mult, Some i1, Some i2 ->
- integer ~kind (Integer.mul i1 i2)
+ Build.integer ~kind (Integer.mul i1 i2)
| Mult, Some z, _ when Integer.is_zero z -> e1'
| Mult, Some i1, _ when Integer.is_one i1 -> e2'
| Mult, _, Some z when Integer.is_zero z -> e2'
| Mult, _, Some i2 when Integer.is_one i2 -> e1'
| Div, Some i1, Some i2 ->
begin
- try integer ~kind (Integer.c_div i1 i2)
+ try Build.integer ~kind (Integer.c_div i1 i2)
with Division_by_zero -> default ()
end
| Div, _, Some i2 when Integer.is_one i2 -> e1'
| Mod, Some i1, Some i2 ->
begin
- try integer ~kind (Integer.c_rem i1 i2)
+ try Build.integer ~kind (Integer.c_rem i1 i2)
with Division_by_zero -> default ()
end
| BAnd, Some i1, Some i2 ->
- integer ~kind (Integer.logand i1 i2)
+ Build.integer ~kind (Integer.logand i1 i2)
| BAnd, Some z, _ when Integer.is_zero z -> e1'
| BAnd, _, Some z when Integer.is_zero z -> e2'
| BOr, Some i1, Some i2 ->
- integer ~kind (Integer.logor i1 i2)
+ Build.integer ~kind (Integer.logor i1 i2)
| BOr, Some z, _ when Integer.is_zero z -> e2'
| BOr, _, Some z when Integer.is_zero z -> e1'
| BXor, Some i1, Some i2 ->
- integer ~kind (Integer.logxor i1 i2)
+ Build.integer ~kind (Integer.logxor i1 i2)
| Shiftlt, Some i1, Some i2 when shift_in_bounds i2 ->
- integer ~kind (Integer.shift_left i1 i2)
+ Build.integer ~kind (Integer.shift_left i1 i2)
| Shiftlt, Some z, _ when Integer.is_zero z -> e1'
| Shiftlt, _, Some z when Integer.is_zero z -> e1'
| Shiftrt, Some i1, Some i2 when shift_in_bounds i2 ->
if Cil.isSigned kind then
- integer ~kind (Integer.shift_right i1 i2)
+ Build.integer ~kind (Integer.shift_right i1 i2)
else
- integer ~kind (Integer.shift_right_logical i1 i2)
+ Build.integer ~kind (Integer.shift_right_logical i1 i2)
| Shiftrt, Some z, _ when Integer.is_zero z -> e1'
| Shiftrt, _, Some z when Integer.is_zero z -> e1'
| Eq, Some i1, Some i2 ->
- bool (Integer.equal i1 i2)
+ Build.bool (Integer.equal i1 i2)
| Ne, Some i1, Some i2 ->
- bool (not (Integer.equal i1 i2))
+ Build.bool (not (Integer.equal i1 i2))
| Le, Some i1, Some i2 ->
- bool (Integer.le i1 i2)
+ Build.bool (Integer.le i1 i2)
| Ge, Some i1, Some i2 ->
- bool (Integer.ge i1 i2)
+ Build.bool (Integer.ge i1 i2)
| Lt, Some i1, Some i2 ->
- bool (Integer.lt i1 i2)
+ Build.bool (Integer.lt i1 i2)
| Gt, Some i1, Some i2 ->
- bool (Integer.gt i1 i2)
+ Build.bool (Integer.gt i1 i2)
| LAnd, Some i1, _ ->
- if Integer.is_zero i1 then zero else e2'
+ if Integer.is_zero i1 then Build.zero else e2'
| LAnd, _, Some i2 ->
- if Integer.is_zero i2 then zero else e1'
+ if Integer.is_zero i2 then Build.zero else e1'
| LOr, Some i1, _ ->
- if Integer.is_zero i1 then e2' else one
+ if Integer.is_zero i1 then e2' else Build.one
| LOr, _, Some i2 ->
- if Integer.is_zero i2 then e1' else one
+ if Integer.is_zero i2 then e1' else Build.one
| _ -> default ()
end
(* Floating-point operation *)
| TFloat (fk, _) ->
begin match op, to_float e1', to_float e2' with
| PlusA, Some f1, Some f2 ->
- float ~kind:fk (f1 +. f2)
+ Build.float ~kind:fk (f1 +. f2)
| MinusA, Some f1, Some f2 ->
- float ~kind:fk (f1 -. f2)
+ Build.float ~kind:fk (f1 -. f2)
| Mult, Some f1, Some f2 ->
- float ~kind:fk (f1 *. f2)
+ Build.float ~kind:fk (f1 *. f2)
| Div, Some f1, Some f2 ->
- float ~kind:fk (f1 /. f2)
+ Build.float ~kind:fk (f1 /. f2)
| _ -> default ()
end
| _ -> default ()
and const_fold_lval (lval : lval) : lval =
let lhost, offset = lval.node in
- Evast_builder.mk_lval (const_fold_lhost lhost, const_fold_offset offset)
+ mk_lval (const_fold_lhost lhost, const_fold_offset offset)
and const_fold_lhost : lhost -> lhost = function
| Mem e -> Mem (const_fold e)
diff --git a/src/plugins/eva/ast/evast_utils.mli b/src/plugins/eva/ast/evast_utils.mli
deleted file mode 100644
index 3b7e1196063..00000000000
--- a/src/plugins/eva/ast/evast_utils.mli
+++ /dev/null
@@ -1,114 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** *)
-
-open Evast
-
-(** Conversion to Cil *)
-
-val to_cil_exp : exp -> Cil_types.exp
-val to_cil_lval : lval -> Cil_types.lval
-
-
-(** Queries *)
-
-val is_mutable : lval -> bool
-val is_initialized : lval -> bool
-
-
-(** Expressions/Lvalue heights *)
-
-(** Computes the height of an expression, that is the maximum number of nested
- operations in this expression. *)
-val height_exp : exp -> int
-
-(** Computes the height of an lvalue. *)
-val height_lval : lval -> int
-
-(** Relations *)
-
-(** Inverse a relation, op must be a comparison operator *)
-val invert_relation : binop -> binop
-
-(** Convert a relation to Abstract_interp.Comp, op must be a comparison
- operator *)
-val conv_relation : binop -> Abstract_interp.Comp.t
-
-(** Specialized visitors *)
-
-(** [iter_lvals f exp] calls [f] from every lvalue contained in [exp] *)
-val iter_lvals : (lval -> unit) -> exp -> unit
-
-(** [exp_contains_volatile e] (resp. [lval_contains_volatile lv] is true
- whenever one l-value contained inside the expression [e] (resp. the lvalue
- [lv]) has volatile qualifier. Relational analyses should not learn
- anything on such values. *)
-val exp_contains_volatile : exp -> bool
-val lval_contains_volatile : lval -> bool
-
-val vars_in_exp : exp -> Cil_datatype.Varinfo.Set.t
-val vars_in_lval : lval -> Cil_datatype.Varinfo.Set.t
-
-(** Dependences of expressions and lvalues. *)
-
-val zone_of_exp:
- (lval -> Precise_locs.precise_location) -> exp -> Locations.Zone.t
-(** Given a function computing the location of lvalues, computes the memory zone
- on which the value of an expression depends. *)
-
-val zone_of_lval:
- (lval -> Precise_locs.precise_location) -> lval -> Locations.Zone.t
-(** Given a function computing the location of lvalues, computes the memory zone
- on which the value of an lvalue depends. *)
-
-val indirect_zone_of_lval:
- (lval -> Precise_locs.precise_location) -> lval -> Locations.Zone.t
-(** Given a function computing the location of lvalues, computes the memory zone
- on which the offset and the pointer expression (if any) of an lvalue depend.
-*)
-
-val deps_of_exp:
- (lval -> Precise_locs.precise_location) -> exp -> Deps.t
-(** Given a function computing the location of lvalues, computes the memory
- dependencies of an expression. *)
-
-val deps_of_lval: (lval -> Precise_locs.precise_location) -> lval -> Deps.t
-(** Given a function computing the location of lvalues, computes the memory
- dependencies of an lvalue. *)
-
-(** Constant conversion and folding. *)
-
-val to_integer : exp -> Integer.t option
-val to_float : exp -> float option
-val is_zero : exp -> bool
-val is_zero_ptr : exp -> bool
-val const_fold: exp -> exp
-val fold_to_integer: exp -> Integer.t option
-
-(** Offsets *)
-
-(** Returns the last offset in the chain. *)
-val last_offset: offset -> offset
-
-(** Is an lvalue a bitfield? *)
-val is_bitfield: lval -> bool
diff --git a/src/plugins/eva/ast/evast_visitor.ml b/src/plugins/eva/ast/evast_visitor.ml
index 95fc07eee4c..f76a90a717a 100644
--- a/src/plugins/eva/ast/evast_visitor.ml
+++ b/src/plugins/eva/ast/evast_visitor.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast
+open Evast_types
module Rewrite =
struct
diff --git a/src/plugins/eva/ast/evast_visitor.mli b/src/plugins/eva/ast/evast_visitor.mli
deleted file mode 100644
index 37af5b10596..00000000000
--- a/src/plugins/eva/ast/evast_visitor.mli
+++ /dev/null
@@ -1,69 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Evast
-
-module Rewrite :
-sig
- type visitor = {
- exp : exp -> exp;
- lval : lval -> lval;
- varinfo : varinfo -> varinfo;
- offset : offset -> offset;
- }
-
- type rewriter = {
- rewrite_exp : visitor:visitor -> exp -> exp;
- rewrite_lval : visitor:visitor -> lval -> lval;
- rewrite_varinfo : visitor:visitor -> varinfo -> varinfo;
- rewrite_offset : visitor:visitor -> offset -> offset;
- }
-
- val default : rewriter
- val visit_exp : rewriter -> exp -> exp
- val visit_lval : rewriter -> lval -> lval
-end
-
-module Fold :
-sig
- type 'a visitor = {
- neutral : 'a;
- combine : 'a -> 'a -> 'a;
- exp : exp -> 'a;
- lval : lval -> 'a;
- varinfo : varinfo -> 'a;
- offset : offset -> 'a;
- }
-
- type 'a folder = {
- fold_exp : visitor:'a visitor -> exp -> 'a;
- fold_lval : visitor:'a visitor -> lval -> 'a;
- fold_varinfo : visitor:'a visitor -> varinfo -> 'a;
- fold_offset : visitor:'a visitor -> offset -> 'a;
- }
-
- val default : 'a folder
- val visit_exp : neutral:'a -> combine:('a -> 'a -> 'a) ->
- 'a folder -> exp -> 'a
- val visit_lval : neutral:'a -> combine:('a -> 'a -> 'a) ->
- 'a folder -> lval -> 'a
-end
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index b683c7341b0..eeed011cf15 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -287,7 +287,7 @@ let rec constraint_expr eval oracle env expr positive =
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 = Evast_utils.conv_relation binop in
+ let binop = Evast.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")
@@ -495,7 +495,7 @@ module Make (Man : Input) = struct
compute state expr
let extract_lval ~oracle:_ _context state lval _loc =
- let expr = Evast_builder.lval lval in
+ let expr = Evast.Build.lval lval in
compute state expr
let maybe_bottom state =
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 268fc9925b6..3a11ebaa7da 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.map (fun (exp, v) -> Evast_utils.to_cil_exp exp, v) (list @ rest)
+ List.map (fun (exp, v) -> Evast.to_cil_exp exp, v) (list @ rest)
let process_result call state call_result =
let clob = Locals_scoping.bottom () in
@@ -254,7 +254,7 @@ 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
- let lval_ret = Evast_builder.var vi_ret in
+ let lval_ret = Evast.Build.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? *)
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 1173be96001..804e2a4533f 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 -> Evast_builder.translate_lval lval
+ | AddrOf lval -> Evast.translate_lval lval
| CastE (_typ, exp) -> lval_of_address exp
- | _ -> Evast_builder.mem (Evast_builder.translate_exp exp)
+ | _ -> Evast.(Build.mem (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 18114892b1f..be71a62ae76 100644
--- a/src/plugins/eva/domains/cvalue/builtins_misc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_misc.ml
@@ -37,7 +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 arg_exp = Evast.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 8bf921c0940..97e59e12cb4 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_split.ml
@@ -74,7 +74,7 @@ let warning warn s =
[max_card] elements. *)
let split_v ~warn lv state max_card =
if Cil.isArithmeticOrPointerType (Cil.typeOfLval lv) then
- let lv' = Evast_builder.translate_lval lv in
+ let lv' = Evast.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
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index 132dd760ff5..4d0c162429a 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -45,7 +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
+ let lval = Evast.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_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 938b3b82daf..76d912877af 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -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 Evast_printer.pp_lval lval (Origin.descr origin)
+ prefix pp_lval lval (Origin.descr origin)
Eva_utils.pp_callstack
| _ -> ()
@@ -218,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 (Evast_builder.var arg.formal) offsm;
+ warn_imprecise_offsm_write (Build.var arg.formal) offsm;
Cvalue.Model.add_base (Base.of_varinfo arg.formal) offsm state
in
List.fold_left treat_one_formal state arguments
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index 846e1cb5b5e..57ac9c2a525 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 = Evast_builder.var varinfo in
+ let lval = Evast.Build.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 = Evast_builder.var varinfo in
+ let lval = Evast.Build.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 3295cf02364..f84f9b54164 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 = Evast_utils.height_exp elt in
+ let h = Evast.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 = Evast_utils.height_exp current in
+ let height = Evast.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_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index cc6cd8afeee..3030dff7750 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -200,7 +200,7 @@ struct
Equality.Equality.fold
(fun atom acc ->
let e = HCE.to_exp atom in
- if Evast_datatype.Exp.equal e expr
+ if Evast.Exp.equal e expr
then acc else (e, value) :: acc)
equality []
| None -> []
@@ -240,7 +240,7 @@ struct
| None -> `Value (Value.top, None), Alarmset.all
let extract_expr ~oracle _context (equalities, _, _) expr =
- let expr = Evast_utils.const_fold expr in
+ let expr = Evast.const_fold expr in
let atom_e = HCE.of_exp expr in
coop_eval oracle equalities atom_e
@@ -322,8 +322,8 @@ struct
match lv.node with
| Var vi, NoOffset -> Locations.zone_of_varinfo vi
| _ ->
- let expr = Evast_builder.lval lv in
- Evast_utils.zone_of_exp (find_loc valuation) expr
+ let expr = Evast.Build.lval lv in
+ Evast.zone_of_exp (find_loc valuation) expr
in
Deps.add lval zone deps
@@ -379,8 +379,8 @@ 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 Evast_utils.lval_contains_volatile left_lval ||
- Evast_utils.exp_contains_volatile right_expr ||
+ if Evast.lval_contains_volatile left_lval ||
+ Evast.exp_contains_volatile right_expr ||
not (Cil.isArithmeticOrPointerType left_lval.typ) ||
indeterminate_copy value
then state
@@ -401,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 = Evast_utils.const_fold right_expr in
+ let right_expr = Evast.const_fold right_expr in
try
let indirect_left_zone =
- Evast_utils.indirect_zone_of_lval (find_loc valuation) left_value.lval
+ Evast.indirect_zone_of_lval (find_loc valuation) left_value.lval
and right_zone =
- Evast_utils.zone_of_exp (find_loc valuation) right_expr
+ Evast.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,
@@ -431,7 +431,7 @@ struct
state
else
try
- let left_value = Evast_builder.var arg.formal in
+ let left_value = Evast.Build.var arg.formal in
assign_eq left_value arg.concrete arg.avalue valuation state
with Top_location -> state
in
@@ -453,10 +453,10 @@ struct
if not (is_safe_equality valuation e1 e2)
then `Value state
else
- 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
+ let e1 = Evast.const_fold e1
+ and e2 = Evast.const_fold e2 in
+ if Evast.exp_contains_volatile e1
+ || Evast.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)
diff --git a/src/plugins/eva/domains/hcexprs.ml b/src/plugins/eva/domains/hcexprs.ml
index e3a9ed02316..b7de1ba5084 100644
--- a/src/plugins/eva/domains/hcexprs.ml
+++ b/src/plugins/eva/domains/hcexprs.ml
@@ -20,8 +20,8 @@
(* *)
(**************************************************************************)
-module Exp = Evast_datatype.Exp
-module Lval = Evast_datatype.Lval
+module Exp = Evast.Exp
+module Lval = Evast.Lval
(* lvalues are never stored under a constructor [E]. *)
type unhashconsed_exprs = E of Exp.t | LV of Lval.t
@@ -41,7 +41,7 @@ module E = struct
type t = unhashconsed_exprs
let name = "Value.Symbolic_exprs.key"
- let reprs = List.map (fun e -> E e) Evast_datatype.Exp.reprs
+ let reprs = List.map (fun e -> E e) Exp.reprs
let structural_descr =
Structural_descr.t_sum
@@ -70,7 +70,7 @@ module E = struct
end)
let replace kind ~late ~heir =
- let open Evast_visitor.Rewrite in
+ let open Evast.Rewrite in
let rewrite_exp ~visitor (exp : Evast.exp) =
match exp.node with
| Lval lval ->
@@ -82,7 +82,7 @@ module E = struct
| _ -> default.rewrite_exp ~visitor exp
in
let rewriter = { default with rewrite_exp } in
- Evast_visitor.Rewrite.visit_exp rewriter
+ Evast.Rewrite.visit_exp rewriter
end
module HCE = struct
@@ -107,7 +107,7 @@ module HCE = struct
let to_exp h = match get h with
| E e -> e
- | LV lv -> Evast_builder.lval lv
+ | LV lv -> Evast.Build.lval lv
let to_lval h = match get h with
| E _ -> None
@@ -124,7 +124,7 @@ module HCE = struct
let replace kind ~late ~heir h = match get h with
| E e ->
let e = E.replace kind ~late ~heir e in
- if Evast_utils.height_exp e > height_limit
+ if Evast.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
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index cc971d86b03..342a7be295a 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 = Evast_utils.zone_of_exp to_z e in
+ let inputs = Evast.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 = 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_e = Evast.zone_of_exp to_z e in
+ let inputs_lv = Evast.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_offset.ml b/src/plugins/eva/domains/multidim/abstract_offset.ml
index 193ca1a689b..35a34392969 100644
--- a/src/plugins/eva/domains/multidim/abstract_offset.ml
+++ b/src/plugins/eva/domains/multidim/abstract_offset.ml
@@ -37,7 +37,7 @@ let rec pretty fmt = function
pretty s
| Index (Some e, i, _t, s) ->
Format.fprintf fmt "[%a∈%a]%a"
- Evast_printer.pp_exp e
+ Evast.pp_exp e
Int_val.pretty i
pretty s
@@ -61,10 +61,10 @@ let add_index oracle base exp =
let idx' = Int_val.add i (oracle exp) 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 ->
- Some (Evast_builder.integer (Int_val.project_int i))
+ Some (Evast.Build.integer (Int_val.project_int i))
| e -> e
in
- let e' = Option.map (Fun.flip (Evast_builder.add) exp) e in
+ let e' = Option.map (fun e -> Evast.Build.(add e exp)) e in
(* TODO: is idx inside bounds ? *)
`Value (Index (e', idx', t, sub))
| Index (e, i, t, sub) ->
@@ -85,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 Evast_datatype.Exp.equal e1 e2 ->
+ | Some e1, Some e2 when Evast.Exp.equal e1 e2 ->
Some e1 (* keep expression only when equivalent from both offsets *)
| _ -> None
in
@@ -246,7 +246,7 @@ let references =
| NoOffset _ -> acc
| Field (_, sub) | Index (None, _, _, sub) -> aux acc sub
| Index (Some e, _, _, sub) ->
- let r = Evast_utils.vars_in_exp e in
+ let r = Evast.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/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 94b7bc20a69..814f90a2f6e 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -177,9 +177,9 @@ struct
let of_lval oracle (lval : lval) : t or_top =
let (host,offset) = lval.node in
let oracle' = convert_oracle oracle in
- let base_typ = Evast_typing.type_of_lhost host in
+ let base_typ = Evast.type_of_lhost host in
let offset =
- if Evast_utils.lval_contains_volatile lval then
+ if Evast.lval_contains_volatile lval then
`Top
else
Offset.of_evast_offset oracle' base_typ offset in
@@ -421,11 +421,11 @@ struct
in
match expr.node with
| BinOp ((PlusA|PlusPI), e1, e2, _typ) when is_dst e1 ->
- Evast_utils.fold_to_integer e2
+ Evast.fold_to_integer e2
| BinOp ((PlusA|PlusPI), e1, e2, _typ) when is_dst e2 ->
- Evast_utils.fold_to_integer e1
+ Evast.fold_to_integer e1
| BinOp ((MinusA|MinusPI), e1, e2, _typ) when is_dst e1 ->
- Option.map Integer.neg (Evast_utils.fold_to_integer e2)
+ Option.map Integer.neg (Evast.fold_to_integer e2)
| _ -> None)
in
(* [oracle] must be the oracle before the (non-invertible)
@@ -516,9 +516,9 @@ struct
| _ ->
Self.fatal
"This type of array index expression is not supported: %a"
- Evast_printer.pp_exp exp
+ Evast.pp_exp exp
in
- fun exp -> oracle (Evast_utils.const_fold exp)
+ fun exp -> oracle (Evast.const_fold exp)
let mk_bioracle s1 s2 =
let oracle_left = mk_oracle s1
@@ -689,7 +689,7 @@ struct
Value_or_Uninitialized.get_v_normalized v >>-: (fun v -> v, None),
if Value_or_Uninitialized.is_initialized v
then
- let origin = Evast_utils.to_cil_lval lv in
+ let origin = Evast.to_cil_lval lv in
Alarmset.(set (Alarms.Uninitialized origin) True all)
else Alarmset.all
else
@@ -771,7 +771,7 @@ struct
let oracle = valuation_to_oracle state valuation in
let bind state arg =
state >>-:
- assign' ~oracle ~value:arg.avalue (Evast_builder.var arg.formal) (Some arg.concrete)
+ assign' ~oracle ~value:arg.avalue (Evast.Build.var arg.formal) (Some arg.concrete)
in
List.fold_left bind (`Value state) call.arguments
@@ -782,7 +782,7 @@ struct
let args = List.map (fun arg -> arg.avalue) call.arguments in
let+ assigned_result = f args in
let oracle = mk_oracle post in
- let dst = Evast_builder.var return in
+ let dst = Evast.Build.var return in
assign' ~oracle ~value:assigned_result dst None post
let show_expr valuation state fmt expr =
@@ -856,8 +856,8 @@ struct
let annotation = Eva_annotations.read_array_segmentation extension in
let vi,offset,bounds = annotation in
(* Update the segmentation *)
- let bounds = List.map Evast_builder.translate_exp bounds in
- let lval = Evast_builder.translate_lval (Var vi, offset) in
+ let bounds = List.map Evast.translate_exp bounds in
+ let lval = Evast.translate_lval (Var vi, offset) in
let oracle = mk_oracle state in
begin match Location.of_lval oracle lval with
| `Top -> state
@@ -869,7 +869,7 @@ struct
let state = write update state loc in
(* Update the references *)
let add acc e =
- let r = Evast_utils.vars_in_exp e in
+ let r = Evast.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
@@ -905,7 +905,7 @@ struct
erase ~oracle state dst d
let initialize_variable_using_type _kind vi state =
- let lval = Evast_builder.var vi in
+ let lval = Evast.Build.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 332c9f798f9..764d781cff6 100644
--- a/src/plugins/eva/domains/multidim/segmentation.ml
+++ b/src/plugins/eva/domains/multidim/segmentation.ml
@@ -103,7 +103,7 @@ struct
module Var = Cil_datatype.Varinfo
module Exp =
struct
- include Evast_datatype.Exp
+ include Evast.Exp
let equal e1 e2 =
if e1 == e2 then true else equal e1 e2
end
@@ -185,18 +185,18 @@ struct
let of_exp (exp : Evast.exp) =
check_support exp;
(* Normalizes x + c, c + x and x - c *)
- match Evast_utils.fold_to_integer exp with
+ match Evast.fold_to_integer exp with
| Some i -> Const i
| None ->
match exp.node with
| BinOp ((PlusA|PlusPI), e1, e2, _typ) ->
- begin match Evast_utils.(fold_to_integer e1, fold_to_integer e2) with
+ begin match Evast.(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 Evast_utils.fold_to_integer e2 with
+ begin match Evast.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/octagons.ml b/src/plugins/eva/domains/octagons.ml
index d6be2506a3a..e4c8e57a46a 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -141,7 +141,7 @@ module Variable : Variable = struct
let lval (var, _) =
match var with
- | Var vi -> Some (Evast_builder.var vi)
+ | Var vi -> Some (Evast.Build.var vi)
| Lval lval -> HCE.to_lval lval
| Int _ | StartOf _ -> None
@@ -155,7 +155,7 @@ module Variable : Variable = struct
| StartOf _ ->
{ data = Locations.Zone.bottom ; indirect = Locations.Zone.bottom }
| Lval lval ->
- Evast_utils.deps_of_lval eval_loc (Option.get (HCE.to_lval lval))
+ Evast.deps_of_lval eval_loc (Option.get (HCE.to_lval lval))
end
module VarSet =
@@ -466,7 +466,7 @@ module Rewriting = struct
else
let comp =
if Ival.is_zero ival
- then Evast_utils.invert_relation binop
+ then Evast.invert_relation binop
else binop
in
let range = comparison_range comp in
@@ -484,7 +484,7 @@ 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 cil_expr = Evast_utils.to_cil_exp expr in
+ let cil_expr = Evast.to_cil_exp expr in
let alarm = Alarms.Overflow (overflow, cil_expr, bound, bound_kind) in
Alarmset.set alarm Alarmset.True alarms
else alarms
@@ -1300,7 +1300,7 @@ module State = struct
match exp.node with
| Lval lval
when Cil.isIntegralOrPointerType lval.typ
- && not (Evast_utils.lval_contains_volatile lval)
+ && not (Evast.lval_contains_volatile lval)
&& not (is_singleton (eval exp)) ->
Some (Variable.make_lval lval, Ival.zero)
@@ -1682,7 +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_expr = Evast_builder.lval lval in
+ let y_expr = Evast.Build.lval lval in
let y_cvalue = Cvalue.V.inject_ival y_ival in
(y_expr, y_cvalue) :: acc
in
@@ -1720,7 +1720,7 @@ module Domain = struct
else
match expr.node with
| Lval lval when Cil.(isIntegralType lval.typ)
- && not (Evast_utils.lval_contains_volatile lval) ->
+ && not (Evast.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
@@ -1786,7 +1786,7 @@ module Domain = struct
with Not_found -> State.remove state variable
in
let state = assign_interval eval_deps variable assigned state in
- let left_expr = Evast_builder.lval lvalue in
+ let left_expr = Evast.Build.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
@@ -1802,7 +1802,7 @@ module Domain = struct
let assign kinstr left_value expr assigned valuation state =
if kinstr <> Cil_types.Kglobal
&& Cil.isIntegralOrPointerType left_value.lval.typ
- && not (Evast_utils.lval_contains_volatile left_value.lval)
+ && not (Evast.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
@@ -1834,7 +1834,7 @@ module Domain = struct
`Value (start_recursive_call recursion state)
| None ->
let assign_formal state { formal; concrete; avalue } =
- let lval = Evast_builder.var formal in
+ let lval = Evast.Build.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 d36a5b867e0..86cd9a4b2ac 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"
- Evast_printer.pp_exp arg.concrete
+ Evast.pp_exp arg.concrete
pp_cvalue_assigned arg.avalue
let assign _kinstr loc exp cvalue_assigned _valuation state =
feedback "assign %a with %a = %a"
- Evast_printer.pp_lval loc.lval
- Evast_printer.pp_exp exp
+ Evast.pp_lval loc.lval
+ Evast.pp_exp exp
pp_cvalue_assigned cvalue_assigned;
`Value state
let assume _stmt exp truth _valuation state =
feedback "assume %a is %b"
- Evast_printer.pp_exp exp
+ Evast.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"
- Evast_printer.pp_lval lval
+ Evast.pp_lval lval
pp_init_val init;
state
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 591e509f914..8d72449d972 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -146,10 +146,10 @@ let vars_to_bases vi_set =
|> Base.Set.of_seq
let vars_lv lv =
- vars_to_bases (Evast_utils.vars_in_lval lv)
+ vars_to_bases (Evast.vars_in_lval lv)
let vars_exp (e: exp) =
- vars_to_bases (Evast_utils.vars_in_exp e)
+ vars_to_bases (Evast.vars_in_exp e)
(* Legacy names *)
module B2K = K.BaseToHCESet
@@ -367,12 +367,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 Evast_utils.lval_contains_volatile lv then
+ if Evast.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 = Evast_utils.indirect_zone_of_lval get_z lv in
+ let z_lv_indirect = Evast.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. *)
@@ -384,11 +384,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 Evast_utils.exp_contains_volatile e then
+ if Evast.exp_contains_volatile e then
state
else
let k = K.HCE.of_exp e in
- let z = Evast_utils.zone_of_exp get_z e in
+ let z = Evast.zone_of_exp get_z e in
add_key k v z state
let find k state =
@@ -485,7 +485,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" Evast_printer.pp_lval lv
+ Self.fatal "Unknown location for %a" Evast.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 00cc78a0807..be49880df44 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -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 = Evast_utils.indirect_zone_of_lval to_loc lval in
+ let lv_indirect_zone = Evast.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 = Evast_utils.zone_of_exp to_loc exp in
+ let exp_zone = Evast.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 = Evast_utils.zone_of_exp to_loc exp in
+ let exp_zone = Evast.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 (Evast_builder.var formal) concrete to_loc s)
+ assign_aux (Evast.Build.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 = Evast_utils.zone_of_exp to_loc exp in
+ let exp_zone = Evast.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 3d471e0104a..b86171afadb 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1102,13 +1102,13 @@ module D = struct
let log_category = Self.register_category "d-traces"
let assign ki lv e _v _valuation state =
- let cil_lval = Evast_utils.to_cil_lval lv.Eval.lval in
- let cil_exp = Evast_utils.to_cil_exp e in
+ let cil_lval = Evast.to_cil_lval lv.Eval.lval in
+ let cil_exp = Evast.to_cil_exp e in
let trans = Assign (ki, cil_lval, lv.lval.typ, cil_exp) in
`Value (Traces.add_trans state trans)
let assume stmt e pos _valuation state =
- let cil_exp = Evast_utils.to_cil_exp e in
+ let cil_exp = Evast.to_cil_exp e in
let trans = Assume (stmt, cil_exp, pos) in
`Value (Traces.add_trans state trans)
@@ -1124,7 +1124,7 @@ module D = struct
Traces.add_trans state
(Assign (Kstmt stmt, Cil.var arg.Eval.formal,
arg.Eval.formal.Cil_types.vtype,
- Evast_utils.to_cil_exp arg.Eval.concrete)))
+ Evast.to_cil_exp arg.Eval.concrete)))
state call.Eval.arguments in
`Value state
else
@@ -1135,7 +1135,7 @@ module D = struct
| None -> state in
let exps =
List.map
- (fun arg -> Evast_utils.to_cil_exp arg.Eval.concrete)
+ (fun arg -> Evast.to_cil_exp arg.Eval.concrete)
call.Eval.arguments
in
let state = Traces.add_trans state
@@ -1158,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" Evast_printer.pp_lval lv ))
+ Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Evast.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 18ee73a4b3e..fb66e58aa64 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -172,7 +172,7 @@ let rec signed_counterpart typ =
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)
+ Evast.Build.(cast signed_typ exp)
let return t = `Value t, Alarmset.none
@@ -247,8 +247,8 @@ module Make
type origin = Domain.origin
type loc = Loc.location
- module ECache = Evast_datatype.Exp.Map
- module LCache = Evast_datatype.Lval.Map
+ module ECache = Evast.Exp.Map
+ module LCache = Evast.Lval.Map
(* Imperative cache for the evaluation:
all intermediate results of an evaluation are cached here.
@@ -394,7 +394,7 @@ module Make
let truncate_bound overflow_kind bound bound_kind expr value =
let alarm () =
- let cil_expr = Evast_utils.to_cil_exp expr in (* The expression does not necessary come from the original program *)
+ let cil_expr = Evast.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
@@ -432,7 +432,7 @@ 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
+ let cil_expr = Evast.to_cil_exp expr in
if assume_finite
then Alarms.Is_nan_or_infinite (cil_expr, fkind)
else Alarms.Is_nan (cil_expr, fkind)
@@ -453,7 +453,7 @@ module Make
let+ value =
if Kernel.InvalidPointer.get () then
let truth = Value.assume_pointer value in
- let cil_expr = Evast_utils.to_cil_exp expr in
+ let cil_expr = Evast.to_cil_exp expr in
let alarm () = Alarms.Invalid_pointer cil_expr in
interpret_truth ~alarm value truth
else return value
@@ -485,17 +485,17 @@ module Make
let* value, origin = res in
match lval.typ with
| TFloat (fkind, _) ->
- let expr = Evast_builder.lval lval in
+ let expr = Evast.Build.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 (Evast_utils.to_cil_lval lval) in
+ let alarm () = Alarms.Invalid_bool (Evast.to_cil_lval lval) in
let+ new_value = interpret_truth ~alarm value truth in
new_value, origin
| TPtr _ ->
- let expr = Evast_builder.lval lval in
+ let expr = Evast.Build.lval lval in
let+ new_value = assume_pointer context expr value in
new_value, origin
| _ -> res
@@ -507,7 +507,7 @@ module Make
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 (Evast_utils.to_cil_exp expr, Some size)
+ Alarms.Invalid_shift (Evast.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
@@ -523,7 +523,7 @@ module Make
(* Cannot shift a negative value *)
let zero_int = Abstract_value.Int Integer.zero in
let alarm () =
- Alarms.Invalid_shift (Evast_utils.to_cil_exp e1, None)
+ Alarms.Invalid_shift (Evast.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
@@ -535,7 +535,7 @@ 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_index_expr () = Evast_utils.to_cil_exp index_expr in
+ let alarm_index_expr () = Evast.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
@@ -551,7 +551,7 @@ module Make
match op with
| Div | Mod ->
let truth = Value.assume_non_zero v2 in
- let alarm () = Alarms.Division_by_zero (Evast_utils.to_cil_exp e2) in
+ let alarm () = Alarms.Division_by_zero (Evast.to_cil_exp e2) in
let+ v2 = reduce_by_truth ~alarm arg2 truth in
v1, v2
| Shiftrt ->
@@ -565,8 +565,8 @@ module Make
let truth = Value.assume_comparable kind v1 v2 in
let alarm () =
Alarms.Differing_blocks (
- Evast_utils.to_cil_exp e1,
- Evast_utils.to_cil_exp e2)
+ Evast.to_cil_exp e1,
+ Evast.to_cil_exp e2)
in
let arg1 = Some e1, v1 in
reduce_by_double_truth ~alarm arg1 arg2 truth
@@ -585,8 +585,8 @@ module Make
let truth = Value.assume_comparable kind v1 v2 in
let alarm () =
Alarms.Pointer_comparison (
- Option.map Evast_utils.to_cil_exp e1,
- Evast_utils.to_cil_exp e2)
+ Option.map Evast.to_cil_exp e1,
+ Evast.to_cil_exp e2)
in
let propagate_all = propagate_all_pointer_comparison typ in
let args, alarms =
@@ -619,7 +619,7 @@ module Make
| 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 Evast_utils.is_zero_ptr e1 then None else Some e1 in
+ let e1 = if Evast.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
@@ -711,7 +711,7 @@ module Make
then prev_float (Fval.kind fkind) fbound
else fbound
in
- let cil_expr = Evast_utils.to_cil_exp expr in
+ let cil_expr = Evast.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
@@ -973,10 +973,10 @@ module Make
let lval_to_loc = internal_lval_to_loc env ~for_writing ~reduction in
let* loc, volatile = lval_to_loc lval in
if reduction then
- let bitfield = Evast_utils.is_bitfield lval in
+ let bitfield = Evast.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 cil_lval = Evast_utils.to_cil_lval lval in
+ let cil_lval = Evast.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
@@ -989,12 +989,12 @@ module Make
and internal_lval_to_loc env ~for_writing ~reduction lval =
let open Evaluated.Operators in
let host, offset = lval.node in
- let basetyp = Evast_typing.type_of_lhost host in
+ let basetyp = Evast.type_of_lhost host in
let reduce_valid_index = reduction in
let evaluated = eval_offset env ~reduce_valid_index basetyp offset in
let* (offs, offset_volatile) = evaluated in
if for_writing && Eva_utils.is_const_write_invalid lval.typ then
- let cil_lval = Evast_utils.to_cil_lval lval in
+ let cil_lval = Evast.to_cil_lval lval in
let alarm = Alarms.(Memory_access (cil_lval, For_writing)) in
`Bottom, Alarmset.singleton ~status:Alarmset.False alarm
else
@@ -1069,7 +1069,7 @@ module Make
- if it contains a sub-expression which is volatile (volatile_expr)
*)
let volatile = volatile_expr || Cil.typeHasQualifier "volatile" lval.typ in
- let cil_lval = Evast_utils.to_cil_lval lval in
+ let cil_lval = Evast.to_cil_lval lval in
(* Find the value of the location, if not bottom. *)
let v, alarms = domain_query lval loc in
let alarms = close_dereference_alarms cil_lval alarms in
@@ -1284,7 +1284,7 @@ module Make
match expr.node with
| Lval _lv -> assert false
| UnOp (LNot, e, _) ->
- let cond = Evast_builder.normalize_condition e false in
+ let cond = Evast.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)
@@ -1537,7 +1537,7 @@ module Make
let copy_lvalue ?(valuation=Cache.empty) ?subdivnb state lval =
let open Evaluated.Operators in
- let expr = Evast_builder.lval lval in
+ let expr = Evast.Build.lval lval in
let* env = root_environment ?subdivnb state, Alarmset.none in
try
let record, report = Cache.find' valuation expr in
@@ -1575,7 +1575,7 @@ 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 mutable_or_init = Evast_utils.(is_mutable lval || is_initialized lval) in
+ let mutable_or_init = Evast.(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
@@ -1592,7 +1592,7 @@ module Make
let reduce ?valuation:(valuation=Cache.empty) state expr positive =
let open Evaluated.Operators in
(* Generate [e == 0] *)
- let expr = Evast_builder.normalize_condition expr (not positive) in
+ let expr = Evast.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(…)
@@ -1636,7 +1636,7 @@ module Make
else
Self.fatal ~current:true
"Function pointer evaluates to anything. function %a"
- Evast_printer.pp_exp funcexp
+ Evast.pp_exp funcexp
(* For pointer calls, we retro-propagate which function is being called
in the abstract state. This may be useful:
@@ -1647,7 +1647,7 @@ 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 expr = Evast_builder.(ne expr (addr (var vi_f))) in
+ let expr = Evast.Build.(ne expr (addr (var vi_f))) in
fst (reduce ~valuation state expr false)
let eval_function_exp ?subdivnb funcexp ?args state =
@@ -1677,8 +1677,8 @@ module Make
else if alarm || alarm' then Alarmset.Unknown
else Alarmset.True
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 cil_v = Evast.to_cil_exp v in
+ let cil_args = Option.map (List.map (Evast.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
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index 71f118040cb..af795a414b7 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -107,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 = Evast_builder.var vi in
+ let lval = Evast.Build.var vi in
match padding_initialization ~local with
| `Uninitialized -> state
| `Initialized | `MaybeInitialized as i ->
@@ -133,7 +133,7 @@ module Make
| `Bottom ->
if kinstr = Kglobal then
Self.warning ~once:true ~source
- "evaluation of initializer '%a' failed@." Evast_printer.pp_exp expr;
+ "evaluation of initializer '%a' failed@." Evast.pp_exp expr;
raise Initialization_failed
| `Value v -> v
@@ -150,7 +150,7 @@ module Make
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
+ let lval = Evast.add_offset lval off in
apply_evast_initializer ~top_volatile kinstr lval init state
in
List.fold_left doinit state l
@@ -159,8 +159,8 @@ module Make
Very inefficient. *)
let initialize_var_zero_or_volatile kinstr vi state =
let loc = Cil_datatype.Location.unknown in
- let init = Evast_builder.translate_init (Cil.makeZeroInit ~loc vi.vtype) in
- let lval = Evast_builder.var vi in
+ let init = Evast.translate_init (Cil.makeZeroInit ~loc vi.vtype) in
+ let lval = Evast.Build.var vi in
apply_evast_initializer ~top_volatile:true kinstr lval init state
(* ----------------------- Non Lib-entry mode ----------------------------- *)
@@ -169,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 = Evast_builder.var vi in
+ let lval = Evast.Build.var vi in
let volatile_everywhere = Cil.typeHasQualifier "volatile" typ in
let state =
if volatile_everywhere && padding_initialization ~local = `Initialized
@@ -205,8 +205,8 @@ module Make
not (Cil.typeHasQualifier "volatile" typ_lval)
&& not (Cil.is_mutable_or_initialized lval)
then
- let lval = Evast_builder.translate_lval lval
- and exp = Evast_builder.translate_exp exp
+ let lval = Evast.translate_lval lval
+ and exp = Evast.translate_exp exp
and source = fst exp.eloc in
apply_evast_single_initializer ~source kinstr state lval exp
else state
@@ -227,14 +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
+ let init = Option.map Evast.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 = Evast_builder.var vi in
+ let lval = Evast.Build.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
@@ -333,7 +333,7 @@ module Make
initialize_var_lib_entry
else
fun ki vi init state ->
- let init = Option.map Evast_builder.translate_init init in
+ let init = Option.map Evast.translate_init init in
initialize_var_not_lib_entry ki ~local:false vi init state
in
initialize Kglobal vi init.init state
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index ec006367e76..7a8e9a88d0e 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -327,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 = Evast_builder.var vi_ret in
+ let return_lval = Evast.Build.var vi_ret in
let kstmt = Kstmt stmt in
fun state ->
let kind = Abstract_domain.Result kf in
@@ -387,9 +387,9 @@ module Make_Dataflow
| 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,
+ List.map Evast.translate_lval modified,
+ List.map Evast.translate_lval writes,
+ List.map Evast.translate_lval reads,
refs) seq in
let check s =
Transfer.check_unspecified_sequence stmt s seq = `Value ()
diff --git a/src/plugins/eva/engine/subdivided_evaluation.ml b/src/plugins/eva/engine/subdivided_evaluation.ml
index 43f39db787e..c412c011b85 100644
--- a/src/plugins/eva/engine/subdivided_evaluation.ml
+++ b/src/plugins/eva/engine/subdivided_evaluation.ml
@@ -26,8 +26,8 @@ let dkey = Self.register_category "nonlin"
(* ----------------- Occurrences of lvalues in expressions ------------------ *)
-module LvalMap = Evast_datatype.Lval.Map
-module LvalSet = Evast_datatype.Lval.Set
+module LvalMap = Evast.Lval.Map
+module LvalSet = Evast.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
@@ -117,7 +117,7 @@ let gather_non_linear expr =
(* Map from subexpressions to the list of their non-linear lvalues. *)
module ExpMap = struct
- include Evast_datatype.Exp.Map
+ include Evast.Exp.Map
let add expr lv map =
try
let list = find expr map in
@@ -139,7 +139,7 @@ module DepthMap = struct
end
let same lval (expr : Evast.exp) = match expr.node with
- | Lval lv -> Evast_datatype.Lval.equal lv lval
+ | Lval lv -> Evast.Lval.equal lv lval
| _ -> false
(* Converts a map from lvalues to expressions and depth into an association
@@ -155,12 +155,12 @@ let reverse_map map =
DepthMap.fold concat depthmap []
-module LvalList = Datatype.List (Evast_datatype.Lval)
-module NonLinear = Datatype.Pair (Evast_datatype.Exp) (LvalList)
+module LvalList = Datatype.List (Evast.Lval)
+module NonLinear = Datatype.Pair (Evast.Exp) (LvalList)
module NonLinears = Datatype.List (NonLinear)
module Non_linear_expressions =
- State_builder.Hashtbl (Evast_datatype.Exp.Hashtbl) (NonLinears)
+ State_builder.Hashtbl (Evast.Exp.Hashtbl) (NonLinears)
(struct
let name = "Value.Subdivided_evaluation.Non_linear_expressions"
let size = 16
@@ -179,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'" Evast_printer.pp_exp e
- (Pretty_utils.pp_list ~sep:", " Evast_printer.pp_lval) lval)
+ "non-linear '%a', lv '%a'" Evast.pp_exp e
+ (Pretty_utils.pp_list ~sep:", " Evast.pp_lval) lval)
list;
Non_linear_expressions.replace expr list;
list
@@ -655,7 +655,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 = Evast_datatype.Exp.equal expr subexpr in
+ let eq_equal_subexpr = Evast.Exp.equal expr subexpr in
(* Computes a disjunct from subvalues for [lvals]. *)
let compute subvalues =
(* Updates [variables] with their new [subvalues]. *)
@@ -705,7 +705,7 @@ module Make
(* Builds the information for an lvalue. *)
let get_info environment valuation lval =
- let lv_expr = Evast_builder.lval lval in
+ let lv_expr = Evast.Build.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. *)
@@ -770,7 +770,7 @@ module Make
in
Self.result ~current:true ~once:true ~dkey
"subdividing on %a"
- (Pretty_utils.pp_list ~sep:", " Evast_printer.pp_lval) lvals;
+ (Pretty_utils.pp_list ~sep:", " Evast.pp_lval) lvals;
let subdivide =
subdivide_lvals environment valuation subdivnb lvals_info
in
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 50804523203..d4ffc39ca0a 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -109,7 +109,7 @@ let substitution_visitor table =
| None -> vi
| Some vi' -> vi'
in
- { Evast_visitor.Rewrite.default with rewrite_varinfo }
+ { Evast.Rewrite.default with rewrite_varinfo }
module Make (Abstract: Abstractions.S_with_evaluation) = struct
@@ -163,19 +163,19 @@ 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"
- Evast_printer.pp_exp expr;
+ Evast.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"
- Evast_printer.pp_lval lval;
+ Evast.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"
- Evast_printer.pp_lval lval;
+ Evast.pp_lval lval;
res
(* ------------------------------------------------------------------------ *)
@@ -207,7 +207,7 @@ 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 : Evast.exp) = match expr.node with
+ let rec find_lval (expr : exp) = match expr.node with
| Lval lv -> Some lv
| CastE (typ, e) ->
if Eval_typ.need_cast typ e.typ then None else find_lval e
@@ -219,8 +219,8 @@ 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 lval' = Evast_utils.to_cil_lval lval in
- let right_lval' = Evast_utils.to_cil_lval right_lval in
+ let lval' = Evast.to_cil_lval lval in
+ let right_lval' = Evast.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
@@ -355,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 = Evast_utils.zone_of_exp find_loc expr in
+ let expr_zone = Evast.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)
@@ -391,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 = Evast_builder.var argument.formal in
+ let lval = Evast.Build.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
@@ -432,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 = Evast_builder.var_exp vi_ret in
+ let exp_ret_caller = Evast.Build.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
@@ -487,8 +487,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
evaluates the call argument [expr] in the state [state] and the valuation
[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 : Evast.exp).node with
+ let evaluate_actual ~subdivnb ~determinate valuation state (expr : exp) =
+ match expr.node with
| Lval lv ->
lvaluate_and_check ~for_writing:false ~subdivnb ~valuation state lv
>>= fun (valuation, loc) ->
@@ -496,7 +496,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
then
Self.abort ~current:true
"Function argument %a has unknown size. Aborting"
- Evast_printer.pp_exp expr;
+ Evast.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
@@ -541,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 = Evast_visitor.Rewrite.visit_lval visitor loc.lval in
+ let lval = Evast.Rewrite.visit_lval visitor loc.lval in
let loc = { lval; lloc } in
Copy (loc, flagged)
@@ -551,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 = Evast_visitor.Rewrite.visit_exp visitor argument.concrete in
+ let concrete = Evast.Rewrite.visit_exp visitor argument.concrete in
let avalue = replace_value visitor base_substitution argument.avalue in
{ argument with concrete; avalue }
in
@@ -610,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@]" Evast_printer.pp_exp expr pp
+ Format.fprintf fmt "%a : @[<h>%t@]" Evast.pp_exp expr pp
in
let pp = Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@ " ~suf:"@]" pretty in
Self.result ~current:true
@@ -797,8 +797,8 @@ 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 lval1' = Evast_utils.to_cil_lval lval1
- and lval2' = Evast_utils.to_cil_lval lval2 in
+ let lval1' = Evast.to_cil_lval lval1
+ and lval2' = Evast.to_cil_lval lval2 in
let alarm () = Alarms.Not_separated (lval1', lval2') in
let alarm = process_truth ~alarm truth in
Alarmset.combine alarm acc
@@ -817,7 +817,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let unauthorized_reads =
List.filter
(fun x -> List.for_all
- (fun y -> not (Evast_datatype.Lval.equal x y)) modified2)
+ (fun y -> not (Evast.Lval.equal x y)) modified2)
writes1
in
let alarms1 = check_non_overlapping state unauthorized_reads reads2 in
@@ -850,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 = Evast_builder.var varinfo in
+ let lval = Evast.Build.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 6c46b61b70f..c28c2053f8e 100644
--- a/src/plugins/eva/eval.ml
+++ b/src/plugins/eva/eval.ml
@@ -155,7 +155,7 @@ let compute_englobing_subexpr ~subexpr ~expr =
[subexpr], apart [subexpr] itself, or [None] if [subexpr] does not appear
in [expr]. *)
let rec compute expr =
- if Evast_datatype.Exp.equal expr subexpr
+ if Evast.Exp.equal expr subexpr
then Some []
else
let sublist = match expr.node with
@@ -181,9 +181,9 @@ let compute_englobing_subexpr ~subexpr ~expr =
Option.value ~default:[] (compute expr)
module Englobing =
- Datatype.Pair_with_collections (Evast_datatype.Exp) (Evast_datatype.Exp)
+ Datatype.Pair_with_collections (Evast.Exp) (Evast.Exp)
(struct let module_name = "Subexpressions" end)
-module SubExprs = Datatype.List (Evast_datatype.Exp)
+module SubExprs = Datatype.List (Evast.Exp)
module EnglobingSubexpr =
State_builder.Hashtbl (Englobing.Hashtbl) (SubExprs)
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 9dd1badcc8a..5d6cdefbd6a 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -201,7 +201,7 @@ module Make (X: Analysis.S) = struct
GO_Bottom, true
let lval_to_offsetmap state lv =
- let lv = Evast_builder.translate_lval lv in
+ let lv = Evast.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
@@ -249,7 +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 lv = Evast.translate_lval lv in
let loc, _alarms = X.eval_lval_to_loc state lv in
match loc with
| `Bottom -> Locations.Zone.bottom, false, false
@@ -286,7 +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 e = Evast.translate_exp e in
let r = X.eval_expr state e in
fst r, Alarmset.is_empty (snd r), false
in
@@ -305,7 +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 lval = Evast.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 c0e855471ae..3b1ea7d33c1 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 = Evast_builder.(lval (translate_lval lv)) in
+ let e = Evast.(Build.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 e5a69c6f41e..533813a639d 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -996,7 +996,7 @@ let forward_binop_by_type typ =
let forward_binop typ v1 op v2 =
match op with
| Evast.Eq | Ne | Le | Lt | Ge | Gt ->
- let comp = Evast_utils.conv_relation op in
+ let comp = Evast.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,7 +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 op = Evast.translate_unop op in
let v = Cvalue_forward.forward_unop r.etype op r.eover in
let eover = v in
{ etype = typ';
@@ -1364,7 +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 op = Evast.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 1fa576922fb..09f63efa77a 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.ml
@@ -141,9 +141,8 @@ 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 = Evast_datatype.Exp
module Info = struct let module_name = "Condition" end
- include Datatype.Pair_with_collections (Exp) (Datatype.Bool) (Info)
+ include Datatype.Pair_with_collections (Evast.Exp) (Datatype.Bool) (Info)
end
(* Returns a list of loop exit conditions. *)
@@ -284,15 +283,15 @@ let find_lonely_candidate eval_ptr loop_effect expr =
- 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 transition =
- let is_lval = Evast_datatype.Lval.equal lval in
+ let is_lval = Evast.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 ->
+ when is_lval (Evast.Build.var vi) && not inner_loop ->
f expr acc
- | Init (vi, _, _) when is_lval (Evast_builder.var vi) -> raise exn
+ | Init (vi, _, _) when is_lval (Evast.Build.var vi) -> raise exn
| Call (Some lv, _, _, _) when is_lval lv ->
raise exn
| _ -> acc
@@ -311,7 +310,7 @@ let cross_equality loop (lval : Evast.lval) =
transfer_assign lval No_equality find_lval ~inner_loop lval transition
in
let join lv1 lv2 =
- if Evast_datatype.Lval.equal lv1 lv2 then lv1 else raise No_equality
+ if Evast.Lval.equal lv1 lv2 then lv1 else raise No_equality
in
match Graph.compute ~backward:true loop transfer join lval with
| Some lval -> lval
@@ -345,7 +344,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Raises NoIncrement if [expr] is not a constant integer expression. *)
let add_to_delta context binop acc (expr : Evast.exp) =
let typ = expr.typ in
- match Evast_utils.fold_to_integer expr with
+ match Evast.fold_to_integer expr with
| None -> raise NoIncrement
| Some i ->
let inject i = Val.inject_int typ i in
@@ -357,11 +356,11 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let rec delta_assign context lval expr acc =
(* Is the expression [e] equal to the lvalue [lval] (modulo cast)? *)
let rec is_lval (e : Evast.exp) = match e.node with
- | Lval lv -> Evast_datatype.Lval.equal lval lv
+ | Lval lv -> Evast.Lval.equal lval lv
| CastE (typ, e) -> Cil.isIntegralType typ && is_lval e
| _ -> false
in
- match Evast_utils.fold_to_integer expr with
+ match Evast.fold_to_integer expr with
| Some i ->
let v = Val.inject_int expr.typ i in
{ value = `Value v; delta = `Bottom; }
@@ -470,7 +469,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 = Evast_builder.lval lval in
+ let expr = Evast.Build.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]
diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml
index cd58e1240a5..410cee78215 100644
--- a/src/plugins/eva/partitioning/partition.ml
+++ b/src/plugins/eva/partitioning/partition.ml
@@ -30,7 +30,7 @@ type split_kind = Eva_annotations.split_kind = Static | Dynamic
(* Same as Eva_annotations.split_term but with Evast. *)
type split_term =
- | Expression of Evast_datatype.Exp.t
+ | Expression of Evast.Exp.t
| Predicate of (Cil_datatype.Predicate.t
[@compare Logic_utils.compare_predicate]
[@equal Datatype.from_compare])
@@ -40,7 +40,7 @@ let translate_split_term
(term : Eva_annotations.split_term) : split_term * Cil_types.location =
match term with
| Expression cil_exp ->
- Expression (Evast_builder.translate_exp cil_exp), cil_exp.eloc
+ Expression (Evast.translate_exp cil_exp), cil_exp.eloc
| Predicate pred ->
Predicate pred, pred.pred_loc
@@ -69,7 +69,7 @@ let new_monitor
module SplitTerm = Datatype.Make_with_collections (struct
include Datatype.Serializable_undefined
- module Exp = Evast_datatype.Exp
+ module Exp = Evast.Exp
module Predicate = Cil_datatype.PredicateStructEq
type t = split_term [@@deriving eq, ord]
@@ -81,7 +81,7 @@ module SplitTerm = Datatype.Make_with_collections (struct
Stdlib.List.map (fun p -> Predicate p) Predicate.reprs
let pretty fmt = function
- | Expression e -> Evast_printer.pp_exp fmt e
+ | Expression e -> Evast.pp_exp fmt e
| Predicate p -> Printer.pp_predicate fmt p
let hash = function
@@ -99,7 +99,7 @@ module SplitMonitor = Datatype.Make_with_collections (
let name = "Partition.SplitMonitor"
let reprs = [{
- split_term = Expression (List.hd Evast_datatype.Exp.reprs);
+ split_term = Expression (List.hd Evast.Exp.reprs);
split_kind = Static;
split_loc = Cil_datatype.Location.unknown;
split_limit = 0;
@@ -584,7 +584,7 @@ struct
| Enter_loop limit_kind -> fun k x ->
let limit = try match limit_kind with
| ExpLimit cil_exp ->
- let exp = Evast_builder.translate_exp cil_exp
+ let exp = Evast.translate_exp cil_exp
and source = fst cil_exp.eloc in
eval_exp_to_int ~source x exp
| IntLimit i -> i
diff --git a/src/plugins/eva/utils/backward_formals.ml b/src/plugins/eva/utils/backward_formals.ml
index 69fd2da65a6..8e98d6d87a7 100644
--- a/src/plugins/eva/utils/backward_formals.ml
+++ b/src/plugins/eva/utils/backward_formals.ml
@@ -37,7 +37,7 @@ let safe_argument expr =
| _, _ -> raise Unsafe
in
try
- Evast_utils.iter_lvals f expr;
+ Evast.iter_lvals f expr;
true
with Unsafe -> false
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index d04c0a92b44..b129c4b1749 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -44,9 +44,6 @@ 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 cd349fd58b2..75108decc58 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -48,9 +48,6 @@ 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 2e352cf740f..fb2e36c8f8c 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -548,13 +548,13 @@ let build_eval_lval_and_exp () =
eval_lval, eval_exp
let eval_lval lval req =
- let lval = Evast_builder.translate_lval lval in
+ let lval = Evast.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 =
- let exp = Evast_builder.translate_exp exp in
+ let exp = Evast.translate_exp exp in
Value ((snd @@ build_eval_lval_and_exp ()) exp req)
let eval_address' ?(for_writing=false) lval req =
@@ -567,7 +567,7 @@ let eval_address' ?(for_writing=false) lval req =
end : Lvaluation)
let eval_address ?(for_writing=false) lval req =
- let lval = Evast_builder.translate_lval lval in
+ let lval = Evast.translate_lval lval in
eval_address' ~for_writing lval req
let eval_callee exp req =
@@ -578,7 +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
+ let exp = Evast.translate_exp exp in
M.eval_callee exp req
let callee stmt =
@@ -703,20 +703,19 @@ let alarms : type a. a evaluation -> Alarms.t list =
let expr_deps expr request =
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)
+ Evast.zone_of_exp lval_to_loc (Evast.translate_exp expr)
let lval_deps lval request =
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)
+ Evast.zone_of_lval lval_to_loc (Evast.translate_lval lval)
let address_deps lval request =
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)
+ Evast.indirect_zone_of_lval lval_to_loc (Evast.translate_lval lval)
let expr_dependencies expr request =
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)
+ Evast.deps_of_exp lval_to_loc (Evast.translate_exp expr)
(* Taint *)
diff --git a/src/plugins/eva/utils/unit_tests.ml b/src/plugins/eva/utils/unit_tests.ml
index 813ed5ad781..6ba8af66c79 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"
- 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
+ Evast.pp_unop unop Cval.pretty cval (Bottom.pretty Cval.pretty) cval_res
+ Evast.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 Evast_printer.pp_binop binop Cval.pretty cval2
+ Cval.pretty cval1 Evast.pp_binop binop Cval.pretty cval2
(Bottom.pretty Cval.pretty) cval_res
- Sign.pretty sign1 Evast_printer.pp_binop binop Sign.pretty sign2
+ Sign.pretty sign1 Evast.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 5335d863a60..f0421ee6b84 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 = Evast_builder.mk_lval (Mem e, offset) in
+ let lv = Evast.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,8 +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 exp = Evast.translate_exp exp
+ and offset = Evast.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/cvalue_backward.ml b/src/plugins/eva/values/cvalue_backward.ml
index 05f33f98825..7f63d24c51d 100644
--- a/src/plugins/eva/values/cvalue_backward.ml
+++ b/src/plugins/eva/values/cvalue_backward.ml
@@ -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 = Evast_utils.conv_relation binop in
+ let binop = Evast.conv_relation binop in
match V.is_included V.singleton_zero res_value,
V.is_included V.singleton_one res_value with
| true, true ->
diff --git a/src/plugins/eva/values/cvalue_forward.ml b/src/plugins/eva/values/cvalue_forward.ml
index 29d864229ac..2ff1bc2be22 100644
--- a/src/plugins/eva/values/cvalue_forward.ml
+++ b/src/plugins/eva/values/cvalue_forward.ml
@@ -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 = Evast_utils.conv_relation op in
+ let op = Evast.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)
@@ -421,7 +421,7 @@ let forward_binop_float fkind ev1 op ev2 =
| Mult -> binary_float_floats "*." Fval.mul
| Div -> binary_float_floats "/." Fval.div
| Eq | Ne | Lt | Gt | Le | Ge ->
- let op = Evast_utils.conv_relation op in
+ let op = Evast.conv_relation op in
V.inject_comp_result (Fval.forward_comp op f1 f2)
| _ -> assert false
diff --git a/src/plugins/eva/values/offsm_value.ml b/src/plugins/eva/values/offsm_value.ml
index 84f1fa6f6bf..1012e531197 100644
--- a/src/plugins/eva/values/offsm_value.ml
+++ b/src/plugins/eva/values/offsm_value.ml
@@ -419,7 +419,7 @@ module Offsm
let constant _context e _c =
if store_redundant then
- match Evast_utils.fold_to_integer e with
+ match Evast.fold_to_integer e with
| Some i -> inject_int e.typ i
| None -> Top
else Top
diff --git a/src/plugins/eva/values/sign_value.ml b/src/plugins/eva/values/sign_value.ml
index d29ca292ba6..aded4e6650c 100644
--- a/src/plugins/eva/values/sign_value.ml
+++ b/src/plugins/eva/values/sign_value.ml
@@ -318,7 +318,7 @@ let backward_comp_right op ~left ~right =
let backward_binop _ctx ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
match op with
| Evast.Ne | Eq | Le | Lt | Ge | Gt ->
- let op = Evast_utils.conv_relation op in
+ let op = Evast.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. *)
--
GitLab