From 7fb561a9405718cb9b9190f1b9a54cbae42fa7bd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 1 Oct 2024 09:51:33 +0200
Subject: [PATCH] [wp] fix import for boolean and sum types - also fix
compilation of imported fun calls - also fix Why3 path wrt to -wp-library
---
src/plugins/wp/ProverWhy3.ml | 21 +++----
src/plugins/wp/Why3Import.ml | 119 +++++++++++++++++++++--------------
2 files changed, 81 insertions(+), 59 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 31dcea6bd80..97ddd8169bb 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -56,10 +56,11 @@ let get_why3_conf = Conf.memoize
begin fun () ->
let config = Why3Provers.config () in
let main = Why3.Whyconf.get_main config in
- let ld =
- (WpContext.directory () :> string)::
- ((Wp_parameters.Share.get_dir "why3") :> string)::
- (Why3.Whyconf.loadpath main) in
+ let ctx = (WpContext.directory () :> string) in
+ let wp = ((Wp_parameters.Share.get_dir "why3") :> string) in
+ let user = (Wp_parameters.Library.get () :> string list) in
+ let why3 = Why3.Whyconf.loadpath main in
+ let ld = ctx :: wp :: (user @ why3) in
{ env = Why3.Env.create_env ld ; config = main }
end
@@ -506,8 +507,9 @@ let rec of_term ~cnv expected t : Why3.Term.term =
coerce ~cnv sort expected $
t_app' ~cnv ~f:["map"] ~l:"Const" ~p:["const"] [of_term ~cnv vsort v] (of_tau ~cnv sort)
(* Generic *)
- | Fun (FUN({m_source=Wsymbol(f,l,p)}),ls), _, _ ->
- t_app ~cnv ~f ~l ~p $ List.map (of_term' cnv) ls
+ | Fun (FUN({m_source=Wsymbol(f,l,p)}),ls), tau, expected ->
+ coerce ~cnv sort expected $
+ t_app' ~cnv ~f ~l ~p (List.map (of_term' cnv) ls) (of_tau ~cnv tau)
| Fun (f,l), _, _ -> begin
let t_app ls l r =
@@ -520,12 +522,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s))
in
match find s, expected with
- | ls, (Prop | Bool) ->
- coerce ~cnv sort expected $
- t_app ls l (of_tau ~cnv sort)
- | ls, _ ->
- coerce ~cnv sort expected $
- t_app ls l (of_tau ~cnv sort)
+ | ls, _ -> coerce ~cnv sort expected $ t_app ls l (of_tau ~cnv sort)
| exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
in
let apply_from_ns' s l =
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 53983765bda..80a51ee9141 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -84,6 +84,7 @@ type env = {
tenv : C.logic_type_info W.Ty.Hts.t;
lenv : C.logic_info W.Term.Hls.t;
lils : W.Term.lsymbol Logic_info.Hashtbl.t;
+ lcts : W.Term.lsymbol Logic_ctor_info.Hashtbl.t;
ltts : W.Ty.tysymbol Logic_type_info.Hashtbl.t;
menv : why3module Datatype.String.Hashtbl.t;
}
@@ -97,9 +98,10 @@ let create wenv =
let tenv = W.Ty.Hts.create 0 in
let lenv = W.Term.Hls.create 0 in
let lils = Logic_info.Hashtbl.create 0 in
+ let lcts = Logic_ctor_info.Hashtbl.create 0 in
let ltts = Logic_type_info.Hashtbl.create 0 in
let menv = Datatype.String.Hashtbl.create 0 in
- { wenv; tenv; lenv; lils; ltts; menv }
+ { wenv; tenv; lenv; lils; lcts; ltts; menv }
(* -------------------------------------------------------------------------- *)
(* --- Built-in --- *)
@@ -120,7 +122,6 @@ let add_builtins env =
begin
let ts_list = find_ts env ["list"] "List" ["list"] in
let ts_set = find_ts env ["set"] "Set" ["set"] in
- add_builtin env.tenv W.Ty.ts_bool Utf8_logic.boolean [];
add_builtin env.tenv ts_list "\\list" ["A"];
add_builtin env.tenv ts_set "set" ["A"];
end
@@ -161,47 +162,55 @@ let tvars_of_txs (txs: W.Ty.tvsymbol list) : string list * tvars =
x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
) txs ([], W.Ty.Mtv.empty)
-let rec lt_of_ty (env : env) (menv) (tvs : tvars) (ty: W.Ty.ty) : C.logic_type =
+let rec lt_of_ty env menv (tvs : tvars) (ty: W.Ty.ty) : C.logic_type =
match ty.ty_node with
| Tyvar x -> W.Ty.Mtv.find x tvs
| Tyapp(s,[]) when W.Ty.(ts_equal s ts_int) -> C.Linteger
| Tyapp(s,[]) when W.Ty.(ts_equal s ts_real) -> C.Lreal
+ | Tyapp(s,[]) when W.Ty.(ts_equal s ts_bool) -> C.Lboolean
| Tyapp(s,ts) ->
- C.Ltype( lt_of_ts env menv s, List.map (lt_of_ty env menv tvs ) ts)
+ C.Ltype(lt_of_ts env menv s [], List.map (lt_of_ty env menv tvs ) ts)
-and lt_of_ts (env : env) (menv : menv) (ts : W.Ty.tysymbol) : C.logic_type_info =
+and lt_of_ts env menv (ts : W.Ty.tysymbol) (cs: W.Decl.constructor list) : C.logic_type_info =
try W.Ty.Hts.find env.tenv ts with Not_found ->
- let (lt_params,tvars) = tvars_of_txs ts.ts_args in
- let lt_def =
- match ts.ts_def with
- | NoDef | Range _ | Float _ -> None
- | Alias ty -> Some (C.LTsyn (lt_of_ty env menv tvars ty))
- in
- let lti =
- C.{
- lt_name = acsl_name ts.ts_name;
- lt_params ; lt_def ;
- lt_attr = [];
- }
- in W.Ty.Hts.add env.tenv ts lti ;
+ let lt_params,tvars = tvars_of_txs ts.ts_args in
+ let lt_name = acsl_name ts.ts_name in
+ let lti = C.{ lt_name ; lt_params ; lt_def = None ; lt_attr = []; } in
+ lti.lt_def <-
+ (match ts.ts_def with
+ | Range _ | Float _ -> None
+ | NoDef -> Some (C.LTsum (List.map (cli_of_constr env menv lti) cs))
+ | Alias ty -> Some (C.LTsyn (lt_of_ty env menv tvars ty))
+ );
+ W.Ty.Hts.add env.tenv ts lti ;
menv.lti <- (lti, (convert_location ts.ts_name.id_loc) ) :: menv.lti;
Logic_type_info.Hashtbl.add env.ltts lti ts;
lti
+and cli_of_constr env menv ctor_type (ls, _: W.Decl.constructor) : C.logic_ctor_info =
+ let _,tvars =
+ tvars_of_txs @@ W.Ty.Stv.elements @@ W.Term.ls_ty_freevars ls in
+ let l_profile = List.mapi (lv_of_ty env menv tvars ) ls.ls_args in
+ let ctor_params = List.map ( fun (lv:C.logic_var) -> lv.lv_type) l_profile in
+ let ctor_name = acsl_name ls.ls_name in
+ let ctor = Cil_types.{ ctor_name ; ctor_type ; ctor_params } in
+ Logic_ctor_info.Hashtbl.add env.lcts ctor ls ;
+ ctor
+
(* -------------------------------------------------------------------------- *)
(* --- Functions conversion --- *)
(* -------------------------------------------------------------------------- *)
-let lv_of_ty (env:env) (menv : menv) (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
+and lv_of_ty env menv (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
Cil_const.make_logic_var_formal (Printf.sprintf "x%d" index)
@@ (lt_of_ty env menv tvars ty)
-let lt_of_ty_opt (lt_opt) =
+and lt_of_ty_opt (lt_opt) =
match lt_opt with
| None -> C.Ctype (C.TVoid []) (* Same as logic_typing *)
| Some tr -> tr
-let li_of_ls (env:env) (menv : menv) (ls : W.Term.lsymbol) : C.logic_info =
+let li_of_ls env menv (ls : W.Term.lsymbol) : C.logic_info =
let l_tparams,tvars =
tvars_of_txs @@ W.Ty.Stv.elements @@ W.Term.ls_ty_freevars ls in
let l_type = Option.map (lt_of_ty env menv tvars ) ls.ls_value in
@@ -219,32 +228,32 @@ let li_of_ls (env:env) (menv : menv) (ls : W.Term.lsymbol) : C.logic_info =
menv.li <- (li, (convert_location ls.ls_name.id_loc) ):: menv.li;
Logic_info.Hashtbl.add env.lils li ls; li
-let add_ts env menv (ts : W.Ty.tysymbol) =
- L.debug ~dkey "Importing type %a" pp_id ts.ts_name ;
- ignore @@ lt_of_ts env menv ts
+let add_ts env menv (ts : W.Ty.tysymbol) (cs: W.Decl.constructor list)=
+ L.debug ~dkey "Importing type %a: %s" pp_id ts.ts_name (acsl_name ts.ts_name);
+ ignore @@ lt_of_ts env menv ts cs
let add_ls env menv (ls : W.Term.lsymbol) =
- L.debug ~dkey "Importing logic %a" pp_id ls.ls_name ;
+ L.debug ~dkey "Importing logic %a: %s" pp_id ls.ls_name (acsl_name ls.ls_name);
ignore @@ li_of_ls env menv ls
(* -------------------------------------------------------------------------- *)
(* --- Theory --- *)
(* -------------------------------------------------------------------------- *)
-let get_theory (env) (theory_name) (theory_path) =
+let get_theory env (theory_name) (theory_path) =
try W.Env.read_theory env.wenv theory_path theory_name
with W.Env.LibraryNotFound _ ->
L.error "Library %s not found" theory_name; W.Theory.ignore_theory
-let parse_theory (env) (theory:W.Theory.theory) (menv) =
+let parse_theory env (theory:W.Theory.theory) (menv) =
begin
List.iter (fun (tdecl : T.tdecl) ->
match tdecl.td_node with
| Decl decl ->
begin
match decl.d_node with
- | Dtype ts -> add_ts env menv ts
- | Dparam ls ->add_ls env menv ls
- | Ddata ds -> List.iter (fun (ts, _) -> add_ts env menv ts) ds
+ | Dtype ts -> add_ts env menv ts []
+ | Dparam ls -> add_ls env menv ls
+ | Ddata ds -> List.iter (fun (ts, cs) -> add_ts env menv ts cs) ds
| Dlogic ds -> List.iter (fun (ls,_) -> add_ls env menv ls) ds
| Dind (_,ds) -> List.iter (fun (ls,_) -> add_ls env menv ls) ds
| Dprop _ -> ()
@@ -257,6 +266,7 @@ let kind_of_lt (lt : C.logic_type) : LB.kind =
match lt with
| C.Linteger -> LB.Z
| C.Lreal -> LB.R
+ | C.Lboolean -> LB.B
| _ -> LB.A
let sort_of_lt (lt : C.logic_type) : Qed.Logic.sort =
@@ -271,25 +281,40 @@ let sort_of_result = function
let register_builtin env m =
begin
- List.iter (fun (lti, _) ->
- let ty = Logic_type_info.Hashtbl.find env.ltts lti in
- let (package,theory,name) = T.restore_path ty.ts_name in
- LB.add_builtin_type lti.lt_name @@
- Lang.imported_t ~package ~theory ~name
- ) m.types;
- List.iter (fun (li, _) ->
- let ls = Logic_info.Hashtbl.find env.lils li in
- let (package,theory,name) = T.restore_path ls.ls_name in
- let profile = List.map (fun lv -> lv.C.lv_type) li.l_profile in
- let kinds = List.map kind_of_lt profile in
- let params = List.map sort_of_lt profile in
- let result = sort_of_result li.l_type in
- LB.add_builtin li.l_var_info.lv_name kinds @@
- Lang.imported_f ~package ~theory ~name ~params ~result ()
- ) m.logics;
+ let add_builtin (ls: W.Term.lsymbol) acsl_name profile result =
+ let (package, theory, name) = T.restore_path ls.ls_name in
+ let kinds = List.map kind_of_lt profile in
+ let params = List.map sort_of_lt profile in
+ LB.add_builtin acsl_name kinds @@
+ Lang.imported_f ~package ~theory ~name ~params ~result ()
+ in
+ let add_builtin_li li =
+ let ls = Logic_info.Hashtbl.find env.lils li in
+ let profile = List.map (fun lv -> lv.C.lv_type) li.l_profile in
+ let result = sort_of_result li.l_type in
+ add_builtin ls li.l_var_info.lv_name profile result
+ in
+ let add_builtin_ctor ctor =
+ let ls = Logic_ctor_info.Hashtbl.find env.lcts ctor in
+ let profile = ctor.Cil_types.ctor_params in
+ let result = Qed.Logic.Sdata in
+ add_builtin ls ctor.ctor_name profile result
+ in
+ let add_builtin_t lti =
+ let ty = Logic_type_info.Hashtbl.find env.ltts lti in
+ let (package,theory,name) = T.restore_path ty.ts_name in
+ LB.add_builtin_type lti.lt_name @@
+ Lang.imported_t ~package ~theory ~name ;
+ begin match lti.lt_def with
+ | Some C.LTsum ctors -> List.iter add_builtin_ctor ctors
+ | _ -> ()
+ end
+ in
+ List.iter (fun (lti, _) -> add_builtin_t lti) m.types;
+ List.iter (fun (li, _) -> add_builtin_li li) m.logics;
end
-let import_theory (env : env) thname =
+let import_theory env thname =
try
Datatype.String.Hashtbl.find env.menv thname
with Not_found ->
--
GitLab