From e76989059df600177a8f1bd6cb0ed65d92a846b5 Mon Sep 17 00:00:00 2001
From: Virgile Robles <virgile.robles@protonmail.ch>
Date: Thu, 28 Oct 2021 17:58:06 +0200
Subject: [PATCH] [simplify] Remove unused special E-ACSL code
A lot of code was dedicated to the -meta-eacsl option, meant to
circumvent some limitations of E-ACSL by translating \let and some
\separated forms to equivalent formulas.
E-ACSL no longer has these limitations.
---
meta_dispatch.ml | 5 +--
meta_options.ml | 6 ---
meta_run.ml | 4 +-
meta_simplify.ml | 107 ----------------------------------------------
meta_simplify.mli | 1 -
5 files changed, 2 insertions(+), 121 deletions(-)
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 27de33b..d995b8b 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -80,10 +80,7 @@ let unpack_mp flags mp admit =
let pred = if flags.simpl then
Meta_simplify.simplify pred
else pred
- in
- if flags.eacsl_transform then
- Meta_simplify.eacsl_transform pred
- else pred
+ in pred
in
let ump_assert = match mp.mp_translation with
| MtNone -> assert false
diff --git a/meta_options.ml b/meta_options.ml
index d0e8c76..3059719 100644
--- a/meta_options.ml
+++ b/meta_options.ml
@@ -42,11 +42,6 @@ module Check_External = Self.True (struct
modifying/accessing the state inside the caller's body"
end)
-module Eacsl_transform = Self.False (struct
- let option_name = "-meta-eacsl"
- let help = "Removes \\let and simple \\separated to accomodate E-ACSL"
- end)
-
module Targets = Self.String_set (struct
let option_name = "-meta-set"
let arg_name = "targets"
@@ -107,7 +102,6 @@ module Default_to_assert = Self.True (struct
type meta_flags = {
check_external : bool;
simpl : bool;
- eacsl_transform : bool;
static_bindings : int option;
target_set : StringSet.t option;
number_assertions : bool;
diff --git a/meta_run.ml b/meta_run.ml
index ab057a2..2b184b9 100644
--- a/meta_run.ml
+++ b/meta_run.ml
@@ -70,7 +70,6 @@ let register () =
let flags = {
check_external = Check_External.get ();
simpl = Simpl.get ();
- eacsl_transform = Eacsl_transform.get ();
number_assertions = Number_assertions.get ();
prefix_meta = Prefix_meta.get ();
static_bindings = (let r = Static_bindings.get () in
@@ -93,8 +92,7 @@ let translate ?(check_external=true) ?(simpl=true) ?target_set
let flags = {
number_assertions; default_to_assert = true;
static_bindings; prefix_meta; list_targets = false;
- check_external; simpl; target_set; eacsl_transform = false;
- keep_proof_files = false;
+ check_external; simpl; target_set; keep_proof_files = false;
} in generate flags
let () =
diff --git a/meta_simplify.ml b/meta_simplify.ml
index 76f52db..da1e8a6 100644
--- a/meta_simplify.ml
+++ b/meta_simplify.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Meta_options
(* Check if a logic variable corresponds to a C variable in the source code
* (to easily discard a separation between it and something else if there is no
@@ -171,116 +170,10 @@ class simplifier_visitor = object(_)
| _ -> Cil.DoChildren
end
-class unfold_one_let lid t' = object (_)
- inherit Visitor.frama_c_inplace
- method! vterm _ =
- Cil.DoChildrenPost (fun t ->
- match t.term_node with
- | TLval (TVar {lv_kind = LVLocal; lv_id; _}, _) when lv_id = lid -> t'
- | _ -> t
- )
-end
-(*
- * Unfolds \let and replace restricted cases of \separated with
- * \base_addr, \offset, etc.-based formulas
- *
- * -----|--##>-----------
- * ------|##---->--------
- * begin(o) = \base_address(o) + \offset(o)
- * end(o) = begin(o) + \sizeof(o)
- * \separated(o1, o2) <==> begin(o1) > end(o2) || begin(o2) > end(o1)
- *)
-class eacsl_transform_vis = object(_)
- inherit Visitor.frama_c_inplace
-
- method! vpredicate _ =
- Cil.DoChildrenPost (fun p ->
- match p.pred_content with
- | Plet ({l_var_info = lvi; l_body = LBterm t}, pred) ->
- let vis = new unfold_one_let lvi.lv_id t in
- Visitor.visitFramacPredicate vis pred
- | Plet _ -> Self.feedback "Unsupported let %a" Printer.pp_predicate p;
- p
- | Pseparated [t1; t2] ->
- let ptrt = Ctype (Cil.charPtrType) in
- let rec ba o = begin match o.term_node with
- | TAddrOf (TVar tab, TIndex ({term_node = Trange (Some _, Some _)}, TNoOffset)) ->
- ba (Logic_const.term (TStartOf (TVar tab, TNoOffset)) ptrt)
- | TBinOp(PlusPI, ptr, {term_node = Trange (Some _, Some _)}) ->
- ptr
- | TBinOp(IndexPI, ptr, {term_node = Trange (Some _, Some _)}) ->
- ptr
- | _ -> Logic_const.term (Tbase_addr(BuiltinLabel Here, o)) ptrt
- end in
- let off o = begin match o.term_node with
- | TAddrOf (TVar tab, TIndex ( {term_node = Trange ( Some begt, Some _)}, TNoOffset)) ->
- let artype = begin match tab.lv_type with
- | Ctype at -> Cil.typeOf_array_elem at
- | _ -> assert false
- end in
- let so = Logic_const.term (TSizeOf artype) Linteger in
- Logic_const.term (TBinOp (Mult, so, begt)) Linteger
- | TBinOp(PlusPI,
- {term_type = ptrType},
- {term_node = Trange (Some begt, Some _)})
- | TBinOp(IndexPI,
- {term_type = ptrType},
- {term_node = Trange (Some begt, Some _)}) ->
- let artype = begin match ptrType with
- | Ctype tt -> Cil.typeOf_pointed tt
- | _ -> assert false
- end in
- let so = Logic_const.term (TSizeOf artype) Linteger in
- Logic_const.term (TBinOp (Mult, so, begt)) Linteger
- | _ -> Logic_const.term (Toffset(BuiltinLabel Here, o)) Linteger
- end in
- let bl o = begin match o.term_node with
- | TAddrOf (TVar tab, TIndex (
- {term_node = Trange (Some begt, Some endt)}, TNoOffset)) ->
- let diff = Logic_const.term (TBinOp (MinusA, endt, begt)) Linteger in
- let artype = begin match tab.lv_type with
- | Ctype at -> Cil.typeOf_array_elem at
- | _ -> assert false
- end in
- let so = Logic_const.term (TSizeOf artype) Linteger in
- Logic_const.term (TBinOp (Mult, so, diff)) Linteger
- | TBinOp(PlusPI,
- {term_type = ptrType},
- {term_node = Trange (Some begt, Some endt)})
- | TBinOp(IndexPI,
- {term_type = ptrType},
- {term_node = Trange (Some begt, Some endt)}) ->
- let diff = Logic_const.term (TBinOp (MinusA, endt, begt)) Linteger in
- let artype = begin match ptrType with
- | Ctype tt -> Cil.typeOf_pointed tt
- | _ -> assert false
- end in
- let so = Logic_const.term (TSizeOf artype) Linteger in
- Logic_const.term (TBinOp (Mult, so, diff)) Linteger
- | _ ->
- let tp = begin match o.term_type with
- | Ctype tt -> Cil.typeOf_pointed tt
- | _ -> assert false
- end in
- Logic_const.term (TSizeOf tp) Linteger
- end in
- let fbeg o = Logic_const.term (TBinOp (PlusA, ba o, off o)) Linteger in
- let fend o = Logic_const.term (TBinOp (PlusA, fbeg o, bl o)) Linteger in
- let c1 = Logic_const.prel (Rge, fbeg t1, fend t2) in
- let c2 = Logic_const.prel (Rge, fbeg t2, fend t1) in
- Logic_const.por (c1, c2)
- | _ -> p
- )
-end
-
let simplify pred =
let vis = new simplifier_visitor in
Visitor.visitFramacPredicate vis pred
-let eacsl_transform pred =
- let vis = new eacsl_transform_vis in
- Visitor.visitFramacPredicate vis pred
-
(*
* Given a predicate and the statement (and kf) it will be attached to,
* return another predicate where every quantified, local or formal logic
diff --git a/meta_simplify.mli b/meta_simplify.mli
index bd33ed1..b970d3f 100644
--- a/meta_simplify.mli
+++ b/meta_simplify.mli
@@ -23,7 +23,6 @@
open Cil_types
val simplify : predicate -> predicate
-val eacsl_transform : predicate -> predicate
val remove_alpha_conflicts : predicate -> kernel_function -> stmt -> predicate
val neq_lval : term_lval -> term_lval -> bool
val is_not_orig_variable : logic_var -> bool
--
GitLab