Commit a6e0fae8 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[kernel] introduce status flag for acsl-extensions

parent ec3725b2
......@@ -461,16 +461,21 @@ module ExtMerging =
Merging
(struct
type t = acsl_extension
let hash (_,name,_,kind) =
let hash ((_,name,_,_,kind) : acsl_extension) =
Datatype.String.hash name + 5 * hash_ext_kind kind
let compare (_,name1, _,kind1) (_,name2,_,kind2) =
let compare
((_,name1,_,s1,kind1) : acsl_extension)
((_,name2,_,s2,kind2) : acsl_extension) =
let res = Datatype.String.compare name1 name2 in
if res <> 0 then res
else
compare_ext_kind kind1 kind2
let res = Datatype.Bool.compare s1 s2 in
if res <> 0 then res
else
compare_ext_kind kind1 kind2
let equal x y = compare x y = 0
let merge_synonym _ = true
let output fmt (_,name,_,_) =
let output fmt (_,name,_,_,_) =
Format.fprintf fmt "global ACSL extension %s" name
end)
......
......@@ -1646,6 +1646,11 @@ and spec = {
(** Extension to standard ACSL clause with an unique identifier.
The integer is a (unique) identifier.
The boolean flag is [true] if the annotation can be assigned a
property status.
Use {!Logic_const.new_acsl_extension} to create new acsl extension with
a fresh id.
Each extension is associated with a keyword, and can be either a global
......@@ -1664,7 +1669,7 @@ and spec = {
grammar ambiguous.
@plugin development guide *)
and acsl_extension = int * string * location * acsl_extension_kind
and acsl_extension = int * string * location * bool * acsl_extension_kind
(** @plugin development guide *)
and acsl_extension_kind =
......
......@@ -246,7 +246,7 @@ let rec location = function
| [] -> Cil_datatype.Location.unknown
| p :: _ -> location p)
| IPLemma (_,_,_,_,loc) -> loc
| IPExtended(_,(_,_,loc,_)) -> loc
| IPExtended(_,(_,_,loc,_,_)) -> loc
| IPOther(_,loc_e) -> loc_of_loc_o loc_e
| IPTypeInvariant(_,_,_,loc) | IPGlobalInvariant(_,_,loc) -> loc
......@@ -413,7 +413,7 @@ include Datatype.Make_with_collections
| IPOther(s,_) -> Hashtbl.hash (15, (s:string))
| IPTypeInvariant(s,_,_,_) -> Hashtbl.hash (16, (s:string))
| IPGlobalInvariant(s,_,_) -> Hashtbl.hash (17, (s:string))
| IPExtended (_,(i,_,_,_)) -> Hashtbl.hash (18, i)
| IPExtended (_,(i,_,_,_,_)) -> Hashtbl.hash (18, i)
let rec equal p1 p2 =
let eq_bhv (f1,ki1,b1) (f2,ki2,b2) =
......@@ -430,7 +430,7 @@ include Datatype.Make_with_collections
in
match p1, p2 with
| IPPredicate (_,_,_,s1), IPPredicate (_,_,_,s2) -> s1.ip_id = s2.ip_id
| IPExtended (_,(i1,_,_,_)), IPExtended (_,(i2,_,_,_)) -> Datatype.Int.equal i1 i2
| IPExtended (_,(i1,_,_,_,_)), IPExtended (_,(i2,_,_,_,_)) -> Datatype.Int.equal i1 i2
| IPAxiom (s1,_,_,_,_), IPAxiom (s2,_,_,_,_)
| IPAxiomatic(s1, _), IPAxiomatic(s2, _)
| IPTypeInvariant(s1,_,_,_), IPTypeInvariant(s2,_,_,_)
......@@ -490,7 +490,7 @@ include Datatype.Make_with_collections
match x, y with
| IPPredicate (_,_,_,s1), IPPredicate (_,_,_,s2) ->
Datatype.Int.compare s1.ip_id s2.ip_id
| IPExtended (_,(i1,_,_,_)), IPExtended (_,(i2,_,_,_)) ->
| IPExtended (_,(i1,_,_,_,_)), IPExtended (_,(i2,_,_,_,_)) ->
Datatype.Int.compare i1 i2
| IPCodeAnnot(_,_,ca1), IPCodeAnnot(_,_,ca2) ->
Datatype.Int.compare ca1.annot_id ca2.annot_id
......@@ -572,7 +572,7 @@ let rec short_pretty fmt p = match p with
| IPPredicate (_,_,_,{ ip_content = {pred_name = name :: _ }}) ->
Format.pp_print_string fmt name
| IPPredicate _ -> pretty fmt p
| IPExtended (_,(_,name,_,_)) -> Format.pp_print_string fmt name
| IPExtended (_,(_,name,_,_,_)) -> Format.pp_print_string fmt name
| IPAxiom (name,_,_,_,_) | IPLemma(name,_,_,_,_)
| IPTypeInvariant(name,_,_,_) -> Format.pp_print_string fmt name
| IPGlobalInvariant(name,_,_) -> Format.pp_print_string fmt name
......@@ -861,7 +861,7 @@ struct
Format.asprintf "%s%s%a"
(kf_prefix kf) (predicate_kind_txt pk ki)
pp_names idp.ip_content.pred_name
| IPExtended (le,(_,name,_,_)) ->
| IPExtended (le,(_,name,_,_,_)) ->
Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [name]
| IPCodeAnnot (kf,_, ca) ->
let name = match ca.annot_content with
......@@ -1045,7 +1045,7 @@ struct
| IPCodeAnnot (kf,stmt, { annot_content = APragma _ } ) ->
[ K kf ; A "pragma" ; S stmt ]
| IPCodeAnnot (kf,stmt, { annot_content = AExtended(_,_,(_,clause,_,_)) } )
| IPCodeAnnot (kf,stmt, { annot_content = AExtended(_,_,(_,clause,_,_,_)) } )
-> [ K kf ; A clause ; S stmt ]
| IPCodeAnnot (kf,_, { annot_content = AAssert(_,p) } ) ->
......@@ -1089,9 +1089,9 @@ struct
| IPOther(name,OLContract kf) -> [ K kf ; A name ]
| IPOther(name,OLStmt(kf,s)) -> [ K kf ; A name ; S s ]
| IPExtended(ELGlob,(_,name,_,_)) -> [ A name ]
| IPExtended(ELContract(kf),(_,name,_,_)) -> [ K kf ; A name ]
| IPExtended(ELStmt(kf,s),(_,name,_,_)) -> [ K kf ; A name ; S s ]
| IPExtended(ELGlob,(_,name,_,_,_)) -> [ A name ]
| IPExtended(ELContract(kf),(_,name,_,_,_)) -> [ K kf ; A name ]
| IPExtended(ELStmt(kf,s),(_,name,_,_,_)) -> [ K kf ; A name ; S s ]
| IPPropertyInstance (_, _, _, ip) -> parts_of_property ip
......@@ -1330,7 +1330,8 @@ let ip_of_code_annot kf stmt ca =
| APragma p when Logic_utils.is_property_pragma p ->
[ IPCodeAnnot (kf,stmt,ca) ]
| APragma _ -> []
| AExtended _ -> []
| AExtended(_,_,(_,_,_,status,_ as ext)) ->
if status then [IPExtended(ELStmt(kf,stmt),ext)] else []
let ip_of_code_annot_single kf stmt ca = match ip_of_code_annot kf stmt ca with
| [] ->
......
......@@ -42,7 +42,7 @@ module Behavior_extensions = struct
| Ext_preds preds ->
Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt preds
let pp (printer) fmt (_, name, _, ext) =
let pp (printer) fmt (_,name,_,_,ext) =
let pp =
try
Hashtbl.find printer_tbl name
......@@ -2675,8 +2675,8 @@ class cil_printer () = object (self)
self#pp_acsl_keyword "requires"
self#identified_predicate p
method extended fmt (id, name, l,ext) =
Behavior_extensions.pp (self :> extensible_printer_type) fmt (id,name,l,ext)
method extended fmt (ext : acsl_extension) =
Behavior_extensions.pp (self :> extensible_printer_type) fmt ext
method post_cond fmt (k,p) =
let kw = get_termination_kind_name k in
......@@ -2932,7 +2932,7 @@ class cil_printer () = object (self)
let prefix = if is_loop then "loop " else "" in
fprintf fmt "@[<2>%a%s%a@]"
pp_for_behavs behav prefix
(Behavior_extensions.pp (self:>Printer_api.extensible_printer_type)) e
self#extended e
method private logicPrms fmt arg =
let pvar fmt = self#logic_var fmt arg in
......
......@@ -879,7 +879,7 @@ and pp_spec fmt _spec = Format.fprintf fmt "pp_spec_TODO" (*{
mutable spec_disjoint_behaviors: string_list_list;
}*)
and pp_acsl_extension fmt = pp_tuple4 pp_int pp_string pp_location pp_acsl_extension_kind fmt
and pp_acsl_extension fmt = pp_tuple5 pp_int pp_string pp_location pp_bool pp_acsl_extension_kind fmt
and pp_acsl_extension_kind fmt = function
| Ext_id(int) -> Format.fprintf fmt "Ext_id(%a)" pp_int int
......
......@@ -206,8 +206,7 @@ let pp_active fmt active =
~pre:" under active behaviors" ~sep:"," Format.pp_print_string fmt
(Datatype.String.Set.elements active)
let pp_acsl_extension fmt (_,s,_,_) =
Format.fprintf fmt "%s" s
let pp_acsl_extension fmt ((_,s,_,_,_) : acsl_extension) = Format.pp_print_string fmt s
let rec pp_prop kfopt kiopt kloc fmt = function
| IPAxiom (s,_,_,_,_) -> Format.fprintf fmt "Axiom '%s'" s
......@@ -227,9 +226,9 @@ let rec pp_prop kfopt kiopt kloc fmt = function
pp_predicate kind
(pp_idpred kloc) idpred
(pp_kinstr kloc) ki
| IPExtended(le,(_,_,loc,_ as pred)) ->
| IPExtended(le,(_,_,loc,_,_ as ext)) ->
Format.fprintf fmt "%a%a"
pp_acsl_extension pred
pp_acsl_extension ext
(pp_extended_loc kfopt kiopt kloc) (loc,le)
| IPBehavior(_,ki, active, bhv) ->
if Cil.is_default_behavior bhv then
......@@ -481,10 +480,10 @@ let rec ip_order = function
| IPPropertyInstance (kf, s, _, ip) -> [I 18; F kf; K (Kstmt s)] @ ip_order ip
| IPTypeInvariant(a,_,_,_) -> [I 19; S a]
| IPGlobalInvariant(a,_,_) -> [I 20; S a]
| IPExtended(ELContract kf,(_,n,_,_)) -> [I 21;F kf; S n]
| IPExtended(ELStmt (kf, stmt), (_, n, _,_)) ->
| IPExtended(ELContract kf,(_,n,_,_,_)) -> [I 21;F kf; S n]
| IPExtended(ELStmt (kf, stmt), (_,n,_,_,_)) ->
[ I 22; F kf; K (Kstmt stmt); S n]
| IPExtended(ELGlob, (_, n, _,_)) -> [ I 23; S n]
| IPExtended(ELGlob, (_,n,_,_,_)) -> [ I 23; S n]
let pp_compare p q = cmp (ip_order p) (ip_order q)
......
......@@ -2931,14 +2931,14 @@ and childrenBehavior vis b =
b.b_extended <- mapNoCopy (visitCilExtended vis) b.b_extended;
b
and visitCilExtended vis (i,s,l,p as orig) =
and visitCilExtended vis (i,a,l,s,e as orig) =
let visit =
try Hashtbl.find visitor_tbl s
try Hashtbl.find visitor_tbl a
with Not_found -> (fun _ _ -> DoChildren)
in
let p' = doVisitCil vis id (visit vis) childrenCilExtended p in
if is_fresh_behavior vis#behavior then Logic_const.new_acsl_extension s l p
else if p == p' then orig else (i,s,l,p')
let e' = doVisitCil vis id (visit vis) childrenCilExtended e in
if is_fresh_behavior vis#behavior then Logic_const.new_acsl_extension a l s e
else if e == e' then orig else (i,a,l,s,e')
and childrenCilExtended vis p =
match p with
......
......@@ -1932,7 +1932,7 @@ module Global_annotation = struct
if res = 0 then Attributes.compare attr1 attr2 else res
| Dcustom_annot _, _ -> -1
| _, Dcustom_annot _ -> 1
| Dextended ((id1,_,_,_),_,_), Dextended((id2,_,_,_),_,_) ->
| Dextended ((id1,_,_,_,_),_,_), Dextended((id2,_,_,_,_),_,_) ->
Datatype.Int.compare id1 id2
let equal = Datatype.from_compare
......@@ -1952,7 +1952,7 @@ module Global_annotation = struct
| Dtype_annot(l,_) -> 17 * Logic_info.hash l
| Dmodel_annot(l,_) -> 19 * Model_info.hash l
| Dcustom_annot(_,n,_,_) -> 23 * Datatype.String.hash n
| Dextended ((id,_,_,_),_,_) -> 29 * Datatype.Int.hash id
| Dextended ((id,_,_,_,_),_,_) -> 29 * Datatype.Int.hash id
let copy = Datatype.undefined
end)
......
......@@ -733,7 +733,7 @@ let synchronize_source_annot has_new_stmt kf =
match annot.annot_content with
| AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt)
-> true
| AExtended(_,is_loop,(_,name,_,_)) ->
| AExtended(_,is_loop,(_,name,_,_,_)) ->
(match Logic_env.extension_category name with
| Some (Ext_code_annot (Ext_here | Ext_next_loop)) -> false
| Some (Ext_code_annot Ext_next_stmt) -> true
......
......@@ -615,7 +615,7 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor =
in
let my_labels =
match ca.annot_content with
| AExtended (_, is_loop, (_, name, _, _)) ->
| AExtended (_, is_loop, (_, name, _, _, _)) ->
(match Logic_env.extension_category name, is_loop with
| Some (Ext_code_annot (Ext_next_stmt | Ext_next_both)), false ->
Logic_const.post_label :: my_labels
......
......@@ -55,8 +55,8 @@ let refresh_predicate p = { p with ip_id = PredicateId.next () }
let new_identified_term t =
{ it_id = TermId.next (); it_content = t }
let new_acsl_extension name l p =
ExtendedId.next (),name, l, p
let new_acsl_extension name l s k : acsl_extension =
ExtendedId.next (), name, l, s , k
let fresh_term_id = TermId.next
......
......@@ -53,7 +53,7 @@ val new_predicate: predicate -> identified_predicate
@plugin development guide
@since Chlorine-20180501
*)
val new_acsl_extension: string -> location -> acsl_extension_kind -> acsl_extension
val new_acsl_extension: string -> location -> bool -> acsl_extension_kind -> acsl_extension
(** Gives a new id to an existing predicate.
@since Oxygen-20120901
......
......@@ -507,19 +507,20 @@ module Extensions = struct
let typer_tbl = Hashtbl.create 5
let find_typer name = Hashtbl.find typer_tbl name
let is_extension name = Hashtbl.mem typer_tbl name
let register name category typer =
let register name category status typer =
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
Logic_env.register_extension name category;
Hashtbl.add typer_tbl name typer
Hashtbl.add typer_tbl name (status,typer)
end
let typer name ~typing_context:typing_context ~loc p =
try let typ = find_typer name in
typ ~typing_context ~loc p
try
let status,typer = find_typer name in
status, typer ~typing_context ~loc p
with Not_found ->
Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
end
......@@ -3554,7 +3555,8 @@ struct
| p::_ -> p.lexpr_loc
in
if Extensions.is_extension name then
Logic_const.new_acsl_extension name loc (Extensions.typer name ~typing_context ~loc ps)
let status , kind = Extensions.typer name ~typing_context ~loc ps in
Logic_const.new_acsl_extension name loc status kind
else
C.error
loc "No type-checking function registered for extension %s" name
......@@ -4176,8 +4178,8 @@ struct
Dvolatile (tsets, rvi_opt, wvi_opt, [], loc)
| LDextended (kind, content) ->
let typing_context = base_ctxt (Lenv.empty ()) in
let tcontent = Extensions.typer kind ~typing_context ~loc content in
let textended = Logic_const.new_acsl_extension kind loc tcontent in
let status,tcontent = Extensions.typer kind ~typing_context ~loc content in
let textended = Logic_const.new_acsl_extension kind loc status tcontent in
Dextended (textended, [], loc)
let annot a =
......
......@@ -147,9 +147,14 @@ type typing_context = {
on_error: 'a 'b. ('a -> 'b) -> (unit -> unit) -> 'a -> 'b
}
(** [register_behavior_extension name f] registers a typing function [f] to
(** [register_behavior_extension name status f] registers a
typing function [f] to
be used to type function contract clause with name [name].
The boolean flags specifies if the extension can be assigned
a property status or not.
Here is a basic example:
let count = ref 0 in
let foo_typer ~typing_context ~loc ps =
match ps with p::[] ->
......@@ -161,7 +166,7 @@ type typing_context = {
p)])
| [] -> let id = !count in incr count; Ext_id id
| _ -> typing_context.error loc "expecting a predicate after keyword FOO"
let () = register_behavior_extension "FOO" foo_typer
let () = register_behavior_extension "FOO" false foo_typer
@plugin development guide
......@@ -169,7 +174,7 @@ type typing_context = {
@modify Silicon-20161101 change type of the function
*)
val register_behavior_extension:
string ->
string -> bool ->
(typing_context:typing_context -> loc:location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
......@@ -180,7 +185,7 @@ val register_behavior_extension:
@since 18.0-Argon
*)
val register_global_extension:
string ->
string -> bool ->
(typing_context:typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
......@@ -192,7 +197,7 @@ val register_global_extension:
@since 18.0-Argon
*)
val register_code_annot_extension:
string ->
string -> bool ->
(typing_context: typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
......@@ -204,7 +209,7 @@ val register_code_annot_extension:
@since 18.0-Argon
*)
val register_code_annot_next_stmt_extension:
string ->
string -> bool ->
(typing_context: typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
......@@ -215,7 +220,7 @@ val register_code_annot_next_stmt_extension:
@since 18.0-Argon
*)
val register_code_annot_next_loop_extension:
string ->
string -> bool ->
(typing_context: typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
......@@ -227,7 +232,7 @@ val register_code_annot_next_loop_extension:
@since 18.0-Argon
*)
val register_code_annot_next_both_extension:
string ->
string -> bool ->
(typing_context: typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
......
......@@ -1008,8 +1008,9 @@ let is_same_pragma p1 p2 =
| Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
| (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
let is_same_extension (_,e1, _,c1) (_,e2, _,c2) =
let is_same_extension (_,e1,_,s1,c1) (_,e2,_,s2,c2) =
Datatype.String.equal e1 e2 &&
(s1 = s2) &&
match c1, c2 with
| Ext_id i1, Ext_id i2 -> i1 = i2
| Ext_terms t1, Ext_terms t2 ->
......
......@@ -445,7 +445,7 @@ let to_do_on_select
main_ui#pretty_information "This is a requires clause.@.%a@."
pretty_predicate_status ip;
main_ui#view_original (Property.location ip)
| PIP (Property.IPExtended(_,(_,name,_,_)) as ip) ->
| PIP (Property.IPExtended(_,(_,name,_,_,_)) as ip) ->
main_ui#pretty_information "This clause is a %s extension.@.%a@."
name
pretty_predicate_status ip;
......
......@@ -325,7 +325,7 @@ module MYTREE = struct
| Dtype_annot (li, _) -> Some (global_name li.l_var_info.lv_name)
| Dmodel_annot (mf, _) -> Some (global_name mf.mi_name)
| Dcustom_annot _ -> Some "custom clause"
| Dextended ((_,name,_,_),_,_) -> Some ("ACSL extension " ^ name)
| Dextended ((_,name,_,_,_),_,_) -> Some ("ACSL extension " ^ name)
let make_list_globals hide sort_order globs =
(* Association list binding names to globals. *)
......
......@@ -323,7 +323,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
| Dtype_annot (ta, _) -> ta.l_var_info.lv_name
| Dmodel_annot (mi, _) -> mi.mi_name
| Dcustom_annot (_c, _n, _, _) -> " (Custom) "
| Dextended ((_, n, _, _), _, _) -> " (Extension " ^ n ^ ")"
| Dextended ((_, n, _, _, _), _, _) -> " (Extension " ^ n ^ ")"
end
method private images (globs:global list) =
......
......@@ -54,7 +54,7 @@ let retrieve_annot lt =
| _ -> LDefault (* be kind. Someone is bound to write a visitor that will
simplify our term into something unrecognizable... *)
let () = Logic_typing.register_code_annot_next_stmt_extension "slevel"
let () = Logic_typing.register_code_annot_next_stmt_extension "slevel" false
(fun ~typing_context:_ ~loc args ->
let abort () =
Value_parameters.abort ~source:(fst loc) "Invalid slevel directive"
......@@ -115,7 +115,7 @@ let extract_slevel_directive s =
let rec find_one l =
match l with
| [] -> None
| {annot_content = AExtended(_,_,(_,"slevel", _, Ext_terms lp))} :: _ ->
| {annot_content = AExtended(_,_,(_,"slevel", _, _,Ext_terms lp))} :: _ ->
Some (retrieve_annot lp)
| _ :: q -> find_one q
in
......
......@@ -26,7 +26,7 @@ exception Parse_error of string option
let parse_error ?msg () = raise (Parse_error msg)
let () = Logic_typing.register_code_annot_next_loop_extension "unroll"
let () = Logic_typing.register_code_annot_next_loop_extension "unroll" false
begin fun ~typing_context ~loc:_ args ->
match args with
| [arg] ->
......@@ -48,7 +48,7 @@ let get_unroll_terms stmt =
(fun _emitter annot acc ->
match annot with
| {annot_content =
AExtended (_, true, (_, "unroll", _,Ext_terms [term]))} ->
AExtended (_, true, (_, "unroll", _,_,Ext_terms [term]))} ->
term :: acc
| _ -> acc
) stmt []
Markdown is supported
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