diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 3fbd174366f6ea7a3dbd1be7cdd868800ee3e4af..78f90c6978a4fa2d30a866460bde9fd493777145 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,8 @@
Plugin E-ACSL <next-release>
############################
+-* E-ACSL [2022-03-01] Fix normalization of global annotations that
+ may lead to crashes (frama-c/e-acsl#195).
- E-ACSL [2022-01-28] Add Linux's pthread concurrency support.
-* E-ACSL [2021-12-03] Fix crash when creating an axiomatic with an
existing name in E-ACSL's RTL (frama-c/e-acsl#161).
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index e7eaa96b0cd410bfe1c2ce7def431d9d1a9068c3..3afb018482d3cbf0e297d62feebafeb48de66b3e 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -696,34 +696,26 @@ end
(Result.Error (Error.make_not_yet "unguarded \\exists quantification"))
| _ -> ()
- let do_user_predicates () =
- let gannot a =
- match a with
- | Dfun_or_pred ({l_body = LBpred p},loc) ->
- (match Logic_normalizer.get_pred p with
- | PoT_pred p -> process_quantif ~loc p
- | PoT_term _ -> ())
- | _ -> ()
- in
- Annotations.iter_global (fun _ a -> gannot a)
-
let preprocessor = object
inherit E_acsl_visitor.visitor
+ method !vannotation annot =
+ match annot with
+ | Dfun_or_pred _ -> Cil.DoChildren
+ | _ -> Cil.SkipChildren
+
method !vpredicate p =
let loc = p.pred_loc in
- match Logic_normalizer.get_pred p with
- | PoT_pred p -> process_quantif ~loc p;
- Cil.DoChildren
- | PoT_term _ -> Cil.DoChildren
+ let p = Logic_normalizer.get_pred p in
+ process_quantif ~loc p;
+ Cil.DoChildren
end
let compute ast =
Visitor.visitFramacFileSameGlobals
(preprocessor :> Visitor.frama_c_inplace)
- ast;
- do_user_predicates ()
+ ast
let compute_annot annot =
ignore
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
index fea87f8c78f1b68f947686546ce61809497e5731..fab6c7ffcec22d641aa65aa69b9a2ed591936801 100644
--- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
@@ -31,6 +31,7 @@ let case_globals
?(var_fun_decl = fun _ -> default ())
?(var_init = fun _ -> default ())
?(var_def = fun _ _ -> default ())
+ ?(glob_annot = fun _ -> default ())
~fun_def
= function
(* library functions and built-ins *)
@@ -65,6 +66,10 @@ let case_globals
| GFun(fundec, _) ->
fun_def fundec
+ (* global annotation *)
+ | GAnnot (ga, _) ->
+ glob_annot ga
+
(* other globals: nothing to do *)
| GType _
| GCompTag _
@@ -74,7 +79,6 @@ let case_globals
| GAsm _
| GPragma _
| GText _
- | GAnnot _ (* do never read annotation from sources *)
->
default ()
@@ -106,6 +110,9 @@ class visitor
method var_def : varinfo -> init -> global list Cil.visitAction =
fun _ _ -> self#default ()
+ method glob_annot: global_annotation -> global list Cil.visitAction =
+ fun _ -> Cil.DoChildren (* do visit ACSL annotations by default *)
+
method fun_def ({svar = vi}) =
let kf = try Globals.Functions.get vi with Not_found -> assert false in
if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
@@ -120,5 +127,6 @@ class visitor
~var_fun_decl:self#var_fun_decl
~var_init:self#var_init
~var_def:self#var_def
+ ~glob_annot:self#glob_annot
~fun_def:self#fun_def
end
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli
index b1f50d9faaf88a49f034d16ae6dd42bf40180aa6..21ca0fea5d1ed32bcbd3adf7d10867cd4539f41c 100644
--- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli
@@ -31,6 +31,7 @@ val case_globals :
?var_fun_decl:(varinfo -> 'a) ->
?var_init:(varinfo -> 'a) ->
?var_def:(varinfo -> init -> 'a) ->
+ ?glob_annot:(global_annotation -> 'a) ->
fun_def:(fundec -> 'a) ->
global -> 'a
(** Function to descend into the root of the ast according to the various cases
@@ -47,6 +48,7 @@ val case_globals :
value
- [var_def] is the case for variable definitions with an initialization
value
+ - [glob_annot] is the case for global annotations
- [fun_def] is the case for function definition. *)
(** Visitor for managing the root of the AST, on the globals level, with the
@@ -64,5 +66,6 @@ class visitor :
method var_fun_decl: varinfo -> global list Cil.visitAction
method var_init: varinfo -> global list Cil.visitAction
method var_def: varinfo -> init -> global list Cil.visitAction
+ method glob_annot: global_annotation -> global list Cil.visitAction
method fun_def: fundec -> global list Cil.visitAction
end
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
index bc2b125769d3f2132e603764a329775e06911caf..eb5b5fb88651fe092b6ac3b77bff2892bedab363 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Analyses_types
module Id_predicate =
Datatype.Make_with_collections
@@ -40,8 +39,8 @@ module Id_predicate =
(* Memoization module which retrieves the preprocessed form of predicates *)
module Memo: sig
- val memo_pred: (predicate -> pred_or_term option) -> predicate -> unit
- val get_pred: predicate -> pred_or_term
+ val memo_pred: (predicate -> predicate option) -> predicate -> unit
+ val get_pred: predicate -> predicate
val memo_term : (term -> term option) -> term -> unit
val get_term : term -> term
val clear: unit -> unit
@@ -52,7 +51,7 @@ end = struct
let get_pred p =
try Id_predicate.Hashtbl.find tbl_pred p
- with Not_found -> PoT_pred p
+ with Not_found -> p
let memo_pred process p =
try ignore (Id_predicate.Hashtbl.find tbl_pred p) with
@@ -97,7 +96,7 @@ let preprocess_pred ~loc p =
| Pvalid _ -> Logic_const.pvalid ~loc (llabel, t)
| _ -> assert false
in
- Some (PoT_pred (Logic_const.pand ~loc (init, p_copy)))
+ Some (Logic_const.pand ~loc (init, p_copy))
| _ -> None
end
| _ -> None
@@ -126,8 +125,6 @@ let preprocess_term ~loc t =
let preprocessor = object
inherit E_acsl_visitor.visitor
- (* Only logic functions and logic predicates are handled.
- E-acsl simply ignores all the other global annotations *)
method !vannotation annot =
match annot with
| Dfun_or_pred _ -> Cil.DoChildren
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
index 7eafabeb5287e0dcae03d0a935438077ad5117d7..bee473b8b87d60499c8f81445a3e7d93251632ac 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
@@ -42,7 +42,7 @@ val preprocess_annot : code_annotation -> unit
val preprocess_predicate : predicate -> unit
(** Preprocess a predicate and its children and store the results *)
-val get_pred : predicate -> pred_or_term
+val get_pred : predicate -> predicate
(** Retrieve the preprocessed form of a predicate *)
val get_term : term -> term
(** Retrieve the preprocessed form of a term *)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index f23e7f2d050b547d41689b5c49840c6bf9bb8fc3..5a714336460373d6ec0a4d5771ca763329427c31 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -812,107 +812,105 @@ and type_bound_variables ~loc ~lenv (t1, lv, t2) =
(t1, lv, t2)
and type_predicate ~lenv p =
- match Logic_normalizer.get_pred p with
- | PoT_term t -> type_term ~use_gmp_opt:true ~lenv t
- | PoT_pred p ->
- Cil.CurrentLoc.set p.pred_loc;
- (* this pattern matching also follows the formal rules of the JFLA's paper *)
- let op =
- match p.pred_content with
- | Pfalse | Ptrue -> c_int
- | Papp(li, _, args) ->
- begin
- match li.l_body with
- | LBpred p ->
- let typed_args =
- type_args
- ~use_gmp_opt:true
- ~lenv
- li.l_profile
- args
- li.l_var_info.lv_name
- in
- ignore (type_predicate ~lenv:typed_args p);
- List.iter Interval.Env.remove li.l_profile
- | LBnone -> ()
- | LBreads _ -> ()
- | LBinductive _ -> ()
- | LBterm _ ->
- Options.fatal "unexpected logic definition"
- Printer.pp_predicate p
- end;
- c_int
- | Pdangling _ -> Error.not_yet "\\dangling"
- | Prel(_, t1, t2) ->
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
- let i = Interval.join i1 i2 in
- let ctx = mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i) in
- ignore (type_term ~use_gmp_opt:true ~ctx ~lenv t1);
- ignore (type_term ~use_gmp_opt:true ~ctx ~lenv t2);
- (match ctx with
- | Nan -> c_int
- | Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx)
- | Pand(p1, p2)
- | Por(p1, p2)
- | Pxor(p1, p2)
- | Pimplies(p1, p2)
- | Piff(p1, p2) ->
- ignore (type_predicate ~lenv p1);
- ignore (type_predicate ~lenv p2);
- c_int
- | Pnot p ->
- ignore (type_predicate ~lenv p);
- c_int
- | Pif(t, p1, p2) ->
- let ctx = mk_ctx ~use_gmp_opt:false c_int in
- ignore (type_term ~use_gmp_opt:false ~ctx ~lenv t);
- ignore (type_predicate ~lenv p1);
- ignore (type_predicate ~lenv p2);
- c_int
- | Plet(li, p) ->
- let li_t = Misc.term_of_li li in
- type_letin li li_t;
- ignore (type_term ~use_gmp_opt:true ~lenv li_t);
- (type_predicate ~lenv p).ty
- | Pforall _
- | Pexists _ ->
- begin
- let guards, goal =
- Error.retrieve_preprocessing
- "preprocessing of quantified predicate"
- Bound_variables.get_preprocessed_quantifier
- p
- Printer.pp_predicate
+ let p = Logic_normalizer.get_pred p in
+ Cil.CurrentLoc.set p.pred_loc;
+ (* this pattern matching also follows the formal rules of the JFLA's paper *)
+ let op =
+ match p.pred_content with
+ | Pfalse | Ptrue -> c_int
+ | Papp(li, _, args) ->
+ begin
+ match li.l_body with
+ | LBpred p ->
+ let typed_args =
+ type_args
+ ~use_gmp_opt:true
+ ~lenv
+ li.l_profile
+ args
+ li.l_var_info.lv_name
in
- let guards =
- List.map
- (fun (t1, x, t2) ->
- type_bound_variables ~loc:p.pred_loc ~lenv (t1, x, t2))
- guards
- in Bound_variables.replace p guards goal;
- (type_predicate ~lenv goal).ty
- end
- | Pseparated tlist ->
- List.iter
- (fun t ->
- ignore
- (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t))
- tlist;
- c_int
- | Pinitialized(_, t)
- | Pfreeable(_, t)
- | Pallocable(_, t)
- | Pvalid(_, t)
- | Pvalid_read(_, t)
- | Pobject_pointer(_,t)
- | Pvalid_function t ->
- ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t);
- c_int
- | Pat(p, _) -> (type_predicate ~lenv p).ty
- | Pfresh _ -> Error.not_yet "\\fresh"
- in
- coerce ~arith_operand:false ~ctx:c_int ~op c_int
+ ignore (type_predicate ~lenv:typed_args p);
+ List.iter Interval.Env.remove li.l_profile
+ | LBnone -> ()
+ | LBreads _ -> ()
+ | LBinductive _ -> ()
+ | LBterm _ ->
+ Options.fatal "unexpected logic definition"
+ Printer.pp_predicate p
+ end;
+ c_int
+ | Pdangling _ -> Error.not_yet "\\dangling"
+ | Prel(_, t1, t2) ->
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
+ let i = Interval.join i1 i2 in
+ let ctx = mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i) in
+ ignore (type_term ~use_gmp_opt:true ~ctx ~lenv t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx ~lenv t2);
+ (match ctx with
+ | Nan -> c_int
+ | Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx)
+ | Pand(p1, p2)
+ | Por(p1, p2)
+ | Pxor(p1, p2)
+ | Pimplies(p1, p2)
+ | Piff(p1, p2) ->
+ ignore (type_predicate ~lenv p1);
+ ignore (type_predicate ~lenv p2);
+ c_int
+ | Pnot p ->
+ ignore (type_predicate ~lenv p);
+ c_int
+ | Pif(t, p1, p2) ->
+ let ctx = mk_ctx ~use_gmp_opt:false c_int in
+ ignore (type_term ~use_gmp_opt:false ~ctx ~lenv t);
+ ignore (type_predicate ~lenv p1);
+ ignore (type_predicate ~lenv p2);
+ c_int
+ | Plet(li, p) ->
+ let li_t = Misc.term_of_li li in
+ type_letin li li_t;
+ ignore (type_term ~use_gmp_opt:true ~lenv li_t);
+ (type_predicate ~lenv p).ty
+ | Pforall _
+ | Pexists _ ->
+ begin
+ let guards, goal =
+ Error.retrieve_preprocessing
+ "preprocessing of quantified predicate"
+ Bound_variables.get_preprocessed_quantifier
+ p
+ Printer.pp_predicate
+ in
+ let guards =
+ List.map
+ (fun (t1, x, t2) ->
+ type_bound_variables ~loc:p.pred_loc ~lenv (t1, x, t2))
+ guards
+ in Bound_variables.replace p guards goal;
+ (type_predicate ~lenv goal).ty
+ end
+ | Pseparated tlist ->
+ List.iter
+ (fun t ->
+ ignore
+ (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t))
+ tlist;
+ c_int
+ | Pinitialized(_, t)
+ | Pfreeable(_, t)
+ | Pallocable(_, t)
+ | Pvalid(_, t)
+ | Pvalid_read(_, t)
+ | Pobject_pointer(_,t)
+ | Pvalid_function t ->
+ ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t);
+ c_int
+ | Pat(p, _) -> (type_predicate ~lenv p).ty
+ | Pfresh _ -> Error.not_yet "\\fresh"
+ in
+ coerce ~arith_operand:false ~ctx:c_int ~op c_int
let type_term ~use_gmp_opt ?ctx ~lenv t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
@@ -980,28 +978,31 @@ let get_cast_of_predicate ~lenv p =
let clear = Memo.clear
-let typer_visitor lenv = object
+let typing_visitor lenv = object
inherit E_acsl_visitor.visitor
+ (* global logic functions and predicates are evaluated are callsites *)
+ method !glob_annot _ = Cil.SkipChildren
+
method !vpredicate p =
(* Do not raise a warning for e-acsl errors at preprocessing time,
those errrors are stored in the table and warnings are raised at
- translation time*)
- let _ = try type_named_predicate ~lenv p
- with Error.Not_yet _ | Error.Typing_error _ -> ()
- in
+ translation time *)
+ ignore
+ (try type_named_predicate ~lenv p
+ with Error.Not_yet _ | Error.Typing_error _ -> ());
Cil.SkipChildren
end
let type_program ast =
Visitor.visitFramacFileSameGlobals
- (typer_visitor [] :> Visitor.frama_c_inplace)
+ (typing_visitor [] :> Visitor.frama_c_inplace)
ast
let type_code_annot lenv annot =
ignore
(Visitor.visitFramacCodeAnnotation
- (typer_visitor lenv :> Visitor.frama_c_inplace)
+ (typing_visitor lenv :> Visitor.frama_c_inplace)
annot)
let preprocess_predicate lenv p =
@@ -1009,7 +1010,7 @@ let preprocess_predicate lenv p =
Bound_variables.preprocess_predicate p;
ignore
(Visitor.visitFramacPredicate
- (typer_visitor lenv :> Visitor.frama_c_inplace)
+ (typing_visitor lenv :> Visitor.frama_c_inplace)
p)
let preprocess_rte ~lenv rte =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index d369220466f63974ff0d2ec2f2cac11508847858..333bd7115dd1da25c44cad16fe731c2901c9d226 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -310,36 +310,34 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
| Pfresh _ -> Env.not_yet env "\\fresh"
and to_exp ~adata ?name kf ?rte env p =
- match Logic_normalizer.get_pred p with
- | PoT_term t -> Translate_terms.to_exp ~adata kf env t
- | PoT_pred p ->
- let rte = match rte with None -> Env.generate_rte env | Some b -> b in
- Extlib.flatten
- (Env.with_params_and_result
- ~rte:false
- ~f:(fun env ->
- let e, adata, env =
- predicate_content_to_exp ~adata ?name kf env p
- in
- let env = if rte then !translate_rte_exp_ref kf env e else env in
- let cast =
- Typing.get_cast_of_predicate
- ~lenv:(Env.Local_vars.get env)
- p
- in
- Extlib.nest
- adata
- (Typed_number.add_cast
- ~loc:p.pred_loc
- ?name
- env
- kf
- cast
- Typed_number.C_number
- None
- e)
- )
- env)
+ let p = Logic_normalizer.get_pred p in
+ let rte = match rte with None -> Env.generate_rte env | Some b -> b in
+ Extlib.flatten
+ (Env.with_params_and_result
+ ~rte:false
+ ~f:(fun env ->
+ let e, adata, env =
+ predicate_content_to_exp ~adata ?name kf env p
+ in
+ let env = if rte then !translate_rte_exp_ref kf env e else env in
+ let cast =
+ Typing.get_cast_of_predicate
+ ~lenv:(Env.Local_vars.get env)
+ p
+ in
+ Extlib.nest
+ adata
+ (Typed_number.add_cast
+ ~loc:p.pred_loc
+ ?name
+ env
+ kf
+ cast
+ Typed_number.C_number
+ None
+ e)
+ )
+ env)
let generalized_untyped_to_exp ~adata ?name kf ?rte env p =
(* If [rte] is true, it means we're translating the root predicate of an