From 69731fb8fd9e59ed0dcba44cb703f417fb4929e7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 28 Jan 2020 10:49:42 +0100
Subject: [PATCH] [Parsing] lexical transformation for ACSL extensions
---
src/kernel_internals/parsing/logic_parser.mly | 99 ++++++++++---------
.../ast_queries/acsl_extension.ml | 11 ++-
.../ast_queries/acsl_extension.mli | 3 +
src/kernel_services/ast_queries/logic_env.ml | 5 +-
src/kernel_services/ast_queries/logic_env.mli | 4 +
tests/spec/Extend_preprocess.i | 31 ++++++
tests/spec/Extend_preprocess.ml | 53 ++++++++++
.../spec/oracle/Extend_preprocess.res.oracle | 43 ++++++++
8 files changed, 201 insertions(+), 48 deletions(-)
create mode 100644 tests/spec/Extend_preprocess.i
create mode 100644 tests/spec/Extend_preprocess.ml
create mode 100644 tests/spec/oracle/Extend_preprocess.res.oracle
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 7d800ea9fe6..243757e9f38 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -109,14 +109,14 @@
let concat_froms a1 a2 =
let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
- (* NB: the following has an horrible complexity, but the order of
+ (* NB: the following has an horrible complexity, but the order of
clauses in the input is preserved. *)
let concat_one acc (_,f2 as p) =
try
let (_,f1) = List.find (compare_pair p) acc
in
match (f1, f2) with
- | _,FromAny ->
+ | _,FromAny ->
(* the new fundeps does not give more information than the one
which is already present. Just ignore it.
*)
@@ -125,11 +125,11 @@
(* the new fundeps is strictly more precise than the old one.
We replace the old dependency by the new one, but keep
the location at its old place in the list. This ensures
- that we get the exact same clause if we try to
+ that we get the exact same clause if we try to
link the original contract with its pretty-printed version. *)
Extlib.replace compare_pair p acc
- | From _, From _ ->
- (* we keep the two functional dependencies,
+ | From _, From _ ->
+ (* we keep the two functional dependencies,
as they have to be proved separately. *)
acc @ [p]
with Not_found -> acc @ [p]
@@ -140,7 +140,7 @@
| FreeAllocAny,_ -> fa2
| _,FreeAllocAny -> fa1
| FreeAlloc(f1,a1),FreeAlloc(f2,a2) -> FreeAlloc(f2@f1,a2@a1)
-
+
(* a1 represents the assigns _after_ the current clause a2. *)
let concat_assigns a1 a2 =
match a1,a2 with
@@ -152,17 +152,17 @@
| Writes a1, a2 -> Writes (concat_froms a2 a1)
let concat_loop_assigns_allocation annots bhvs2 a2 fa2=
- (* NB: this is supposed to merge assigns related to named behaviors, in
+ (* NB: this is supposed to merge assigns related to named behaviors, in
case of annotation like
for a,b: assigns x,y;
for b,c: assigns z,t;
- DO NOT CALL this function for loop assigns not attached to specific
- behaviors.
+ DO NOT CALL this function for loop assigns not attached to specific
+ behaviors.
*)
assert (bhvs2 <> []);
- if fa2 == FreeAllocAny && a2 == WritesAny
+ if fa2 == FreeAllocAny && a2 == WritesAny
then annots
- else
+ else
let split l1 l2 =
let treat_one (only1,both,only2) x =
if List.mem x l1 then
@@ -201,12 +201,12 @@
let (bhvs2, annots) = List.fold_right treat_one annots (bhvs2,[]) in
match bhvs2 with
| [] -> annots (* Already considered all cases. *)
- | _ ->
- let annots = if a2 <> WritesAny
+ | _ ->
+ let annots = if a2 <> WritesAny
then AAssigns (bhvs2,a2) :: annots
else annots
- in
- if fa2 <> FreeAllocAny
+ in
+ if fa2 <> FreeAllocAny
then AAllocation (bhvs2,fa2) :: annots
else annots
@@ -362,9 +362,9 @@ lexpr:
{ info (PLif ($1, $3, $5)) }
/* both terms and predicates */
| any_identifier COLON lexpr %prec prec_named { info (PLnamed ($1, $3)) }
-| string COLON lexpr %prec prec_named
+| string COLON lexpr %prec prec_named
{ let (iswide,str) = $1 in
- if iswide then begin
+ if iswide then begin
let l = loc () in
raise (Not_well_formed(l, "Wide strings are not allowed as labels."))
end;
@@ -459,15 +459,15 @@ lexpr_inner:
| VALID opt_label_1 LPAR lexpr RPAR { info (PLvalid ($2,$4)) }
| VALID_READ opt_label_1 LPAR lexpr RPAR { info (PLvalid_read ($2,$4)) }
| VALID_FUNCTION LPAR lexpr RPAR { info (PLvalid_function $3) }
-| VALID_INDEX opt_label_1 LPAR lexpr COMMA lexpr RPAR {
+| VALID_INDEX opt_label_1 LPAR lexpr COMMA lexpr RPAR {
let source = fst (loc ()) in
obsolete ~source "\\valid_index(addr,idx)" ~now:"\\valid(addr+idx)";
info (PLvalid ($2,info (PLbinop ($4, Badd, $6)))) }
| VALID_RANGE opt_label_1 LPAR lexpr COMMA lexpr COMMA lexpr RPAR {
let source = fst (loc ()) in
- obsolete "\\valid_range(addr,min,max)"
+ obsolete "\\valid_range(addr,min,max)"
~source ~now:"\\valid(addr+(min..max))";
- info (PLvalid
+ info (PLvalid
($2,info (PLbinop ($4, Badd, (info (PLrange((Some $6),Some $8)))))))
}
| INITIALIZED opt_label_1 LPAR lexpr RPAR { info (PLinitialized ($2,$4)) }
@@ -953,7 +953,7 @@ ext_function_specs_opt:
;
ext_function_specs:
-| ext_at_stmt_markup { []}
+| ext_at_stmt_markup { []}
| ext_function_spec { [$1] }
| ext_function_spec ext_function_specs { $1::$2 }
;
@@ -969,7 +969,7 @@ ext_fun_specs:
;
ext_fun_spec:
-| ext_at_stmt_markup ext_stmt_loop_spec
+| ext_at_stmt_markup ext_stmt_loop_spec
{ Ext_stmt($1,$2,loc()) }
| ext_contract_markup contract
{ let s,pos = $2 in Ext_spec (s,pos) }
@@ -981,7 +981,7 @@ ext_stmt_loop_spec:
;
ext_identifier_opt:
-| /* empty*/ { "" }
+| /* empty*/ { "" }
| ext_identifier { $1 }
;
@@ -1030,12 +1030,12 @@ contract:
let behaviors =
if requires <> [] || post_cond <> [] ||
allocation <> FreeAllocAny ||
- assigns <> WritesAny || extended <> []
+ assigns <> WritesAny || extended <> []
then
(Cabshelper.mk_behavior
~requires ~post_cond ~assigns ~allocation ~extended ())
:: behaviors
- else if $2<>None || $3<>None ||
+ else if $2<>None || $3<>None ||
behaviors<>[] || completes<>[] ||disjoints<>[]
then behaviors
else raise (Not_well_formed (loc(),"Empty annotation is not allowed"))
@@ -1100,7 +1100,7 @@ clause_kw:
| FREES {"frees"}
| COMPLETE {"complete"}
| DISJOINT {"disjoint"}
-/* often, we'll be in c_kw_mode, where these keywords are
+/* often, we'll be in c_kw_mode, where these keywords are
recognized as identifiers... */
| IDENTIFIER { $1 }
| EXT_CONTRACT { $1 }
@@ -1166,7 +1166,8 @@ ne_simple_clauses:
}
| EXT_CONTRACT grammar_extension SEMICOLON simple_clauses
{ let allocation,assigns,post_cond,extended = $4 in
- allocation,assigns,post_cond,($1,$2)::extended
+ let processed = Logic_env.preprocess_extension $1 $2 in
+ allocation,assigns,post_cond,($1,processed)::extended
}
| post_cond_kind full_lexpr clause_kw { missing 2 ";" $3 }
| allocation clause_kw { missing 1 ";" $2 }
@@ -1301,7 +1302,7 @@ loop_annotations:
let ext = List.map (fun x -> AExtended([],true, x)) e in
let oth = match a with
| WritesAny -> b
- | Writes _ ->
+ | Writes _ ->
(* by definition all existing AAssigns are tied to at least
one behavior. No need to merge against them. *)
AAssigns ([],a)::b
@@ -1338,7 +1339,7 @@ loop_annot_stack:
check_empty
(pos, "loop extension is not allowed after loop variant.") e;
(match fa with
- | FreeAlloc(f,a) ->
+ | FreeAlloc(f,a) ->
check_empty
(pos,"loop frees is not allowed after loop variant.") f ;
check_empty
@@ -1346,9 +1347,9 @@ loop_annot_stack:
| FreeAllocAny -> ());
(match a with
WritesAny -> ()
- | Writes _ ->
- raise
- (Not_well_formed
+ | Writes _ ->
+ raise
+ (Not_well_formed
(pos,"loop assigns is not allowed after loop variant.")));
check_empty
(pos,"loop behavior is not allowed after loop variant.") b ;
@@ -1392,7 +1393,9 @@ loop_grammar_extension:
let open Cil_types in
let ext = $2 in
match Logic_env.extension_category ext with
- | Some (Ext_code_annot (Ext_next_loop | Ext_next_both)) -> (ext, $3)
+ | Some (Ext_code_annot (Ext_next_loop | Ext_next_both)) ->
+ let processed = Logic_env.preprocess_extension ext $3 in
+ (ext, processed)
| Some (Ext_code_annot (Ext_here | Ext_next_stmt)) ->
raise
(Not_well_formed
@@ -1446,7 +1449,8 @@ code_annotation:
let ext = $1 in
match Logic_env.extension_category ext with
| Some (Ext_code_annot (Ext_here | Ext_next_stmt | Ext_next_both)) ->
- Logic_ptree.AExtended(bhvs,false,(ext,$2))
+ let processed = Logic_env.preprocess_extension ext $2 in
+ Logic_ptree.AExtended(bhvs,false,(ext,processed))
| Some (Ext_code_annot Ext_next_loop) ->
raise
(Not_well_formed
@@ -1491,7 +1495,10 @@ decl:
| type_annot {LDtype_annot $1}
| model_annot {LDmodel_annot $1}
| logic_def { $1 }
-| EXT_GLOBAL grammar_extension SEMICOLON { LDextended ($1, $2) }
+| EXT_GLOBAL grammar_extension SEMICOLON {
+ let processed = Logic_env.preprocess_extension $1 $2 in
+ LDextended ($1, processed)
+ }
| deprecated_logic_decl { $1 }
;
@@ -1516,7 +1523,7 @@ volatile_opt:
type_annot:
| TYPE INVARIANT any_identifier LPAR full_parameter RPAR EQUAL
full_lexpr SEMICOLON
- { let typ,name = $5 in{ inv_name = $3; this_name = name; this_type = typ; inv = $8; } }
+ { let typ,name = $5 in{ inv_name = $3; this_name = name; this_type = typ; inv = $8; } }
;
opt_semicolon:
@@ -1525,8 +1532,8 @@ opt_semicolon:
model_annot:
| MODEL type_spec LBRACE full_parameter opt_semicolon RBRACE SEMICOLON
- { let typ,name = $4 in
- { model_for_type = $2; model_name = name; model_type = typ; }
+ { let typ,name = $4 in
+ { model_for_type = $2; model_name = name; model_type = typ; }
}
;
@@ -1612,7 +1619,7 @@ deprecated_logic_decl:
exit_type_variables_scope ();
let source = fst (loc ()) in
obsolete "logic type declaration" ~source ~now:"an axiomatic block";
- LDtype(id,tvars,None)
+ LDtype(id,tvars,None)
}
/* OBSOLETE: axiom */
| AXIOM poly_id COLON full_lexpr SEMICOLON
@@ -1710,21 +1717,21 @@ ne_label_list:
| label_name COMMA ne_label_list { $1 :: $3 }
;
-opt_label_1:
-| opt_label_list { match $1 with
+opt_label_1:
+| opt_label_list { match $1 with
| [] -> None
| l::[] -> Some l
| _ -> raise (Not_well_formed (loc(),"Only one label is allowed")) }
;
-
-opt_label_2:
-| opt_label_list { match $1 with
+
+opt_label_2:
+| opt_label_list { match $1 with
| [] -> None
| l1::l2::[] -> Some (l1,l2)
| _::[] -> raise (Not_well_formed (loc(),"One label is missing"))
| _ -> raise (Not_well_formed (loc(),"Only two labels are allowed")) }
;
-
+
opt_label_list:
| /* epsilon */ { [] }
| LBRACE ne_label_list RBRACE { $2 }
@@ -1884,7 +1891,7 @@ non_logic_keyword:
| is_acsl_spec { $1 }
| is_acsl_decl_or_code_annot { $1 }
| is_acsl_other { $1 }
-| CUSTOM { "custom" (* token that cannot be used in C fields *) }
+| CUSTOM { "custom" (* token that cannot be used in C fields *) }
;
bs_keyword:
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 6bc74220684..b8b92d6f74a 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -26,10 +26,13 @@ open Logic_ptree
type extension_info = {
ext_status: bool ;
+ ext_preprocess: extension_preprocessing ;
ext_typing: extension_typing ;
ext_visit: extension_visit ;
ext_printing: extension_printing ;
}
+and extension_preprocessing =
+ lexpr list -> lexpr list
and extension_typing =
typing_context -> location -> lexpr list -> acsl_extension_kind
and extension_visit =
@@ -40,6 +43,8 @@ and extension_printing =
(* Default extension *)
+let default_preprocessing = Extlib.id
+
let default_typing typing_context loc l =
let _ = loc in
let typing = typing_context.type_predicate typing_context (Lenv.empty ()) in
@@ -54,6 +59,7 @@ let default_printing printer fmt = function
let default = {
ext_status = false ;
+ ext_preprocess = default_preprocessing ;
ext_typing = default_typing ;
ext_printing = default_printing ;
ext_visit = default_visit ;
@@ -79,6 +85,8 @@ module Extensions = struct
name
else Hashtbl.add ext_tbl name (category, info)
+ let preprocess name = (find name).ext_preprocess
+
let typing name typing_context loc es =
let ext_info = find name in
let status = ext_info.ext_status in
@@ -109,7 +117,8 @@ let register_code_annot_next_both =
let () =
Logic_env.set_extension_handler
~category:Extensions.category
- ~is_extension: Extensions.is_extension ;
+ ~is_extension: Extensions.is_extension
+ ~preprocess: Extensions.preprocess ;
Logic_typing.set_extension_handler
~is_extension: Extensions.is_extension
~typer: Extensions.typing ;
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index f6114dec250..8e9d0dae0db 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -26,10 +26,13 @@ open Logic_ptree
type extension_info = {
ext_status: bool ;
+ ext_preprocess: extension_preprocessing ;
ext_typing: extension_typing ;
ext_visit: extension_visit ;
ext_printing: extension_printing ;
}
+and extension_preprocessing =
+ lexpr list -> lexpr list
and extension_typing =
typing_context -> location -> lexpr list -> acsl_extension_kind
and extension_visit =
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 0d7f4da3712..fdadf34d678 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -27,16 +27,19 @@ open Cil_types
let initialized_extensions = ref false
let ref_is_extension = ref (fun _ -> assert false)
let ref_extension_category = ref (fun _ -> assert false)
+let ref_preprocess_extension = ref (fun _ -> assert false)
-let set_extension_handler ~category ~is_extension =
+let set_extension_handler ~category ~is_extension ~preprocess =
assert (not !initialized_extensions) ;
ref_is_extension := is_extension ;
ref_extension_category := category ;
+ ref_preprocess_extension := preprocess ;
initialized_extensions := true ;
()
let is_extension s = !ref_is_extension s
let extension_category s = !ref_extension_category s
+let preprocess_extension s = !ref_preprocess_extension s
module CurrentLoc = Cil_const.CurrentLoc
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index bc9cf490523..3cf0a69b6a2 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -32,6 +32,9 @@ val is_extension: string -> bool
val extension_category: string -> ext_category option
+val preprocess_extension:
+ string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list
+
(** {2 Global Tables} *)
module Logic_info: State_builder.Hashtbl
with type key = string and type data = Cil_types.logic_info list
@@ -204,6 +207,7 @@ val builtin_types_as_typenames: unit -> unit
val set_extension_handler:
category:(string -> ext_category option) ->
is_extension:(string -> bool) ->
+ preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
unit
(** Used to setup references related to the handling of ACSL extensions.
If your name is not [Acsl_extension], do not call this
diff --git a/tests/spec/Extend_preprocess.i b/tests/spec/Extend_preprocess.i
new file mode 100644
index 00000000000..24b2d061048
--- /dev/null
+++ b/tests/spec/Extend_preprocess.i
@@ -0,0 +1,31 @@
+/* run.config
+MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
+*/
+
+/*@ bhv_foo must_replace(x); */
+int f(int x);
+
+/*@ behavior test:
+ bhv_foo must_replace(x);
+*/
+int g(int x);
+
+
+int f(int x) {
+ int s = 0;
+ /*@ loop nl_foo must_replace(x); */
+ for (int i = 0; i < x; i++) s+=g(i);
+ /*@ ca_foo must_replace(x); */
+ return s;
+}
+
+int k(int z) {
+ int x = z;
+ int y = 0;
+ /*@ ns_foo must_replace(x); */
+ y = x++;
+ return y;
+}
+
+/*@ gl_foo must_replace(x); */
diff --git a/tests/spec/Extend_preprocess.ml b/tests/spec/Extend_preprocess.ml
new file mode 100644
index 00000000000..d2905255e14
--- /dev/null
+++ b/tests/spec/Extend_preprocess.ml
@@ -0,0 +1,53 @@
+open Logic_ptree
+open Logic_const
+
+(* For each kind of extension:
+ - behavior: bhv
+ - next loop: nl
+ - code annotation: ca
+ - next statement: ns
+ - global: gl
+ replaces node "must_replace(x)" with "<kind>_ok(x)". The typing phase
+ validates that we find the right "<kind>_ok" for each kind of extension:
+ - if a must_replaced is found, it fails,
+ - if the wrong kind is found, a "\false" is generated
+ - if everything is ok "\true" is generated
+*)
+
+let validate kind call =
+ assert (not (String.equal "must_replace" call)) ;
+ match String.split_on_char '_' call with
+ | [ lkind ; lok ] -> String.equal kind lkind && String.equal lok "ok"
+ | _ -> false
+
+let ext_typing kind typing_context loc l =
+ let _ = loc in
+ let _ = typing_context in
+ let type_lexpr = function
+ | { lexpr_node = PLapp(s, [], [ _ ]) } when validate kind s -> ptrue
+ | _ -> pfalse
+ in
+ Cil_types.Ext_preds (List.map type_lexpr l)
+
+let preprocess_foo_ptree_element kind = function
+ | { lexpr_node = PLapp("must_replace", [], [ v ]) } as x ->
+ { x with lexpr_node = PLapp(kind ^ "_ok", [], [ v ]) }
+ | x -> x
+
+let preprocess_foo_ptree kind = List.map (preprocess_foo_ptree_element kind)
+
+let register registration kind =
+ let ext = {
+ Acsl_extension.default with
+ ext_typing = ext_typing kind ;
+ ext_preprocess = preprocess_foo_ptree kind
+ } in
+ registration (kind ^ "_foo") ext
+
+let () =
+ let open Acsl_extension in
+ register register_behavior "bhv" ;
+ register register_code_annot_next_loop "nl";
+ register register_code_annot "ca";
+ register register_code_annot_next_stmt "ns";
+ register register_global "gl"
diff --git a/tests/spec/oracle/Extend_preprocess.res.oracle b/tests/spec/oracle/Extend_preprocess.res.oracle
new file mode 100644
index 00000000000..843b1e4bc8d
--- /dev/null
+++ b/tests/spec/oracle/Extend_preprocess.res.oracle
@@ -0,0 +1,43 @@
+[kernel] Parsing tests/spec/Extend_preprocess.i (no preprocessing)
+/* Generated by Frama-C */
+int f(int x);
+
+/*@ behavior test:
+ bhv_foo \true; */
+int g(int x);
+
+/*@ bhv_foo \true; */
+int f(int x)
+{
+ int s = 0;
+ {
+ int i = 0;
+ /*@ loop nl_foo \true; */
+ while (i < x) {
+ int tmp;
+ tmp = g(i);
+ s += tmp;
+ i ++;
+ }
+ }
+ /*@ ca_foo \true; */ ;
+ return s;
+}
+
+int k(int z)
+{
+ int tmp;
+ int x = z;
+ int y = 0;
+ /*@ ns_foo \true; */
+ { /* sequence */
+ tmp = x;
+ x ++;
+ y = tmp;
+ }
+ return y;
+}
+
+/*@ gl_foo \true;
+*/
+
--
GitLab