summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--typing/typedtree.mli6
-rw-r--r--typing/types.mli6
-rw-r--r--verify/escSyn.ml16
-rw-r--r--verify/thmEnv.ml2
-rw-r--r--verify/thmProvers.ml2
-rw-r--r--verify/toErgosrc.ml22
-rw-r--r--verify/verify.ml123
7 files changed, 90 insertions, 87 deletions
diff --git a/typing/typedtree.mli b/typing/typedtree.mli
index 5999ea071e..b314c8eafa 100644
--- a/typing/typedtree.mli
+++ b/typing/typedtree.mli
@@ -120,10 +120,10 @@ and core_contract =
and core_contract_desc =
Tctr_pred of Ident.t * expression * ((pattern * expression) list) option
- | Tctr_arrow of Ident.t option * core_contract * core_contract
- | Tctr_tuple of (Ident.t option * core_contract) list
+ | Tctr_arrow of Ident.t * core_contract * core_contract
+ | Tctr_tuple of (Ident.t * core_contract) list
| Tctr_constr of Path.t * constructor_description
- * (Ident.t option * core_contract) list
+ * (Ident.t * core_contract) list
| Tctr_and of core_contract * core_contract
| Tctr_or of core_contract * core_contract
| Tctr_typconstr of Path.t * core_contract list
diff --git a/typing/types.mli b/typing/types.mli
index b99d00c1f6..584d7d6a4c 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -261,10 +261,10 @@ and core_contract =
and core_contract_desc =
Tctr_pred of Ident.t * expression * ((pattern * expression) list) option
- | Tctr_arrow of Ident.t option * core_contract * core_contract
- | Tctr_tuple of (Ident.t option * core_contract) list
+ | Tctr_arrow of Ident.t * core_contract * core_contract
+ | Tctr_tuple of (Ident.t * core_contract) list
| Tctr_constr of Path.t * constructor_description
- * (Ident.t option * core_contract) list
+ * (Ident.t * core_contract) list
| Tctr_and of core_contract * core_contract
| Tctr_or of core_contract * core_contract
| Tctr_typconstr of Path.t * core_contract list
diff --git a/verify/escSyn.ml b/verify/escSyn.ml
index 27000585c6..407fd15cda 100644
--- a/verify/escSyn.ml
+++ b/verify/escSyn.ml
@@ -1,3 +1,19 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: env.ml 9240 2009-04-28 05:11:54Z garrigue $ *)
+
+(* auxiliary functions on expressions *)
+
open Types
open Typedtree
open Path
diff --git a/verify/thmEnv.ml b/verify/thmEnv.ml
index 84f9747204..2b8303517d 100644
--- a/verify/thmEnv.ml
+++ b/verify/thmEnv.ml
@@ -124,7 +124,7 @@ let increase_depth env = { env with depth = env.depth + 1 }
let add_top_defs env ds = { env with top_defs = env.top_defs@ds }
let add_dep_contracts env x c =
- { env with dep_contracts = Ident.add x c env.dep_contracts }
+ { env with dep_contracts = Ident.add x c env.dep_contracts}
let add_contract_decl env cdecl =
{ env with contract_decls = (env.contract_decls)@[cdecl] }
diff --git a/verify/thmProvers.ml b/verify/thmProvers.ml
index 5c1a1e069d..0976fc5d57 100644
--- a/verify/thmProvers.ml
+++ b/verify/thmProvers.ml
@@ -53,7 +53,7 @@ let askmErgo filename tasks n =
let outchnl = open_out filename in
out_ergotasks outchnl tasks;
close_out outchnl;
- let (cin, cout) as p = open_process (Printf.sprintf "alt-ergo -redondance 4 -stop 2 %s" filename) in
+ let (cin, cout) as p = open_process (Printf.sprintf "alt-ergo -redondance 2 %s" filename) in
let out = channel_contents cin in
let _ = close_process p in
mValid out n
diff --git a/verify/toErgosrc.ml b/verify/toErgosrc.ml
index 7bf58cdbb6..0358fd9a0a 100644
--- a/verify/toErgosrc.ml
+++ b/verify/toErgosrc.ml
@@ -21,7 +21,6 @@ type error =
| Pattern_to_lexpr
exception Error of Location.t * error
-exception Haha
(* make lexpr simper:
(1) remove redundant existential quantifiers,
@@ -1433,29 +1432,22 @@ let mlaxiom_to_smtaxiom type_decls decl =
let rec contract_to_smt type_decls t = match t.contract_desc with
| Tctr_pred (id, p, _) ->
expression_to_eqlexpr type_decls (mklexpr p.exp_loc etrue) p
-| Tctr_arrow(idopt, t1, t2) ->
- begin match idopt with
- | None -> f_implies (contract_to_smt type_decls t1) (contract_to_smt type_decls t2)
- | Some id -> f_forall [Ident.unique_name id]
+| Tctr_arrow(id, t1, t2) ->
+ f_forall [Ident.unique_name id]
(type_to_ppure_type t1.contract_loc t1.contract_type) []
(f_implies (contract_to_smt type_decls t1) (contract_to_smt type_decls t2))
- end
| Tctr_tuple(idopt_t_list) ->
let rec and_them xs = match xs with
| [] -> mklexpr t.contract_loc etrue
- | [(idopt, t)] -> begin match idopt with
- | None -> contract_to_smt type_decls t
- | Some id -> f_forall [Ident.unique_name id]
+ | [(id, t)] ->
+ f_forall [Ident.unique_name id]
(type_to_ppure_type t.contract_loc t.contract_type) []
(contract_to_smt type_decls t)
- end
- | (idopt, t)::l ->
- begin match idopt with
- | None -> contract_to_smt type_decls t
- | Some id -> f_forall [Ident.unique_name id]
+ | (id, t)::l ->
+ f_forall [Ident.unique_name id]
(type_to_ppure_type t.contract_loc t.contract_type) []
(f_and (contract_to_smt type_decls t) (and_them l))
- end in
+ in
and_them idopt_t_list
| _ -> mklexpr t.contract_loc etrue
diff --git a/verify/verify.ml b/verify/verify.ml
index 260167d118..c36402f7d0 100644
--- a/verify/verify.ml
+++ b/verify/verify.ml
@@ -88,7 +88,7 @@ let rec transl_core_contract env cntr e callee caller =
let xe = { e with exp_desc = Texp_ident(Pident new_x, vd) } in
(* let wrapped_p = contract_id_in_expr env p in
let expanded_p = deep_transl_contract env wrapped_p in
- let cond = Texp_ifthenelse (subst [] [(x, new_x)] p, xe, Some callee) in
+ let cond = Texp_ifthenelse (subst [] [(x, new_x)] expanded_p, xe, Some callee) in
*)
let cond = Texp_ifthenelse (subst [] [(x, new_x)] p, xe, Some callee) in
Texp_let (Nonrecursive, [(mkpat (Tpat_var new_x) cty, e)], mkexp cond cty)
@@ -124,18 +124,16 @@ let rec transl_core_contract env cntr e callee caller =
Texp_ifthenelse (mkexp trycond Predef.type_bool, e, Some callee)
end
*)
- | Tctr_arrow (xop, c1, c2) ->
+ | Tctr_arrow (x, c1, c2) ->
(* variant of indy version:
e |>r1,r2<| x:c1 -> c2 =
\v. (e (v |>r2,r1<| c1)) |>r1,r2<| c2[(v |>r2,r1<| c1)/x]
*)
let c1_type = c1.contract_type in
let c2_type = c2.contract_type in
- let res = match xop with
- | Some x ->
let v = Ident.create "v" in
- let xvar = mkexp (mkident v c1_type) c1_type in
- let v_c1 = transl_core_contract env c1 xvar caller callee in
+ let vvar = mkexp (mkident v c1_type) c1_type in
+ let v_c1 = transl_core_contract env c1 vvar caller callee in
let resarg = Texp_apply (e, [(Some v_c1, Required)]) in
(* e.g. x:({a | a > 0} -> {b | true}) -> {c | x 0 > c}
we want to blame the x in {c | x 0 > c} *)
@@ -160,27 +158,17 @@ let rec transl_core_contract env cntr e callee caller =
Some (ThmEnv.contract_name env),
Pident x))}
| _ -> caller in
-
let env2 = add_dep_contracts env v c1 in
- (* let v_c1_indy = transl_core_contract env2 c1 xvar caller callee in
+ (* let v_c1_indy = transl_core_contract env2 c1 vvar caller callee in
let c2subst = subst_contract x v_c1_indy c2 in
let resfun = transl_core_contract env c2subst
(mkexp resarg c2_type) callee caller in
*)
- let c2subst = subst_contract x xvar c2 in
+ let c2subst = subst_contract x vvar c2 in
let resfun = transl_core_contract env2 c2subst
(mkexp resarg c2_type) new_callee new_caller in
Texp_function ([(mkpat (Tpat_var v) c1_type, resfun)], Partial)
- | None ->
- let v = Ident.create "v" in
- let xvar = mkexp (mkident v c1_type) c1_type in
- let c1x = transl_core_contract env c1 xvar caller callee in
- let resarg = Texp_apply (e, [(Some c1x, Required)]) in
- let resfun = transl_core_contract env c2
- (mkexp resarg c2_type) callee caller in
- Texp_function ([(mkpat (Tpat_var v) c1_type, resfun)], Partial)
- in res
| Tctr_tuple cs ->
(* e |>r1,r2<| (x:c1, c2) = match e with
(x1, x2) -> (x1 |>r1,r2<| c1,
@@ -190,20 +178,25 @@ let rec transl_core_contract env cntr e callee caller =
let typs = match (Ctype.repr cty).desc with
| Ttuple ts -> ts
| _ -> print_string "verify: not tuple type"; [] in
- let (ps, es) = List.split (List.map (fun (i, t) ->
- let vd = {val_type = t; val_kind = Val_reg} in
- let exp = { exp_desc = Texp_ident (Pident i, vd);
- exp_loc = e.exp_loc;
- exp_type = t;
- exp_env = e.exp_env
- } in
- (mkpat (Tpat_var i) t, exp))
+ let (ps, es) = List.split (List.map (fun (id, t) ->
+ (mkpat (Tpat_var id) t, id))
(List.combine new_ids typs)) in
- (* similar to dependent function contract, the substitution
- c2[(x1 |>r2,r1<| c1)/x] is done in transmod.ml *)
- let ces = List.map (fun ((vo,c), ei) ->
- transl_core_contract env c ei callee caller)
- (List.combine cs es) in
+ let rec do_dep_contract env1 xs = match xs with
+ | [] -> []
+ | ((x,c),id)::l ->
+ let t = c.contract_type in
+ let vd = {val_type = t; val_kind = Val_reg} in
+ let ei = { exp_desc = Texp_ident (Pident id, vd);
+ exp_loc = e.exp_loc;
+ exp_type = t;
+ exp_env = e.exp_env
+ } in
+ let env2 = add_dep_contracts env1 id c in
+ let l_subst = List.map (fun ((x2,c2),e2) ->
+ ((x2,subst_contract x ei c2),e2)) l in
+ let wrapped_elem = transl_core_contract env1 c ei callee caller in
+ wrapped_elem::(do_dep_contract env2 l_subst) in
+ let ces = do_dep_contract env (List.combine cs es) in
let newpat = { pat_desc = Tpat_tuple ps;
pat_loc = e.exp_loc;
pat_type = cty;
@@ -214,23 +207,26 @@ let rec transl_core_contract env cntr e callee caller =
(* this is constructor contract, which is the general case of tuple contract
e |>r1,r2<| K ci = match e with
| K x1 .. xn -> K (x1 |>r1,r2<| c1, .. ,
- xn |>r1,r2<| cn [(xi |>r1,r2<| ci)/xi] )
+ xn |>r1,r2<| cn [(xi |>r2,r1<| ci)/xi] )
| _ -> r1
*)
- let ids = Ident.create_idents "px" (List.length cs) in
+ let new_ids = Ident.create_idents "px" (List.length cs) in
let xi = List.map (fun (i,t) -> mkpat (Tpat_var i) t)
- (List.combine ids cdesc.cstr_args) in
- let xi_rhs = List.map (fun (i,t) ->
- let vd = {val_type = t; val_kind = Val_reg} in
- mkexp (Texp_ident (Pident i,vd)) t)
- (List.combine ids cdesc.cstr_args) in
- (* similar to dependent function contract, the substitution
- cn [(xi |>r1,r2<| ci)/xi] is done in transmod.ml *)
+ (List.combine new_ids cdesc.cstr_args) in
+ let rec do_dep_contract env1 xs = match xs with
+ | [] -> []
+ | ((x,c),id)::l ->
+ let t = c.contract_type in
+ let vd = {val_type = t; val_kind = Val_reg} in
+ let ei = mkexp (Texp_ident (Pident id,vd)) t in
+ let env2 = add_dep_contracts env1 id c in
+ let l_subst = List.map (fun ((xr,cr),er) ->
+ ((xr,subst_contract x ei cr),er)) l in
+ let wrapped_elem = transl_core_contract env1 c ei callee caller in
+ wrapped_elem::(do_dep_contract env2 l_subst) in
let kxi = (mkpat (Tpat_construct (p1, cdesc, xi)) cdesc.cstr_res,
mkexp (Texp_construct (p1, cdesc,
- List.map (fun ((vo, c), e) ->
- transl_core_contract env c e callee caller)
- (List.combine cs xi_rhs))) cdesc.cstr_res) in
+ do_dep_contract env (List.combine cs new_ids))) cdesc.cstr_res) in
Texp_match (e, [kxi; (mkpat Tpat_any cdesc.cstr_res, callee)], Total)
| Tctr_and (c1, c2) ->
(* e |>r1,r2<| c1 and c2 = (e |>r1,r2<| c1) |>r1,r2<| c2 *)
@@ -240,10 +236,11 @@ let rec transl_core_contract env cntr e callee caller =
| Tctr_or (c1, c2) ->
(* e |>r1,r2<| c1 or c2
= try e |>r1,r2<| c1 with
- Contract_exn1 -> try e |>r1,r2<| c2 with
- Contract_exn2 -> raise Contract_exn2
- | _ -> e
- | _ -> e
+ | Contract_exn1 -> begin try e |>r1,r2<| c2 with
+ | Contract_exn2 -> raise Contract_exn2
+ | _ -> e
+ end
+ | _ -> e
*)
let e1 = transl_core_contract env c1 e callee caller in
let e2 = transl_core_contract env c2 e callee caller in
@@ -273,7 +270,7 @@ let rec transl_core_contract env cntr e callee caller =
ce.exp_desc
in mkexp ce cty
-(* Given x:t1 -> t2, the subst_contract computes t2[(v |><| t1)/x] *)
+(* The subst_contract computes cntr[(e/v] *)
and subst_contract v e cntr =
let mkpat var = { pat_desc = Tpat_var var;
pat_loc = e.exp_loc;
@@ -284,15 +281,14 @@ and subst_contract v e cntr =
(* {x | p} [e/v] is expressed as {x | let v = e in p} *)
let subst_p = Texp_let (Nonrecursive, [(mkpat v, e)], p) in
Tctr_pred (x, { e with exp_desc = subst_p }, exnop)
- | Tctr_arrow (xop, c1, c2) ->
+ | Tctr_arrow (x, c1, c2) ->
let sc1 = subst_contract v e c1 in
let sc2 = subst_contract v e c2 in
- Tctr_arrow (xop, sc1, sc2)
+ Tctr_arrow (x, sc1, sc2)
| Tctr_tuple cs ->
- Tctr_tuple (List.map (fun (vo,c) -> (vo, subst_contract v e c)) cs)
+ Tctr_tuple (List.map (fun (x,c) -> (x, subst_contract v e c)) cs)
| Tctr_constr (i, cdesc, cs) ->
- Tctr_constr (i, cdesc,
- List.map (fun (vo, c) -> (vo, subst_contract v e c)) cs)
+ Tctr_constr (i, cdesc, List.map (fun (x,c) -> (x, subst_contract v e c)) cs)
| Tctr_and (c1, c2) ->
let sc1 = subst_contract v e c1 in
let sc2 = subst_contract v e c2 in
@@ -426,22 +422,21 @@ let rec contract_id_in_contract env c =
| Tctr_tuple cs ->
let rec sub_dep senv xs = begin match xs with
| [] -> []
- | (vo, c)::l ->
- let new_c = contract_id_in_contract env c in
- let senv2 = match vo with
- | None -> senv
- | Some id -> update_name env (Pident id) in
- (vo, new_c) :: sub_dep senv2 l
+ | (x, c)::l ->
+ let new_c = contract_id_in_contract senv c in
+ let senv2 = add_dep_contracts senv x new_c in
+ (x, new_c) :: sub_dep senv2 l
end
in Tctr_tuple (sub_dep env cs)
| Tctr_constr (i, cdesc, cs) ->
- let rec sub_dep xs = begin match xs with
+ let rec sub_dep senv xs = begin match xs with
| [] -> []
- | (vo, c)::l ->
- let new_c = contract_id_in_contract env c
- in (vo, new_c) :: sub_dep l
+ | (x, c)::l ->
+ let new_c = contract_id_in_contract senv c in
+ let senv2 = add_dep_contracts senv x new_c in
+ (x, new_c) :: sub_dep senv2 l
end
- in Tctr_constr (i, cdesc, sub_dep cs)
+ in Tctr_constr (i, cdesc, sub_dep env cs)
| Tctr_and (c1, c2) ->
let new_c1 = contract_id_in_contract env c1 in
let new_c2 = contract_id_in_contract env c2 in
View Lorry Controller Status