Skip to content
Snippets Groups Projects
Commit e7698905 authored by Virgile Robles's avatar Virgile Robles
Browse files

[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.
parent 7976f024
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
meta_dispatch.ml
+ 1
− 4
View file @ e7698905
......@@ -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
......
meta_options.ml
+ 0
− 6
View file @ e7698905
......@@ -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;
......
meta_run.ml
+ 1
− 3
View file @ e7698905
......@@ -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 () =
......
meta_simplify.ml
+ 0
− 107
View file @ e7698905
......@@ -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
......
meta_simplify.mli
+ 0
− 1
View file @ e7698905
......@@ -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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment