Commit 62603b24 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/lionel/recursive_global_extended_annotation' into 'master'

Recursive global extended annotations

See merge request frama-c/frama-c!2742
parents a49f2eed dbfeaee3
......@@ -207,7 +207,12 @@
match Logic_env.extension_category s with
| exception Not_found -> None
| Cil_types.Ext_contract -> Some (EXT_CONTRACT s)
| Cil_types.Ext_global -> Some (EXT_GLOBAL s)
| Cil_types.Ext_global ->
begin
match Logic_env.is_extension_block s with
| false -> Some (EXT_GLOBAL s)
| true -> Some (EXT_GLOBAL_BLOCK s)
end
| Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT s)
end
else None
......
......@@ -107,6 +107,8 @@
let loc_decl d = { decl_node = d; decl_loc = loc () }
let loc_ext d = { extended_node = d; extended_loc = loc () }
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
......@@ -253,7 +255,7 @@
%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
%token CHECK_REQUIRES CHECK_LOOP CHECK_INVARIANT CHECK_LEMMA
%token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_CONTRACT
%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT
%token EXITS BREAKS CONTINUES RETURNS
%token VOLATILE READS WRITES
%token LOGIC PREDICATE INDUCTIVE AXIOMATIC AXIOM LEMMA LBRACE RBRACE
......@@ -1532,13 +1534,34 @@ decl:
| type_annot {LDtype_annot $1}
| model_annot {LDmodel_annot $1}
| logic_def { $1 }
| EXT_GLOBAL grammar_extension SEMICOLON {
let processed = Logic_env.preprocess_extension $1 $2 in
LDextended ($1, processed)
}
| ext_decl { LDextended $1 }
| deprecated_logic_decl { $1 }
;
ext_decl:
| EXT_GLOBAL grammar_extension SEMICOLON {
let processed = Logic_env.preprocess_extension $1 $2 in
Ext_lexpr($1, processed)
}
| EXT_GLOBAL_BLOCK any_identifier LBRACE ext_decls RBRACE {
let processed_id,processed_block =
Logic_env.preprocess_extension_block $1 ($2,$4)
in
Ext_extension($1,processed_id,processed_block)
}
;
ext_decls:
| /* epsilon */
{ [] }
| ext_decl_loc ext_decls
{ $1::$2 }
;
ext_decl_loc:
| ext_decl { loc_ext $1 }
;
volatile_opt:
| /* empty */ { None, None }
| READS any_identifier volatile_opt
......@@ -1893,6 +1916,7 @@ is_acsl_spec:
is_acsl_decl_or_code_annot:
| EXT_CODE_ANNOT { $1 }
| EXT_GLOBAL { $1 }
| EXT_GLOBAL_BLOCK { $1 }
| ASSUMES { "assumes" }
| ASSERT { "assert" }
| CHECK { "check" }
......
......@@ -442,28 +442,35 @@ let hash_list f l =
| _ -> acc
in aux 47 3 l
let hash_ext_kind = function
| Ext_id i -> Datatype.Int.hash i
| Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
| Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
let compare_ext_kind k1 k2 =
match k1, k2 with
| Ext_id i1, Ext_id i2 -> Datatype.Int.compare i1 i2
| Ext_id _, _ -> 1 | _, Ext_id _ -> -1
| Ext_terms terms1, Ext_terms terms2 ->
Extlib.list_compare Logic_utils.compare_term terms1 terms2
| Ext_terms _, _ -> 1 | _, Ext_terms _ -> -1
| Ext_preds p1, Ext_preds p2 ->
Extlib.list_compare Logic_utils.compare_predicate p1 p2
module ExtMerging =
Merging
(struct
type t = acsl_extension
let hash (e : acsl_extension) =
let rec hash (e : acsl_extension) =
let hash_ext_kind = function
| Ext_id i -> Datatype.Int.hash i
| Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
| Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
| Ext_annot (id, annots) -> Datatype.String.hash id + 5 * (hash_list hash annots)
in
Datatype.String.hash e.ext_name + 5 * hash_ext_kind e.ext_kind
let compare (e1 : acsl_extension) (e2 : acsl_extension) =
let rec compare (e1 : acsl_extension) (e2 : acsl_extension) =
let compare_ext_kind k1 k2 =
match k1, k2 with
| Ext_id i1, Ext_id i2 -> Datatype.Int.compare i1 i2
| Ext_id _, _ -> 1 | _, Ext_id _ -> -1
| Ext_terms terms1, Ext_terms terms2 ->
Extlib.list_compare Logic_utils.compare_term terms1 terms2
| Ext_terms _, _ -> 1 | _, Ext_terms _ -> -1
| Ext_preds p1, Ext_preds p2 ->
Extlib.list_compare Logic_utils.compare_predicate p1 p2
| Ext_preds _, _ -> 1 | _, Ext_preds _ -> -1
| Ext_annot (id1, a1) , Ext_annot (id2, a2) ->
match String.compare id1 id2 with
| 0 -> Extlib.list_compare compare a1 a2
| n -> n
in
let res = Datatype.String.compare e1.ext_name e2.ext_name in
if res <> 0 then res
else
......
......@@ -1693,6 +1693,7 @@ and acsl_extension_kind =
| Ext_terms of term list
| Ext_preds of predicate list
(** a list of predicates, the most common case of for extensions *)
| Ext_annot of string * acsl_extension list
(** Where are we expected to find corresponding extension keyword.
@plugin development guide
......
......@@ -921,6 +921,8 @@ and pp_acsl_extension_kind fmt = function
| Ext_id(int) -> Format.fprintf fmt "Ext_id(%a)" pp_int int
| Ext_terms(term_list) -> Format.fprintf fmt "Ext_terms(%a)" (pp_list pp_term) term_list
| Ext_preds(predicate_list) -> Format.fprintf fmt "Ext_preds(%a)" (pp_list pp_predicate) predicate_list
| Ext_annot(string,annotation_list) ->
Format.fprintf fmt "Ext_annots(%a,%a)" pp_string string (pp_list pp_acsl_extension) annotation_list
and pp_behavior fmt behavior =
Format.fprintf fmt
......
......@@ -311,6 +311,15 @@ let print_model_annot fmt ty =
(print_logic_type None) ty.model_type
ty.model_name
let rec print_extended_decl fmt d =
let aux fmt d = print_extended_decl fmt d.extended_node in
match d with
| Ext_lexpr(name,d) ->
fprintf fmt "@[<2>%s@ %a@]" name (pp_list ~sep:",@ " print_lexpr) d
| Ext_extension(name,id,d) ->
fprintf fmt "@[<2>%s@ %s@ {@\n%a@]@\n}" name id
(pp_list ~sep:"@\n" aux) d
let rec print_decl fmt d =
match d.decl_node with
| LDlogic_def(name,labels,tvar,rt,prms,body) ->
......@@ -374,8 +383,7 @@ let rec print_decl fmt d =
(pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" print_lexpr) tsets
(pp_opt ~pre:"@ reads@ " pp_print_string) read
(pp_opt ~pre:"@ writes@ " pp_print_string) write
| LDextended (s,l) ->
fprintf fmt "@[<2>%s@ %a@]" s (pp_list ~sep:",@ " print_lexpr) l
| LDextended d -> print_extended_decl fmt d
let print_deps fmt deps =
match deps with
......
......@@ -28,16 +28,36 @@ type extension_preprocessor =
lexpr list -> lexpr list
type extension_typer =
typing_context -> location -> lexpr list -> acsl_extension_kind
type extension_preprocessor_block =
string * extended_decl list -> string * extended_decl list
type extension_typer_block =
typing_context -> location -> string * extended_decl list -> acsl_extension_kind
type extension_visitor =
Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
type extension_printer =
Printer_api.extensible_printer_type -> Format.formatter ->
acsl_extension_kind -> unit
type extension = {
category: ext_category ;
type extension_single = {
preprocessor: extension_preprocessor ;
typer: extension_typer ;
status: bool ;
}
type extension_block = {
preprocessor: extension_preprocessor_block ;
typer: extension_typer_block ;
status: bool ;
}
type extension_common = {
category: ext_category ;
visitor: extension_visitor ;
printer: extension_printer ;
short_printer: extension_printer ;
}
type extension = {
preprocessor: extension_preprocessor ;
typer: extension_typer ;
status: bool ;
category: ext_category ;
visitor: extension_visitor ;
printer: extension_printer ;
short_printer: extension_printer ;
......@@ -47,9 +67,10 @@ let default_printer printer fmt = function
| Ext_id i -> Format.fprintf fmt "%d" i
| Ext_terms ts -> Pretty_utils.pp_list ~sep:",@ " printer#term fmt ts
| Ext_preds ps -> Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt ps
| Ext_annot (_,an) -> Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
printer#extended fmt an
let default_short_printer name _printer fmt _ext_kind =
Format.fprintf fmt "%s" name
let default_short_printer name _printer fmt _ext_kind = Format.fprintf fmt "%s" name
let make
name category
......@@ -58,15 +79,39 @@ let make
?(visitor=fun _ _ -> Cil.DoChildren)
?(printer=default_printer)
?(short_printer=default_short_printer name)
status =
{ category; status; preprocessor; typer; visitor; printer; short_printer }
status : extension_single*extension_common =
{ preprocessor; typer; status},{ category; visitor; printer; short_printer }
let make_block
name category
?(preprocessor=Extlib.id)
typer
?(visitor=fun _ _ -> Cil.DoChildren)
?(printer=default_printer)
?(short_printer=default_short_printer name)
status : extension_block*extension_common =
{ preprocessor; typer; status},{ category; visitor; printer; short_printer }
module Extensions = struct
(*hash table for category, visitor, printer and short_printer of extensions*)
let ext_tbl = Hashtbl.create 5
let find name =
try Hashtbl.find ext_tbl name
with Not_found ->
(*hash table for status, preprocessor and typer of single extensions*)
let ext_single_tbl = Hashtbl.create 5
(*hash table for status, preprocessor and typer of block extensions*)
let ext_block_tbl = Hashtbl.create 5
let find_single name :extension_single =
try Hashtbl.find ext_single_tbl name with Not_found ->
Kernel.fatal ~current:true "unsupported clause of name '%s'" name
let find_common name :extension_common =
try Hashtbl.find ext_tbl name with Not_found ->
Kernel.fatal ~current:true "unsupported clause of name '%s'" name
let find_block name :extension_block =
try Hashtbl.find ext_block_tbl name with Not_found ->
Kernel.fatal ~current:true "unsupported clause of name '%s'" name
(* [Logic_lexer] can ask for something that is not a category, which is not
......@@ -75,21 +120,60 @@ module Extensions = struct
let is_extension = Hashtbl.mem ext_tbl
let is_extension_block = Hashtbl.mem ext_block_tbl
let register
cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
let info =
let info1,info2 =
make name cat ?preprocessor typer ?visitor ?printer ?short_printer status
in
if is_extension name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
"Trying to register ACSL extension %s twice. Ignoring second extension"
name
else Hashtbl.add ext_tbl name info
else
begin
Hashtbl.add ext_single_tbl name info1;
Hashtbl.add ext_tbl name info2
end
let preprocess name = (find name).preprocessor
let register_block
cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
let info1,info2 =
make_block name cat ?preprocessor typer ?visitor ?printer ?short_printer status
in
if is_extension name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
"Trying to register ACSL extension %s twice. Ignoring second extension"
name
else
begin
Hashtbl.add ext_block_tbl name info1;
Hashtbl.add ext_tbl name info2
end
let preprocess name = (find_single name).preprocessor
let preprocess_block name = (find_block name).preprocessor
let typing name typing_context loc es =
let ext_info = find name in
let ext_info = find_single name in
let status = ext_info.status in
let typer = ext_info.typer in
let normal_error = ref false in
let has_error () = normal_error := true in
let wrapper =
typing_context.on_error (typer typing_context loc) has_error
in
try status, wrapper es
with
| (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
| exn when not !normal_error ->
Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
name (Printexc.to_string exn)
let typing_block name typing_context loc es =
let ext_info = find_block name in
let status = ext_info.status in
let typer = ext_info.typer in
let normal_error = ref false in
......@@ -104,14 +188,18 @@ module Extensions = struct
Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
name (Printexc.to_string exn)
let visit name = (find name).visitor
let visit name = (find_common name).visitor
let print name printer fmt kind =
let pp = (find name).printer printer in
Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
let pp = (find_common name).printer printer in
match kind with
| Ext_annot (id,_) ->
Format.fprintf fmt "@[<v 2>@[%s %s {@]@\n%a}@]" name id pp kind
| _ ->
Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
let short_print name printer fmt kind =
let pp = (find name).short_printer in
let pp = (find_common name).short_printer in
Format.fprintf fmt "%a" (pp printer) kind
end
......@@ -121,6 +209,8 @@ let register_behavior =
Extensions.register Ext_contract
let register_global =
Extensions.register Ext_global
let register_global_block =
Extensions.register_block Ext_global
let register_code_annot =
Extensions.register (Ext_code_annot Ext_here)
let register_code_annot_next_stmt =
......@@ -136,10 +226,13 @@ let () =
Logic_env.set_extension_handler
~category:Extensions.category
~is_extension: Extensions.is_extension
~preprocess: Extensions.preprocess ;
~preprocess: Extensions.preprocess
~is_extension_block: Extensions.is_extension_block
~preprocess_block: Extensions.preprocess_block;
Logic_typing.set_extension_handler
~is_extension: Extensions.is_extension
~typer: Extensions.typing ;
~typer: Extensions.typing
~typer_block: Extensions.typing_block ;
Cil.set_extension_handler
~visit: Extensions.visit ;
Cil_printer.set_extension_handler
......@@ -148,21 +241,45 @@ let () =
(* For Deprecation: *)
let deprecated_replace name ext = Hashtbl.add Extensions.ext_tbl name ext
let deprecated_replace name ext =
let info1:extension_single = {
preprocessor = ext.preprocessor ;
typer = ext.typer ;
status = ext.status ;
}
in
let info2:extension_common = {
category = ext.category ;
visitor = ext.visitor ;
printer = ext.printer ;
short_printer = ext.printer ;
}
in
Hashtbl.add Extensions.ext_single_tbl name info1;
Hashtbl.add Extensions.ext_tbl name info2
let strong_cat = Hashtbl.create 5
let default_typer _typing_context _loc _l = assert false
let merge ((info1:extension_single),(info2:extension_common)) :extension =
{preprocessor = info1.preprocessor ;
typer = info1.typer ;
status = info1.status ;
category = info2.category ;
visitor = info2.visitor ;
printer = info2.printer ;
short_printer = info2.printer}
let deprecated_find ?(strong=true) name cat op_name =
match Hashtbl.find_opt Extensions.ext_tbl name with
match Hashtbl.find_opt Extensions.ext_single_tbl name with
| None ->
if strong then Hashtbl.add strong_cat name cat ;
(make name cat default_typer false)
| Some ext ->
merge (make name cat default_typer false)
| Some ext1 ->
let ext2 = Extensions.find_common name in
if strong && Hashtbl.mem strong_cat name then begin
if ext.category = cat then ext
if ext2.category = cat then merge (ext1,ext2)
else
Kernel.fatal
"Registring %s for %s: this extension already exists for another \
......@@ -170,8 +287,9 @@ let deprecated_find ?(strong=true) name cat op_name =
op_name name
end else if strong then begin
Hashtbl.add strong_cat name cat ;
{ ext with category = cat }
end else ext
let ext2 = { ext2 with category = cat } in
merge (ext1,ext2)
end else merge (ext1,ext2)
let deprecated_register_typing name cat status typer =
deprecated_replace name
......
......@@ -38,6 +38,10 @@ type extension_typer =
(** Visitor functions for ACSL extensions *)
type extension_visitor =
Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
type extension_preprocessor_block =
string * extended_decl list -> string * extended_decl list
type extension_typer_block =
typing_context -> location -> string * extended_decl list -> acsl_extension_kind
(** Pretty printers for ACSL extensions *)
type extension_printer =
Printer_api.extensible_printer_type -> Format.formatter ->
......@@ -106,6 +110,16 @@ val register_global:
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
(** Registers extension for global block annotation. See [register_behavior].
@plugin development guide
*)
val register_global_block:
string -> ?preprocessor:extension_preprocessor_block -> extension_typer_block ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
(** Registers extension for code annotation to be evaluated at _current_
program point. See [register_behavior].
......
......@@ -1994,6 +1994,9 @@ and childrenCilExtended vis p =
| Ext_preds preds ->
let preds' = mapNoCopy (visitCilPredicate vis) preds in
if preds == preds' then p else Ext_preds preds'
| Ext_annot (id,annots) ->
let annots' = mapNoCopy (visitCilExtended vis) annots in
if annots == annots' then p else Ext_annot (id,annots')
and visitCilPredicates vis ps = mapNoCopy (visitCilIdPredicate vis) ps
......
......@@ -29,23 +29,32 @@ module Extensions = struct
let ref_is_extension = ref (fun _ -> assert false)
let ref_category = ref (fun _ -> assert false)
let ref_preprocess = ref (fun _ -> assert false)
let ref_is_extension_block = ref (fun _ -> assert false)
let ref_preprocess_block = ref (fun _ -> assert false)
let set_extension_handler ~category ~is_extension ~preprocess =
let set_extension_handler
~category ~is_extension ~preprocess ~is_extension_block ~preprocess_block =
assert (not !initialized) ;
ref_is_extension := is_extension ;
ref_category := category ;
ref_preprocess := preprocess ;
ref_is_extension_block := is_extension_block;
ref_preprocess_block := preprocess_block;
initialized := true ;
()
let is_extension s = !ref_is_extension s
let is_extension_block s = !ref_is_extension_block s
let category s = !ref_category s
let preprocess s = !ref_preprocess s
let preprocess_block s = !ref_preprocess_block s
end
let set_extension_handler = Extensions.set_extension_handler
let is_extension = Extensions.is_extension
let is_extension_block = Extensions.is_extension_block
let extension_category = Extensions.category
let preprocess_extension = Extensions.preprocess
let preprocess_extension_block = Extensions.preprocess_block
module CurrentLoc = Cil_const.CurrentLoc
......
......@@ -29,12 +29,16 @@ open Cil_types
(** {2 registered ACSL extensions } *)
val is_extension: string -> bool
val is_extension_block: string -> bool
val extension_category: string -> ext_category
val preprocess_extension:
string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list
val preprocess_extension_block:
string -> string * Logic_ptree.extended_decl list -> string * Logic_ptree.extended_decl list
(** {2 Global Tables} *)
module Logic_info: State_builder.Hashtbl
with type key = string and type data = Cil_types.logic_info list
......@@ -208,6 +212,10 @@ val set_extension_handler:
category:(string -> ext_category) ->
is_extension:(string -> bool) ->
preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
is_extension_block:(string -> bool) ->
preprocess_block:
(string -> string * Logic_ptree.extended_decl list ->
string * Logic_ptree.extended_decl list) ->
unit
(** Used to setup references related to the handling of ACSL extensions.
If your name is not [Acsl_extension], do not call this
......
......@@ -528,11 +528,13 @@ module Extensions = struct
let initialized = ref false
let ref_is_extension = ref (fun _ -> assert false)
let ref_typer = ref (fun _ _ _ _ -> assert false)
let ref_typer_block = ref (fun _ _ _ _ -> assert false)
let set_handler ~is_extension ~typer =
let set_handler ~is_extension ~typer ~typer_block =
assert (not !initialized) ;
ref_is_extension := is_extension ;
ref_typer := typer ;
ref_typer_block := typer_block;
initialized := true
let is_extension name = !ref_is_extension name
......@@ -540,6 +542,9 @@ module Extensions = struct
let typer name ~typing_context:typing_context ~loc =
!ref_typer name typing_context loc
let typer_block name ~typing_context:typing_context ~loc =
!ref_typer_block name typing_context loc
(* For deprecated functions *)
let ref_deprecated_handler = ref (fun _ _ _ _ -> assert false)
......@@ -551,6 +556,8 @@ module Extensions = struct
!ref_deprecated_handler name category status typer
end
let set_extension_handler = Extensions.set_handler
let get_typer = Extensions.typer
let get_typer_block = Extensions.typer_block
(* Deprecated ACSL extensions functions *)
let set_deprecated_extension_handler =
......@@ -4281,11 +4288,18 @@ struct
let rvi_opt = get_volatile_fct checks_reads_fct rd_opt in
let wvi_opt = get_volatile_fct checks_writes_fct wr_opt in
Dvolatile (tsets, rvi_opt, wvi_opt, [], loc)
| LDextended (kind, content) ->
| LDextended (Ext_lexpr(kind, content)) ->
let typing_context = base_ctxt (Lenv.empty ()) in
let status,tcontent = Extensions