diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index f2adbc17b9bf232bc8f4612baf2c1a092af9ffa4..01bf83ca952940afa1c339d9914766de164ad86a 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -242,16 +242,21 @@ let rec reduce_eqcomp = function
(* --- ACSL Array Equality --- *)
(* -------------------------------------------------------------------------- *)
-module EQARRAYDEF = WpContext.StaticGenerator(Matrix.NATURAL)
+module EQARRAY = WpContext.Generator(Matrix.NATURAL)
(struct
open Matrix
- let name = "Cvalues.EqArrayDef"
+ let name = "Cvalues.EqArray"
type key = matrix
- type data = dfun
+ type data = lfun
let compile (te,ds) =
- let lfun = Lang.generated_f ~sort:Logic.Sprop "EqArray%s_%s"
- (Matrix.id ds) (Matrix.natural_id te)
- in
+ (* Contextual Symbol *)
+ let lfun = Lang.generated_f
+ ~context:true
+ ~sort:Logic.Sprop
+ "EqArray%s_%s" (Matrix.id ds) (Matrix.natural_id te) in
+ (* Simplification of the symbol *)
+ Lang.F.set_builtin lfun reduce_eqcomp ;
+ (* Definition of the symbol *)
let denv = Matrix.denv ds in
let tau = Matrix.tau te ds in
let xa = Lang.freshvar ~basename:"T" tau in
@@ -262,40 +267,30 @@ module EQARRAYDEF = WpContext.StaticGenerator(Matrix.NATURAL)
let tb_xs = List.fold_left e_get tb denv.index_val in
let property = p_hyps (denv.index_range) (!equal_rec te ta_xs tb_xs) in
let definition = p_forall denv.index_var property in
- Lang.F.set_builtin lfun reduce_eqcomp ;
- (* Definition of the symbol *)
- {
+ (* Registration *)
+ Definitions.define_symbol {
+ d_cluster = Definitions.matrix te ;
d_lfun = lfun ; d_types = 0 ;
d_params = denv.size_var @ [xa ; xb ] ;
d_definition = Predicate(Def,definition) ;
- d_cluster = Definitions.dummy () ;
- }
- end)
-
-module EQARRAY = WpContext.Generator(Matrix.NATURAL)
- (struct
- open Matrix
- let name = "Cvalues.EqArrray"
- type key = matrix
- type data = Lang.lfun
- let compile mtx =
- let def = EQARRAYDEF.get mtx in
- let d_cluster = Definitions.matrix (fst mtx) in
- Definitions.define_symbol { def with d_cluster } ;
- def.d_lfun
+ } ; lfun
end)
(* -------------------------------------------------------------------------- *)
(* --- ACSL Compound Equality --- *)
(* -------------------------------------------------------------------------- *)
-module EQCOMPDEF = WpContext.StaticGenerator(Cil_datatype.Compinfo)
+module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
(struct
- let name = "Cvalues.EqCompDef"
+ let name = "Cvalues.EqComp"
type key = compinfo
- type data = dfun
+ type data = lfun
let compile c =
- let lfun = Lang.generated_p ("Eq" ^ Lang.comp_id c) in
+ (* Contextual Symbol *)
+ let lfun = Lang.generated_p ~context:true ("Eq" ^ Lang.comp_id c) in
+ (* Simplification of the symbol *)
+ Lang.F.set_builtin lfun reduce_eqcomp ;
+ (* Definition of the symbol *)
let basename = if c.cstruct then "S" else "U" in
let xa = Lang.freshvar ~basename (Lang.tau_of_comp c) in
let xb = Lang.freshvar ~basename (Lang.tau_of_comp c) in
@@ -308,24 +303,12 @@ module EQCOMPDEF = WpContext.StaticGenerator(Cil_datatype.Compinfo)
(e_getfield ra fd) (e_getfield rb fd))
c.cfields
in
- Lang.F.set_builtin lfun reduce_eqcomp ;
- {
+ (* Registration *)
+ Definitions.define_symbol {
+ d_cluster = Definitions.compinfo c ;
d_lfun = lfun ; d_types = 0 ; d_params = [xa;xb] ;
- d_cluster = Definitions.dummy () ;
d_definition = Predicate(Def,def) ;
- }
- end)
-
-module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
- (struct
- let name = "Cvalues.EqComp"
- type key = compinfo
- type data = Lang.lfun
- let compile ci =
- let def = EQCOMPDEF.get ci in
- let d_cluster = Definitions.compinfo ci in
- Definitions.define_symbol { def with d_cluster } ;
- def.d_lfun
+ } ; lfun
end)
(* -------------------------------------------------------------------------- *)
@@ -336,7 +319,7 @@ let equal_comp c a b = p_call (EQCOMP.get c) [a;b]
let equal_array m a b =
match m with
| _obj , [None] -> p_equal a b
- | m -> p_call (EQARRAY.get m) (Matrix.size m @ [a;b])
+ | m -> p_call (EQARRAY.get m) (Matrix.size m @ [a;b])
let equal_object obj a b =
match obj with
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 30f0dbaf27fde8a3358e4f3825b212b11c76a081..2a40a79b124bb21ed5bd06a79c017168a3adf4eb 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -246,8 +246,7 @@ let matrix = function
| C_array _ -> assert false
| C_comp c -> compinfo c
| C_int _ | C_float _ | C_pointer _ ->
- Cluster.memoize
- (fun id -> newcluster ~id ~title:"Basic Arrays" ()) "Matrix"
+ cluster ~id:"Matrix" ~title:"Basic Arrays" ()
let call_fun ~result lfun cc es =
Symbol.compile (Lang.local cc) lfun ;
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 18adceaf46966168cd356605206f686f12dcd9ac..15b43689ee30218defb0bf0bb5b41477662a202d 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -390,7 +390,7 @@ and model = {
}
and source =
- | Generated of string
+ | Generated of WpContext.context option * string
| Extern of Engine.link extern
let tau_of_lfun phi ts =
@@ -409,8 +409,15 @@ type balance = Nary | Left | Right
let not_found _ = raise Not_found
+let generated ?(context=false) name =
+ let ctxt = if context
+ then Some (WpContext.get_context ())
+ else None in
+ Generated(ctxt,name)
+
let symbolf
?library
+ ?context
?link
?(balance=Nary) (** specify a default for link *)
?(category=Logic.Function)
@@ -425,7 +432,9 @@ let symbolf
Format.pp_print_flush fmt () ;
let name = Buffer.contents buffer in
let source = match library with
- | None -> assert (link = None); Generated name
+ | None ->
+ assert (link = None);
+ generated ?context name
| Some th ->
let conv n = function
| Nary -> Engine.F_call n
@@ -492,16 +501,16 @@ let extern_fp ~library ?(params=[]) ?link phi =
~debug:phi)
}
-let generated_f ?category ?params ?sort ?result name =
- symbolf ?category ?params ?sort ?result name
+let generated_f ?context ?category ?params ?sort ?result name =
+ symbolf ?context ?category ?params ?sort ?result name
-let generated_p name =
+let generated_p ?context name =
Model {
m_category = Logic.Function ;
m_params = [] ;
m_result = Logic.Sprop;
m_typeof = not_found;
- m_source = Generated name
+ m_source = generated ?context name
}
module Fun =
@@ -512,26 +521,38 @@ struct
let debug = function
| ACSL f -> logic_id f
| CTOR c -> ctor_id c
- | Model({m_source=Generated n}) -> n
+ | Model({m_source=Generated(_,n)}) -> n
| Model({m_source=Extern e}) -> e.ext_debug
let hash = function
| ACSL f -> Logic_info.hash f
| CTOR c -> Logic_ctor_info.hash c
- | Model({m_source=Generated n}) -> Datatype.String.hash n
+ | Model({m_source=Generated(_,n)}) -> Datatype.String.hash n
| Model({m_source=Extern e}) -> e.ext_id
+ let compare_context c1 c2 =
+ match c1 , c2 with
+ | None , None -> 0
+ | None , _ -> (-1)
+ | _ , None -> 1
+ | Some c1 , Some c2 -> WpContext.S.compare c1 c2
+
+ let compare_source s1 s2 =
+ match s1 , s2 with
+ | Generated(m1,f1), Generated(m2,f2) ->
+ let cmp = String.compare f1 f2 in
+ if cmp<>0 then cmp else compare_context m1 m2
+ | Extern f , Extern g ->
+ ext_compare f g
+ | Generated _ , Extern _ -> (-1)
+ | Extern _ , Generated _ -> 1
+
let compare f g =
if f==g then 0 else
match f , g with
- | Model({m_source=Generated f}), Model({m_source=Generated g})
- -> String.compare f g
- | Model({m_source=Generated _}), _ -> (-1)
- | _, Model({m_source=Generated _}) -> 1
- | Model({m_source=Extern f}), Model({m_source=Extern g})
- -> ext_compare f g
- | Model({m_source=Extern _}), _ -> (-1)
- | _, Model({m_source=Extern _}) -> 1
+ | Model {m_source=mf} , Model {m_source=mg} -> compare_source mf mg
+ | Model _ , _ -> (-1)
+ | _ , Model _ -> 1
| ACSL f , ACSL g -> Logic_info.compare f g
| ACSL _ , _ -> (-1)
| _ , ACSL _ -> 1
@@ -583,14 +604,14 @@ class virtual idprinting =
method link = function
| ACSL f -> Engine.F_call (self#sanitize_fun (logic_id f))
| CTOR c -> Engine.F_call (self#sanitize_fun (ctor_id c))
- | Model({m_source=Generated n}) -> Engine.F_call (self#sanitize_fun n)
- | Model({m_source=Extern e}) -> self#infoprover e.ext_link
+ | Model({m_source=Generated(_,n)}) -> Engine.F_call (self#sanitize_fun n)
+ | Model({m_source=Extern e}) -> self#infoprover e.ext_link
end
let name_of_lfun = function
| ACSL f -> logic_id f
| CTOR c -> ctor_id c
- | Model({m_source=Generated f}) -> f
+ | Model({m_source=Generated(_,f)}) -> f
| Model({m_source=Extern e}) -> e.ext_debug
let name_of_field = function
@@ -966,6 +987,7 @@ module For_export = struct
let set_builtin f c =
add_init (fun () -> QZERO.set_builtin f c)
+
let set_builtin' f c =
add_init (fun () -> QZERO.set_builtin' f c)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index c7b4f8135f5591362f98085401380b3ef06fdbff..00d5271f9f02db758a6056fc872456830b385bc6 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -87,7 +87,7 @@ and model = {
}
and source =
- | Generated of string
+ | Generated of WpContext.context option * string
| Extern of Engine.link extern
val mem_builtin_type : name:string -> bool
@@ -140,12 +140,11 @@ val extern_p :
val extern_fp : library:library -> ?params:sort list ->
?link:string infoprover -> string -> lfun
-val generated_f : ?category:lfun category ->
+val generated_f : ?context:bool -> ?category:lfun category ->
?params:sort list -> ?sort:sort -> ?result:tau ->
('a,Format.formatter,unit,lfun) format4 -> 'a
-val generated_p : string -> lfun
-
+val generated_p : ?context:bool -> string -> lfun
(** {2 Sorting and Typing} *)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 4cf97ed3c964b8dbf432d0d4aa54ab6933ee2ca6..cbe30c4322b4f0163a74ed4e948e638252ecff31 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -164,7 +164,7 @@ let lfun_name (lfun:Lang.lfun) =
match lfun with
| ACSL f -> Qed.Engine.F_call (Lang.logic_id f)
| CTOR c -> Qed.Engine.F_call (Lang.ctor_id c)
- | Model({m_source=Generated n}) -> Qed.Engine.F_call n
+ | Model({m_source=Generated(_,n)}) -> Qed.Engine.F_call n
| Model({m_source=Extern e}) -> e.Lang.ext_link.Lang.why3
@@ -629,12 +629,12 @@ class visitor (ctx:context) c =
(* --- Files, Theories and Clusters --- *)
method add_builtin_lib =
- self#add_import2 ["bool"] "Bool" ;
- self#add_import2 ["int"] "Int" ;
- self#add_import2 ["int"] "ComputerDivision" ;
- self#add_import2 ["real"] "RealInfix" ;
+ self#add_import_file ["bool"] "Bool" ;
+ self#add_import_file ["int"] "Int" ;
+ self#add_import_file ["int"] "ComputerDivision" ;
+ self#add_import_file ["real"] "RealInfix" ;
self#on_library "qed";
- self#add_import2 ["map"] "Map"
+ self#add_import_file ["map"] "Map"
method on_cluster c =
let name = Definitions.cluster_id c in
@@ -677,15 +677,15 @@ class visitor (ctx:context) c =
| [] -> Wp_parameters.fatal "empty import option"
| l ->
let file, thy = Why3.Lists.chop_last l in
- self#add_import4 file thy (Why3.Opt.get_def thy was) ~import:true
+ self#add_import_use file thy (Why3.Opt.get_def thy was) ~import:true
- method add_import2 file thy =
- self#add_import4 file thy thy ~import:true
+ method add_import_file file thy =
+ self#add_import_use ~import:true file thy thy
- method add_import3 file thy name =
- self#add_import4 file thy name ~import:false
+ method add_import_file_as file thy name =
+ self#add_import_use ~import:false file thy name
- method add_import4 ~import file thy name =
+ method add_import_use ~import file thy name =
Wp_parameters.debug ~dkey:dkey_api
"@[use@ %s@ @[%a.%s@]@ as@ %s@]"
(if import then "import" else "")
@@ -713,14 +713,14 @@ class visitor (ctx:context) c =
| [file] ->
let filenoext = filenoext file in
copy_file file;
- self#add_import2 [filenoext]
+ self#add_import_file [filenoext]
(String.capitalize_ascii filenoext);
| [file;lib] ->
copy_file file;
- self#add_import2 [filenoext file] lib;
+ self#add_import_file [filenoext file] lib;
| [file;lib;name] ->
copy_file file;
- self#add_import3 [filenoext file] lib name;
+ self#add_import_file_as [filenoext file] lib name;
| _ -> Wp_parameters.failure ~current:false
"Driver: why3.file %S not recognized (theory %s)"
opt thy
@@ -841,6 +841,7 @@ class visitor (ctx:context) c =
end
method on_dfun d =
+ Wp_parameters.debug ~dkey:dkey_api "Define %a@." Lang.Fun.pretty d.d_lfun ;
let cnv = empty_cnv ctx in
List.iter (Lang.F.add_var cnv.pool) d.d_params;
begin
@@ -944,6 +945,13 @@ let why3_of_qed ~id ~title ~name ?axioms t =
let goal = Definitions.cluster ~id ~title () in
let ctx = empty_context name in
let v = new visitor ctx goal in
+ Wp_parameters.debug ~dkey:dkey_api "%t"
+ begin fun fmt ->
+ Format.fprintf fmt "---------------------------------------------@\n" ;
+ Format.fprintf fmt "EXPORT GOAL %s@." id ;
+ Format.fprintf fmt "PROP @[<hov 2>%a@]@." Lang.F.pp_pred t ;
+ Format.fprintf fmt "---------------------------------------------@\n" ;
+ end ;
v#add_builtin_lib;
v#vgoal axioms t;
let cnv = empty_cnv ~in_goal:true ~polarity:`Positive ctx in