From 333eff7682fffcd2af3809741c4683e7dbff7d79 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 18 Mar 2024 19:26:20 +0100
Subject: [PATCH] [Eva] evast: normalize SizeOf/AlignOf constructors to
constants
---
src/plugins/eva/ast/evast.ml | 6 +----
src/plugins/eva/ast/evast_builder.ml | 10 +++----
src/plugins/eva/ast/evast_datatype.ml | 14 ++++------
src/plugins/eva/ast/evast_printer.ml | 26 +++----------------
src/plugins/eva/ast/evast_typing.ml | 3 +--
src/plugins/eva/ast/evast_utils.ml | 22 ++++------------
src/plugins/eva/ast/evast_visitor.ml | 12 +++------
src/plugins/eva/domains/apron/apron_domain.ml | 4 ---
.../eva/domains/gauges/gauges_domain.ml | 3 +--
src/plugins/eva/domains/hcexprs.ml | 6 -----
.../eva/domains/multidim/segmentation.ml | 1 -
src/plugins/eva/domains/symbolic_locs.ml | 6 ++---
src/plugins/eva/engine/evaluation.ml | 6 -----
.../eva/partitioning/auto_loop_unroll.ml | 6 ++---
src/plugins/eva/values/main_values.ml | 3 ++-
15 files changed, 29 insertions(+), 99 deletions(-)
diff --git a/src/plugins/eva/ast/evast.ml b/src/plugins/eva/ast/evast.ml
index 5adaae06414..abbb9efed38 100644
--- a/src/plugins/eva/ast/evast.ml
+++ b/src/plugins/eva/ast/evast.ml
@@ -47,11 +47,6 @@ type exp = exp_node tag
and exp_node =
| Const of constant
| Lval of lval
- | SizeOf of (typ * Integer.t option)
- | SizeOfE of (exp * Integer.t option)
- | SizeOfStr of (string * Integer.t option)
- | AlignOf of (typ * Integer.t option)
- | AlignOfE of (exp * Integer.t option)
| UnOp of unop * exp * typ
| BinOp of binop * exp * exp * typ
| CastE of typ * exp
@@ -60,6 +55,7 @@ and exp_node =
(** 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
diff --git a/src/plugins/eva/ast/evast_builder.ml b/src/plugins/eva/ast/evast_builder.ml
index e30e1d0d6af..f63b72009b4 100644
--- a/src/plugins/eva/ast/evast_builder.ml
+++ b/src/plugins/eva/ast/evast_builder.ml
@@ -69,17 +69,11 @@ let translate_binop = function
let rec translate_exp e =
- let eval_size e = Cil.constFoldToInt e in
let node = match e.Cil_types.enode with
| Cil_types.Const (Cil_types.CStr _ | Cil_types.CWStr _) ->
Const (CString (Base.of_string_exp e))
| Cil_types.Const cst -> Const (translate_constant cst)
| Cil_types.Lval lval -> Lval (translate_lval lval)
- | Cil_types.SizeOf typ -> SizeOf (typ, eval_size e)
- | Cil_types.SizeOfE expr -> SizeOfE (translate_exp expr, eval_size e)
- | Cil_types.SizeOfStr str -> SizeOfStr (str, eval_size e)
- | Cil_types.AlignOf typ -> AlignOf (typ, eval_size e)
- | Cil_types.AlignOfE expr -> AlignOfE (translate_exp expr, eval_size e)
| Cil_types.UnOp (unop, expr, typ) ->
UnOp (translate_unop unop, translate_exp expr, typ)
| Cil_types.BinOp (binop, e1, e2, typ) ->
@@ -87,6 +81,10 @@ let rec translate_exp e =
| Cil_types.CastE (typ, expr) -> CastE (typ, translate_exp expr)
| Cil_types.AddrOf lval -> AddrOf (translate_lval lval)
| Cil_types.StartOf lval -> StartOf (translate_lval lval)
+ | Cil_types.(SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _) ->
+ match (Cil.constFold true e).enode with
+ | Const c -> Const (translate_constant c)
+ | _ -> Const (CTopInt Cil.theMachine.typeOfSizeOf)
in
mk_exp ~origin:(Exp e) node
diff --git a/src/plugins/eva/ast/evast_datatype.ml b/src/plugins/eva/ast/evast_datatype.ml
index 38d3c93ee6f..59da247861d 100644
--- a/src/plugins/eva/ast/evast_datatype.ml
+++ b/src/plugins/eva/ast/evast_datatype.ml
@@ -42,11 +42,6 @@ and hash_exp e =
match e.node with
| Const c -> Hashtbl.hash (1, hash_constant c)
| Lval lv -> Hashtbl.hash (2, hash_lval lv)
- | SizeOf (ty,_) -> Hashtbl.hash (3, Typ.hash ty)
- | SizeOfE (e,_) -> Hashtbl.hash (4, hash_exp e)
- | SizeOfStr (s,_) -> Hashtbl.hash (5, s)
- | AlignOf (ty,_) -> Hashtbl.hash (6, Typ.hash ty)
- | AlignOfE (e,_) -> Hashtbl.hash (7, hash_exp e)
| UnOp (op, e, ty) ->
Hashtbl.hash (8, op, hash_exp e, Typ.hash ty)
| BinOp (op, e1, e2, ty) ->
@@ -56,10 +51,11 @@ and hash_exp e =
| StartOf lv -> Hashtbl.hash (12, hash_lval lv)
and hash_constant c =
match c with
- | CString _ | CChr _ -> Hashtbl.hash (1, c)
- | CReal (fn, fk, _) -> Hashtbl.hash (2, fn, fk)
- | CInt64 (n, k, _) -> Hashtbl.hash (3, n, k )
- | CEnum (ei, _) -> Hashtbl.hash (4, ei.einame)
+ | CTopInt t -> Hashtbl.hash (1, Typ.hash t)
+ | CString _ | CChr _ -> Hashtbl.hash (2, c)
+ | CReal (fn, fk, _) -> Hashtbl.hash (3, fn, fk)
+ | CInt64 (n, k, _) -> Hashtbl.hash (4, n, k )
+ | CEnum (ei, _) -> Hashtbl.hash (5, ei.einame)
(* Tag utility *)
diff --git a/src/plugins/eva/ast/evast_printer.ml b/src/plugins/eva/ast/evast_printer.ml
index e9e2542c63f..b5fcf76e70f 100644
--- a/src/plugins/eva/ast/evast_printer.ml
+++ b/src/plugins/eva/ast/evast_printer.ml
@@ -38,14 +38,9 @@ struct
| BinOp ((Div|Mod|Mult),_,_,_) -> 40
| CastE (_,_) | AddrOf(_) | StartOf(_) | UnOp((Neg|BNot|LNot),_,_) -> 30
| Lval (lval) -> lval_level lval
- | SizeOf _ | SizeOfE _ | SizeOfStr _ -> 20
- | AlignOf _ | AlignOfE _ -> 20
| Const _ -> 0
end
-let pp_string fmt s =
- Format.fprintf fmt "\"%s\"" (Escape.escape_string s)
-
let rec pp_lval fmt lval =
let precedence = Precedence.lval_level lval in
match lval.node with
@@ -72,11 +67,6 @@ and pp_offset fmt = function
Format.fprintf fmt "[%a]%a" pp_exp e pp_offset o
and pp_exp fmt exp =
- (* decay follows Cil_printer rules. Ideally, SizeOf and AlignOf should
- be removed from the AST, removing the need for this argument. *)
- pp_exp_aux ~decay:true fmt exp
-
-and pp_exp_aux ~decay fmt exp =
let precedence = Precedence.exp_level exp in
match exp.node with
| Const (c) ->
@@ -92,22 +82,10 @@ and pp_exp_aux ~decay fmt exp =
(pp_exp' ~precedence) e2
| CastE(t,e) ->
Format.fprintf fmt "(%a)%a" Printer.pp_typ t (pp_exp' ~precedence) e
- | SizeOf (t,_) ->
- Format.fprintf fmt "sizeof(%a)" Printer.pp_typ t
- | SizeOfE (e,_) ->
- Format.fprintf fmt "sizeof(%a)" (pp_exp_aux ~decay:false) e
- | SizeOfStr (s,_) ->
- Format.fprintf fmt "sizeof(%a)" pp_string s
- | AlignOf (t,_) ->
- Format.fprintf fmt "__alignof__(%a)" Printer.pp_typ t
- | AlignOfE (e,_) ->
- Format.fprintf fmt "__alignof__(%a)" (pp_exp_aux ~decay:false) e
| AddrOf lv ->
Format.fprintf fmt "& %a" (pp_lval' ~precedence) lv
| StartOf(lv) ->
- if decay
- then Format.fprintf fmt "%a" (pp_lval' ~precedence) lv
- else Format.fprintf fmt "&(%a[0])" (pp_lval' ~precedence) lv
+ Format.fprintf fmt "%a" (pp_lval' ~precedence) lv
and pp_exp' ~precedence fmt exp =
if Precedence.exp_level exp >= precedence then
@@ -147,6 +125,8 @@ and pp_binop fmt b =
Format.fprintf fmt "%s" s
and pp_constant fmt = function
+ | CTopInt _ ->
+ Format.fprintf fmt "%s" (Unicode.top_string ())
| CInt64 (_, _, Some s) ->
Format.fprintf fmt "%s" s
| CInt64 (i, _, _) ->
diff --git a/src/plugins/eva/ast/evast_typing.ml b/src/plugins/eva/ast/evast_typing.ml
index 0e4c478ac10..6b1f3bd6422 100644
--- a/src/plugins/eva/ast/evast_typing.ml
+++ b/src/plugins/eva/ast/evast_typing.ml
@@ -23,6 +23,7 @@
open Evast
let type_of_const : constant -> typ = function
+ | CTopInt t -> t
| CInt64 (_, ik, _) -> Cil_types.TInt (ik, [])
| CChr _ -> Cil.intType
| CString (String (_, Base.CSString _)) -> Cil.theMachine.stringLiteralType
@@ -56,8 +57,6 @@ let type_of_lval_node (host, offset : lval_node) : typ =
let type_of_exp_node : exp_node -> typ = function
| Const c -> type_of_const c
| Lval lv -> Cil.type_remove_qualifier_attributes lv.typ
- | SizeOf _ | SizeOfE _ | SizeOfStr _ -> Cil.theMachine.typeOfSizeOf
- | AlignOf _ | AlignOfE _ -> Cil.theMachine.typeOfSizeOf
| UnOp (_, _, t) -> t
| BinOp (_, _, _, t) -> t
| CastE (t, _) -> t
diff --git a/src/plugins/eva/ast/evast_utils.ml b/src/plugins/eva/ast/evast_utils.ml
index 6cc774741fd..9dcf3289310 100644
--- a/src/plugins/eva/ast/evast_utils.ml
+++ b/src/plugins/eva/ast/evast_utils.ml
@@ -44,11 +44,6 @@ and build_cil_exp node =
let exp_node = match node with
| Const c -> Cil_types.Const (to_cil_const c)
| Lval lv -> Lval (to_cil_lval lv)
- | SizeOf (t, _) -> SizeOf (t)
- | SizeOfE (e, _) -> SizeOfE (to_cil_exp e)
- | SizeOfStr (s, _) -> SizeOfStr (s)
- | AlignOf (t, _) -> AlignOf (t)
- | AlignOfE (e, _) -> AlignOfE (to_cil_exp e)
| UnOp (op, e, t) -> UnOp (to_cil_unop op, to_cil_exp e, t)
| BinOp (op, e1, e2, t) ->
BinOp (to_cil_binop op, to_cil_exp e1, to_cil_exp e2, t)
@@ -108,6 +103,7 @@ and to_cil_offset offset =
and to_cil_const const =
match const with
+ | CTopInt _ -> to_cil_fail ()
| CInt64 (i, ik, s) -> Cil_types.CInt64 (i, ik, s)
| CString (_base) -> to_cil_fail ()
| CChr (c) -> CChr (c)
@@ -158,10 +154,9 @@ let is_initialized lval =
let rec height_exp exp =
match exp.node with
- | Const _ | SizeOf _ | SizeOfStr _ | AlignOf _ -> 0
+ | Const _ -> 0
| Lval lv | AddrOf lv | StartOf lv -> height_lval lv + 1
- | UnOp (_,e,_) | CastE (_, e) | SizeOfE (e,_) | AlignOfE (e,_)
- -> height_exp e + 1
+ | UnOp (_,e,_) | CastE (_, e) -> height_exp e + 1
| BinOp (_,e1,e2,_) -> max (height_exp e1) (height_exp e2) + 1
and height_lval lv =
@@ -247,7 +242,7 @@ let rec deps_of_exp find_loc exp =
Deps.join (process e1) (process e2)
| StartOf lv | AddrOf lv ->
Deps.data (indirect_zone_of_lval find_loc lv)
- | Const _ | SizeOf _ | AlignOf _ | SizeOfStr _ | SizeOfE _ | AlignOfE _ ->
+ | Const _ ->
Deps.bottom
in
process exp
@@ -321,17 +316,10 @@ let rec const_fold (exp: exp) : exp =
match exp.node with
| Const (CChr c) -> integer (Cil.charConstToInt c)
| Const (CEnum(_ei, e)) -> const_fold e
- | Const (CReal _ | CString _ | CInt64 _) -> exp
+ | Const (CTopInt _ | CReal _ | CString _ | CInt64 _) -> exp
| Lval lv -> mk_exp (Lval (const_fold_lval lv))
| AddrOf lv -> mk_exp (AddrOf (const_fold_lval lv))
| StartOf lv -> mk_exp (StartOf (const_fold_lval lv))
- | SizeOf (_, size_opt) | SizeOfE (_, size_opt) | SizeOfStr (_, size_opt)
- | AlignOf (_, size_opt) | AlignOfE (_, size_opt) ->
- begin match size_opt with
- | None -> exp
- | Some i ->
- integer ~kind:Cil.theMachine.kindOfSizeOf i
- end
| CastE (t, e) -> const_fold_cast t e
| UnOp (op, e, t) -> const_fold_unop op e t
| BinOp (op, e1, e2, t) -> const_fold_binop op e1 e2 t
diff --git a/src/plugins/eva/ast/evast_visitor.ml b/src/plugins/eva/ast/evast_visitor.ml
index 2fb4b2e4fb7..95fc07eee4c 100644
--- a/src/plugins/eva/ast/evast_visitor.ml
+++ b/src/plugins/eva/ast/evast_visitor.ml
@@ -72,13 +72,7 @@ struct
| CastE (t, e) ->
let e' = visitor.exp e in
replace_if (e' != e) (CastE (t, e'))
- | SizeOfE (e,size_opt) ->
- let e' = visitor.exp e in
- replace_if (e' != e) (SizeOfE (e',size_opt))
- | AlignOfE (e,size_opt) ->
- let e' = visitor.exp e in
- replace_if (e' != e) (AlignOfE (e',size_opt))
- | SizeOf _ | Const _ | SizeOfStr _ | AlignOf _ ->
+ | Const _ ->
exp
let rewrite_lval ~visitor lval =
@@ -152,11 +146,11 @@ struct
match exp.node with
| Lval lv | AddrOf lv | StartOf lv ->
visitor.lval lv
- | UnOp (_, e, _) | CastE (_, e) | SizeOfE (e, _) | AlignOfE (e, _) ->
+ | UnOp (_, e, _) | CastE (_, e) ->
visitor.exp e
| BinOp (_op, e1, e2, _t) ->
visitor.combine (visitor.exp e1) (visitor.exp e2)
- | SizeOf _ | Const _ | SizeOfStr _ | AlignOf _ ->
+ | Const _ ->
visitor.neutral
let fold_lval ~visitor lval =
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index 6f654989a77..b683c7341b0 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -268,10 +268,6 @@ let rec translate_expr eval oracle expr = match expr.node with
| CastE (typ, e)->
coerce ~cast:true eval typ (translate_expr_linearize eval oracle e)
| AddrOf _ | StartOf _ -> raise (Out_of_Scope "translate_expr addr")
- | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
- match Evast_utils.fold_to_integer expr with
- | None -> raise (Out_of_Scope "translate_expr sizeof alignof")
- | Some i -> Texpr1.Cst (Coeff.s_of_int (Integer.to_int_exn i))
(* Expressions that cannot be translated by [translate_expr] are replaced
using an oracle. Of course, this oracle must be sound!. If the oracle
cannot find a suitable replacement, it can re-raise the expresssion. *)
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 0fc87c677e8..1c618b9551f 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -1001,8 +1001,7 @@ module G = struct
expression that cannot be handled, [Untranslatable] is raised. *)
let rec aux_gauge e =
match e.node with
- | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
- | AddrOf _ | StartOf _ ->
+ | Const _ | AddrOf _ | StartOf _ ->
raise Untranslatable (* constant: using linearization directly *)
| CastE (typ_dst ,e) ->
diff --git a/src/plugins/eva/domains/hcexprs.ml b/src/plugins/eva/domains/hcexprs.ml
index 5d3de97c1f5..e3a9ed02316 100644
--- a/src/plugins/eva/domains/hcexprs.ml
+++ b/src/plugins/eva/domains/hcexprs.ml
@@ -79,7 +79,6 @@ module E = struct
if kind = Modified
then exp
else if Lval.equal lval late then raise NonExchangeable else exp
- | AlignOfE _ -> raise NonExchangeable
| _ -> default.rewrite_exp ~visitor exp
in
let rewriter = { default with rewrite_exp } in
@@ -148,11 +147,6 @@ let syntactic_lvalues expr =
{ lvalues with read = HCESet.add (HCE.of_lval lv) lvalues.read }
| AddrOf lv | StartOf lv ->
{ lvalues with addr = HCESet.add (HCE.of_lval lv) lvalues.addr }
- | AlignOfE (e,_) | SizeOfE (e,_) ->
- (* The lvalues appearing in [e] are not read, and must all be in addr. *)
- let new_lvalues = gather e empty_lvalues in
- let new_addr = HCESet.union new_lvalues.read new_lvalues.addr in
- { lvalues with addr = HCESet.union new_addr lvalues.addr }
| UnOp (_, e, _) | CastE (_, e) -> gather e lvalues
| BinOp (_, e1, e2, _) -> gather e1 (gather e2 lvalues)
| _ -> lvalues
diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml
index 3b24bf46366..332c9f798f9 100644
--- a/src/plugins/eva/domains/multidim/segmentation.ml
+++ b/src/plugins/eva/domains/multidim/segmentation.ml
@@ -156,7 +156,6 @@ struct
let rec linearity vi (exp : Evast.exp) =
match exp.node with
| Const _
- | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
| AddrOf _ | StartOf _ -> Integer.zero
| Lval {node = Var vi', NoOffset} ->
if Var.equal vi' vi
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index b972cb0a1ed..591e509f914 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -125,8 +125,7 @@ let interesting_exp get_locs get_val e =
has_lvalue e
| BinOp (op, e1, e2,_) ->
not (is_comp op) && (has_lvalue e1 || has_lvalue e2)
- | Const _ | SizeOf _ | SizeOfStr _ | SizeOfE _ | AlignOf _ | AlignOfE _
- | StartOf _ | AddrOf _ ->
+ | Const _ | StartOf _ | AddrOf _ ->
false
in
match e.node with
@@ -134,8 +133,7 @@ let interesting_exp get_locs get_val e =
not (Precise_locs.cardinal_zero_or_one (get_locs lv))
| BinOp (op, e1, e2,_) ->
not (is_comp op) && has_lvalue e1 && has_lvalue e2
- | CastE _ | UnOp _ | Const _ | SizeOf _ | SizeOfStr _ | SizeOfE _
- | AlignOf _ | AlignOfE _ | StartOf _ | AddrOf _ ->
+ | CastE _ | UnOp _ | Const _ | StartOf _ | AddrOf _ ->
false
(* Locals and formals syntactically present in an expression or lvalue *)
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index b93a129e6cb..18ee73a4b3e 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -915,12 +915,6 @@ module Make
in
compute_reduction v volatile
- | SizeOf (_,s) | SizeOfE (_,s) | SizeOfStr (_,s)
- | AlignOf (_,s) | AlignOfE (_,s) ->
- match s with
- | Some v -> return (Value.inject_int expr.typ v, Neither, false)
- | _ -> return (Value.top_int, Neither, false)
-
and internal_forward_eval_constant env expr constant =
let open Evaluated.Operators in
let+ value =
diff --git a/src/plugins/eva/partitioning/auto_loop_unroll.ml b/src/plugins/eva/partitioning/auto_loop_unroll.ml
index 73da9d5434c..1fa576922fb 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.ml
@@ -227,8 +227,7 @@ let classify eval_ptr loop_effect (lval : Evast.lval) =
| Lval lval -> classify_lval lval = Constant
| UnOp (_, e, _) | CastE (_, e) -> is_const_expr e
| BinOp (_, e1, e2, _) -> is_const_expr e1 && is_const_expr e2
- | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
- | AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> true
+ | Const _ | AddrOf _ | StartOf _ -> true
and classify_lval lv = match lv.node with
| Var varinfo, offset ->
if (varinfo.vglob && loop_effect.call)
@@ -263,8 +262,7 @@ let rec get_lvalues (expr : Evast.exp) =
| Lval lval -> [ lval ]
| UnOp (_, e, _) | CastE (_, e) -> get_lvalues e
| BinOp (_op, e1, e2, _typ) -> get_lvalues e1 @ get_lvalues e2
- | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
- | AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> []
+ | Const _ | AddrOf _ | StartOf _ -> []
(* Finds the unique candidate lvalue for the automatic loop unrolling
heuristic in the expression [expr], if it exists. Returns None otherwise. *)
diff --git a/src/plugins/eva/values/main_values.ml b/src/plugins/eva/values/main_values.ml
index dd492866f09..313fad45edf 100644
--- a/src/plugins/eva/values/main_values.ml
+++ b/src/plugins/eva/values/main_values.ml
@@ -49,7 +49,8 @@ module CVal = struct
let assume_comparable = Cvalue_forward.assume_comparable
let constant _context _exp = function
- | Evast.CInt64 (i,_k,_s) -> Cvalue.V.inject_int i
+ | Evast.CTopInt _ -> Cvalue.V.top_int
+ | CInt64 (i,_k,_s) -> Cvalue.V.inject_int i
| CChr c -> Cvalue.V.inject_int (Cil.charConstToInt c)
| CString base ->
Cvalue.V.inject base Ival.zero
--
GitLab