From f7fd02266e7ebce3c4b2e042ccb993a8fd37017c Mon Sep 17 00:00:00 2001 From: Catala nix updated Date: Mon, 14 Nov 2022 00:24:07 +0000 Subject: [PATCH 1/8] update lock files --- flake.lock | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/flake.lock b/flake.lock index 4f2ce58e..43381179 100644 --- a/flake.lock +++ b/flake.lock @@ -17,11 +17,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1667629849, - "narHash": "sha256-P+v+nDOFWicM4wziFK9S/ajF2lc0N2Rg9p6Y35uMoZI=", + "lastModified": 1668087632, + "narHash": "sha256-T/cUx44aYDuLMFfaiVpMdTjL4kpG7bh0VkN6JEM78/E=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "3bacde6273b09a21a8ccfba15586fb165078fb62", + "rev": "5f588eb4a958f1a526ed8da02d6ea1bea0047b9f", "type": "github" }, "original": { From 43fa3ba550cbabe1d1afd57feb7aab3600b18ee5 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Nov 2022 21:36:21 +0100 Subject: [PATCH 2/8] Start removing ctx_var --- compiler/verification/z3backend.real.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 93609da4..d68a1597 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -650,7 +650,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = match Var.Map.find_opt v ctx.ctx_z3matchsubsts with | None -> (* We are in the standard case, where this is a true Catala variable *) - let t = Var.Map.find v ctx.ctx_var in + let (Typed { ty = t; _ }) = Marked.get_mark vc in let name = unique_name v in let ctx = add_z3var name v ctx in let ctx, ty = translate_typ ctx (Marked.unmark t) in From 5c19bdc0dbc76ac71e81a858e0203cce1c7f5cbb Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Nov 2022 21:52:14 +0100 Subject: [PATCH 3/8] Store typ in z3_vars map --- compiler/verification/z3backend.real.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index d68a1597..c4c875ea 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -34,7 +34,7 @@ type context = { ctx_funcdecl : (typed expr, FuncDecl.func_decl) Var.Map.t; (* A map from Catala function names (represented as variables) to Z3 function declarations, used to only define once functions in Z3 queries *) - ctx_z3vars : typed expr Var.t StringMap.t; + ctx_z3vars : (typed expr Var.t * typ) StringMap.t; (* A map from strings, corresponding to Z3 symbol names, to the Catala variable they represent. Used when to pretty-print Z3 models when a counterexample is generated *) @@ -74,8 +74,8 @@ let add_funcdecl (** [add_z3var] adds the mapping between [name] and the Catala variable [v] to the context **) -let add_z3var (name : string) (v : typed expr Var.t) (ctx : context) : context = - { ctx with ctx_z3vars = StringMap.add name v ctx.ctx_z3vars } +let add_z3var (name : string) (v : typed expr Var.t) (ty: typ) (ctx : context) : context = + { ctx with ctx_z3vars = StringMap.add name (v, ty) ctx.ctx_z3vars } (** [add_z3enum] adds the mapping between the Catala enumeration [enum] and the corresponding Z3 datatype [sort] to the context **) @@ -83,7 +83,7 @@ let add_z3enum (enum : EnumName.t) (sort : Sort.sort) (ctx : context) : context = { ctx with ctx_z3datatypes = EnumMap.add enum sort ctx.ctx_z3datatypes } -(** [add_z3var] adds the mapping between temporary variable [v] and the Z3 +(** [add_z3matchsubst] adds the mapping between temporary variable [v] and the Z3 expression [e] representing an accessor application to the context **) let add_z3matchsubst (v : typed expr Var.t) (e : Expr.expr) (ctx : context) : context = @@ -226,7 +226,7 @@ let print_model (ctx : context) (model : Model.model) : string = let symbol_name = Symbol.to_string (FuncDecl.get_name d) in match StringMap.find_opt symbol_name ctx.ctx_z3vars with | None -> () - | Some v -> + | Some (v, _) -> Format.fprintf fmt "%s %s : %s\n" (Cli.with_style [ANSITerminal.blue] "%s" "-->") (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v)) @@ -241,7 +241,7 @@ let print_model (ctx : context) (model : Model.model) : string = (* Print "name : value\n" *) | Some f -> let symbol_name = Symbol.to_string (FuncDecl.get_name d) in - let v = StringMap.find symbol_name ctx.ctx_z3vars in + let (v, _) = StringMap.find symbol_name ctx.ctx_z3vars in Format.fprintf fmt "%s %s : %s" (Cli.with_style [ANSITerminal.blue] "%s" "-->") (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v)) @@ -403,7 +403,7 @@ let find_or_create_funcdecl (ctx : context) (v : typed expr Var.t) : let name = unique_name v in let fd = FuncDecl.mk_func_decl_s ctx.ctx_z3 name [z3_t1] z3_t2 in let ctx = add_funcdecl v fd ctx in - let ctx = add_z3var name v ctx in + let ctx = add_z3var name v f_ty ctx in ctx, fd | TAny -> failwith @@ -652,7 +652,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = (* We are in the standard case, where this is a true Catala variable *) let (Typed { ty = t; _ }) = Marked.get_mark vc in let name = unique_name v in - let ctx = add_z3var name v ctx in + let ctx = add_z3var name v t ctx in let ctx, ty = translate_typ ctx (Marked.unmark t) in let z3_var = Expr.mk_const_s ctx.ctx_z3 name ty in let ctx = From 1343f9e1f65252249adfe7b5ea1f0cacc437ff87 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Nov 2022 21:55:31 +0100 Subject: [PATCH 4/8] Leverage typed information embedded in expressions to remove uses of the ctx_var map --- compiler/verification/z3backend.real.ml | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index c4c875ea..a67a32da 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -72,8 +72,8 @@ let add_funcdecl (ctx : context) : context = { ctx with ctx_funcdecl = Var.Map.add v fd ctx.ctx_funcdecl } -(** [add_z3var] adds the mapping between [name] and the Catala variable [v] to - the context **) +(** [add_z3var] adds the mapping between [name] and the Catala variable [v] and + its typ [ty] to the context **) let add_z3var (name : string) (v : typed expr Var.t) (ty: typ) (ctx : context) : context = { ctx with ctx_z3vars = StringMap.add name (v, ty) ctx.ctx_z3vars } @@ -226,11 +226,11 @@ let print_model (ctx : context) (model : Model.model) : string = let symbol_name = Symbol.to_string (FuncDecl.get_name d) in match StringMap.find_opt symbol_name ctx.ctx_z3vars with | None -> () - | Some (v, _) -> + | Some (v, ty) -> Format.fprintf fmt "%s %s : %s\n" (Cli.with_style [ANSITerminal.blue] "%s" "-->") (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v)) - (print_z3model_expr ctx (Var.Map.find v ctx.ctx_var) e)) + (print_z3model_expr ctx ty e)) else (* Declaration d is a function *) match Model.get_func_interp model d with @@ -386,24 +386,22 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr = Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 d (** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration - corresponding to the variable [v]. If no such function declaration exists + corresponding to the variable [v] and its type [ty]. If no such function declaration exists yet, we construct it and add it to the context, thus requiring to return a new context *) -let find_or_create_funcdecl (ctx : context) (v : typed expr Var.t) : +let find_or_create_funcdecl (ctx : context) (v : typed expr Var.t) (ty:typ) : context * FuncDecl.func_decl = match Var.Map.find_opt v ctx.ctx_funcdecl with | Some fd -> ctx, fd | None -> ( - (* Retrieves the Catala type of the function [v] *) - let f_ty = Var.Map.find v ctx.ctx_var in - match Marked.unmark f_ty with + match Marked.unmark ty with | TArrow (t1, t2) -> let ctx, z3_t1 = translate_typ ctx (Marked.unmark t1) in let ctx, z3_t2 = translate_typ ctx (Marked.unmark t2) in let name = unique_name v in let fd = FuncDecl.mk_func_decl_s ctx.ctx_z3 name [z3_t1] z3_t2 in let ctx = add_funcdecl v fd ctx in - let ctx = add_z3var name v f_ty ctx in + let ctx = add_z3var name v ty ctx in ctx, fd | TAny -> failwith @@ -740,7 +738,8 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = match Marked.unmark head with | EOp op -> translate_op ctx op args | EVar v -> - let ctx, fd = find_or_create_funcdecl ctx v in + let (Typed { ty = f_ty; _ }) = Marked.get_mark head in + let ctx, fd = find_or_create_funcdecl ctx v f_ty in (* Fold_right to preserve the order of the arguments: The head argument is appended at the head *) let ctx, z3_args = From 0ccf7da89a1e85f84a46d0bdf3f778c5c3de556a Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Nov 2022 21:57:26 +0100 Subject: [PATCH 5/8] Remove ctx_var from Z3 backend context --- compiler/verification/z3backend.real.ml | 36 ++++++++++++------------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index a67a32da..8c7ae04e 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -28,9 +28,6 @@ type context = { ctx_decl : decl_ctx; (* The declaration context from the Catala program, containing information to precisely pretty print Catala expressions *) - ctx_var : (typed expr, typ) Var.Map.t; - (* A map from Catala variables to their types, needed to create Z3 expressions - of the right sort *) ctx_funcdecl : (typed expr, FuncDecl.func_decl) Var.Map.t; (* A map from Catala function names (represented as variables) to Z3 function declarations, used to only define once functions in Z3 queries *) @@ -56,13 +53,14 @@ type context = { is an integer which always is greater than 0 *) } (** The context contains all the required information to encode a VC represented - as a Catala term to Z3. The fields [ctx_decl] and [ctx_var] are computed - before starting the translation to Z3, and are thus unmodified throughout - the translation. The [ctx_z3] context is an OCaml abstraction on top of an - underlying C++ imperative implementation, it is therefore only created once. - Unfortunately, the maps [ctx_funcdecl], [ctx_z3vars], and [ctx_z3datatypes] - are computed dynamically during the translation requiring us to pass the - context around in a functional way **) + as a Catala term to Z3. The field [ctx_decl] is computed before starting the + translation to Z3, and are thus unmodified throughout the translation. The + [ctx_z3] context is an OCaml abstraction on top of an underlying C++ + imperative implementation, it is therefore only created once. Unfortunately, + the maps [ctx_funcdecl], [ctx_z3vars], [ctx_z3datatypes], + [ctx_z3matchsubsts], [ctx_z3structs], and [ctx_z3constraints] are computed + dynamically during the translation requiring us to pass the context around + in a functional way **) (** [add_funcdecl] adds the mapping between the Catala variable [v] and the Z3 function declaration [fd] to the context **) @@ -74,7 +72,8 @@ let add_funcdecl (** [add_z3var] adds the mapping between [name] and the Catala variable [v] and its typ [ty] to the context **) -let add_z3var (name : string) (v : typed expr Var.t) (ty: typ) (ctx : context) : context = +let add_z3var (name : string) (v : typed expr Var.t) (ty : typ) (ctx : context) + : context = { ctx with ctx_z3vars = StringMap.add name (v, ty) ctx.ctx_z3vars } (** [add_z3enum] adds the mapping between the Catala enumeration [enum] and the @@ -83,8 +82,8 @@ let add_z3enum (enum : EnumName.t) (sort : Sort.sort) (ctx : context) : context = { ctx with ctx_z3datatypes = EnumMap.add enum sort ctx.ctx_z3datatypes } -(** [add_z3matchsubst] adds the mapping between temporary variable [v] and the Z3 - expression [e] representing an accessor application to the context **) +(** [add_z3matchsubst] adds the mapping between temporary variable [v] and the + Z3 expression [e] representing an accessor application to the context **) let add_z3matchsubst (v : typed expr Var.t) (e : Expr.expr) (ctx : context) : context = { ctx with ctx_z3matchsubsts = Var.Map.add v e ctx.ctx_z3matchsubsts } @@ -241,7 +240,7 @@ let print_model (ctx : context) (model : Model.model) : string = (* Print "name : value\n" *) | Some f -> let symbol_name = Symbol.to_string (FuncDecl.get_name d) in - let (v, _) = StringMap.find symbol_name ctx.ctx_z3vars in + let v, _ = StringMap.find symbol_name ctx.ctx_z3vars in Format.fprintf fmt "%s %s : %s" (Cli.with_style [ANSITerminal.blue] "%s" "-->") (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v)) @@ -386,10 +385,10 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr = Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 d (** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration - corresponding to the variable [v] and its type [ty]. If no such function declaration exists - yet, we construct it and add it to the context, thus requiring to return a - new context *) -let find_or_create_funcdecl (ctx : context) (v : typed expr Var.t) (ty:typ) : + corresponding to the variable [v] and its type [ty]. If no such function + declaration exists yet, we construct it and add it to the context, thus + requiring to return a new context *) +let find_or_create_funcdecl (ctx : context) (v : typed expr Var.t) (ty : typ) : context * FuncDecl.func_decl = match Var.Map.find_opt v ctx.ctx_funcdecl with | Some fd -> ctx, fd @@ -827,7 +826,6 @@ module Backend = struct { ctx_z3 = z3_ctx; ctx_decl = decl_ctx; - ctx_var = free_vars_typ; ctx_funcdecl = Var.Map.empty; ctx_z3vars = StringMap.empty; ctx_z3datatypes = EnumMap.empty; From 5a5003b22d1afba001062afbf68f963fc20396ce Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Nov 2022 21:59:48 +0100 Subject: [PATCH 6/8] Do not pass free_vars to make_context --- compiler/verification/io.ml | 4 ++-- compiler/verification/io.mli | 6 ++---- compiler/verification/solver.ml | 3 +-- compiler/verification/z3backend.dummy.ml | 2 +- compiler/verification/z3backend.real.ml | 4 +--- 5 files changed, 7 insertions(+), 12 deletions(-) diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml index 3227882d..0d0efd94 100644 --- a/compiler/verification/io.ml +++ b/compiler/verification/io.ml @@ -24,7 +24,7 @@ module type Backend = sig type backend_context - val make_context : decl_ctx -> (typed expr, typ) Var.Map.t -> backend_context + val make_context : decl_ctx -> backend_context type vc_encoding @@ -46,7 +46,7 @@ module type BackendIO = sig type backend_context - val make_context : decl_ctx -> (typed expr, typ) Var.Map.t -> backend_context + val make_context : decl_ctx -> backend_context type vc_encoding diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli index 95c726be..556f0d8e 100644 --- a/compiler/verification/io.mli +++ b/compiler/verification/io.mli @@ -24,8 +24,7 @@ module type Backend = sig type backend_context - val make_context : - decl_ctx -> (typed Dcalc.Ast.expr, typ) Var.Map.t -> backend_context + val make_context : decl_ctx -> backend_context type vc_encoding @@ -47,8 +46,7 @@ module type BackendIO = sig type backend_context - val make_context : - decl_ctx -> (typed Dcalc.Ast.expr, typ) Var.Map.t -> backend_context + val make_context : decl_ctx -> backend_context type vc_encoding diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml index 2c6047ef..fb4b4f0e 100644 --- a/compiler/verification/solver.ml +++ b/compiler/verification/solver.ml @@ -30,8 +30,7 @@ let solve_vc try let ctx, z3_vc = Z3backend.Io.translate_expr - (Z3backend.Io.make_context decl_ctx - vc.Conditions.vc_free_vars_typ) + (Z3backend.Io.make_context decl_ctx) vc.Conditions.vc_guard in Z3backend.Io.Success (z3_vc, ctx) diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml index 90beed67..52f7193b 100644 --- a/compiler/verification/z3backend.dummy.ml +++ b/compiler/verification/z3backend.dummy.ml @@ -27,7 +27,7 @@ module Io = struct type backend_context = unit - let make_context _ _ = dummy () + let make_context _ = dummy () type vc_encoding = unit diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 8c7ae04e..07ad6cab 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -814,9 +814,7 @@ module Backend = struct let init_backend () = Cli.debug_print "Running Z3 version %s" Version.to_string - let make_context - (decl_ctx : decl_ctx) - (free_vars_typ : (typed expr, typ) Var.Map.t) : backend_context = + let make_context (decl_ctx : decl_ctx) : backend_context = let cfg = (if !Cli.disable_counterexamples then [] else ["model", "true"]) @ ["proof", "false"] From fe9ef4f8cb9f69a9525914d3804128fee1829b5a Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Nov 2022 22:08:07 +0100 Subject: [PATCH 7/8] Remove map of free_vars_typ from VC generation --- compiler/verification/conditions.ml | 144 +++++++++------------------ compiler/verification/conditions.mli | 4 - 2 files changed, 46 insertions(+), 102 deletions(-) diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index d6020472..49649baa 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -22,9 +22,8 @@ open Ast (** {1 Helpers and type definitions}*) -type vc_return = typed expr * (typed expr, typ) Var.Map.t -(** The return type of VC generators is the VC expression plus the types of any - locally free variable inside that expression. *) +type vc_return = typed expr +(** The return type of VC generators is the VC expression *) type ctx = { current_scope_name : ScopeName.t; @@ -35,31 +34,22 @@ type ctx = { let conjunction (args : vc_return list) (mark : typed mark) : vc_return = let acc, list = - match args with - | hd :: tl -> hd, tl - | [] -> ((ELit (LBool true), mark), Var.Map.empty), [] + match args with hd :: tl -> hd, tl | [] -> (ELit (LBool true), mark), [] in List.fold_left - (fun (acc, acc_ty) (arg, arg_ty) -> - ( (EApp ((EOp (Binop And), mark), [arg; acc]), mark), - Var.Map.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty - )) + (fun acc arg -> EApp ((EOp (Binop And), mark), [arg; acc]), mark) acc list -let negation ((arg, arg_ty) : vc_return) (mark : typed mark) : vc_return = - (EApp ((EOp (Unop Not), mark), [arg]), mark), arg_ty +let negation (arg : vc_return) (mark : typed mark) : vc_return = + EApp ((EOp (Unop Not), mark), [arg]), mark let disjunction (args : vc_return list) (mark : typed mark) : vc_return = let acc, list = - match args with - | hd :: tl -> hd, tl - | [] -> ((ELit (LBool false), mark), Var.Map.empty), [] + match args with hd :: tl -> hd, tl | [] -> (ELit (LBool false), mark), [] in List.fold_left - (fun ((acc, acc_ty) : vc_return) (arg, arg_ty) -> - ( (EApp ((EOp (Binop Or), mark), [arg; acc]), mark), - Var.Map.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty - )) + (fun (acc : vc_return) arg -> + EApp ((EOp (Binop Or), mark), [arg; acc]), mark) acc list (** [half_product \[a1,...,an\] \[b1,...,bm\] returns \[(a1,b1),...(a1,bn),...(an,b1),...(an,bm)\]] *) @@ -128,14 +118,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : so whatever its input. So we universally quantify over the variable of the function when inspecting the body, resulting in simply traversing through in the code here. *) let vars, body = Bindlib.unmbind binder in - let vc_body_expr, vc_body_ty = - (generate_vc_must_not_return_empty ctx) body - in - ( vc_body_expr, - snd - @@ List.fold_left - (fun (i, acc) ty -> i + 1, Var.Map.add vars.(i) ty acc) - (0, vc_body_ty) typs ) + (generate_vc_must_not_return_empty ctx) body | EApp (f, args) -> (* We assume here that function calls never return empty error, which implies all functions have been checked never to return empty errors. *) @@ -143,25 +126,18 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : (List.map (generate_vc_must_not_return_empty ctx) (f :: args)) (Marked.get_mark e) | EIfThenElse (e1, e2, e3) -> - let e1_vc, vc_typ1 = generate_vc_must_not_return_empty ctx e1 in - let e2_vc, vc_typ2 = generate_vc_must_not_return_empty ctx e2 in - let e3_vc, vc_typ3 = generate_vc_must_not_return_empty ctx e3 in + let e1_vc = generate_vc_must_not_return_empty ctx e1 in + let e2_vc = generate_vc_must_not_return_empty ctx e2 in + let e3_vc = generate_vc_must_not_return_empty ctx e3 in conjunction - [ - e1_vc, vc_typ1; - ( (EIfThenElse (e1, e2_vc, e3_vc), Marked.get_mark e), - Var.Map.union - (fun _ _ _ -> failwith "should not happen") - vc_typ2 vc_typ3 ); - ] + [e1_vc; EIfThenElse (e1, e2_vc, e3_vc), Marked.get_mark e] (Marked.get_mark e) - | ELit LEmptyError -> - Marked.same_mark_as (ELit (LBool false)) e, Var.Map.empty + | ELit LEmptyError -> Marked.same_mark_as (ELit (LBool false)) e | EVar _ (* Per default calculus semantics, you cannot call a function with an argument that evaluates to the empty error. Thus, all variable evaluate to non-empty-error terms. *) | ELit _ | EOp _ -> - Marked.same_mark_as (ELit (LBool true)) e, Var.Map.empty + Marked.same_mark_as (ELit (LBool true)) e | EDefault (exceptions, just, cons) -> (* never returns empty if and only if: - first we look if e1 .. en ejust can return empty; @@ -173,21 +149,20 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : conjunction [ generate_vc_must_not_return_empty ctx just; - (let vc_just_expr, vc_just_ty = + (let vc_just_expr = generate_vc_must_not_return_empty ctx cons in - ( ( EIfThenElse - ( just, - (* Comment from Alain: the justification is not checked for holding an default term. - In such cases, we need to encode the logic of the default terms within - the generation of the verification condition (Z3encoding.translate_expr). - Answer from Denis: Normally, there is a structural invariant from the - surface language to intermediate representation translation preventing - any default terms to appear in justifications.*) - vc_just_expr, - (ELit (LBool false), Marked.get_mark e) ), - Marked.get_mark e ), - vc_just_ty )); + ( EIfThenElse + ( just, + (* Comment from Alain: the justification is not checked for holding an default term. + In such cases, we need to encode the logic of the default terms within + the generation of the verification condition (Z3encoding.translate_expr). + Answer from Denis: Normally, there is a structural invariant from the + surface language to intermediate representation translation preventing + any default terms to appear in justifications.*) + vc_just_expr, + (ELit (LBool false), Marked.get_mark e) ), + Marked.get_mark e )); ] (Marked.get_mark e); ]) @@ -196,11 +171,11 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : out [@@ocamlformat "wrap-comments=false"] -(** [generate_vs_must_not_return_confict e] returns the dcalc boolean expression - [b] such that if [b] is true, then [e] will never return a conflict error. - It also returns a map of all the types of locally free variables inside the - expression. *) -let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed expr) : +(** [generate_vc_must_not_return_conflict e] returns the dcalc boolean + expression [b] such that if [b] is true, then [e] will never return a + conflict error. It also returns a map of all the types of locally free + variables inside the expression. *) +let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) : vc_return = let out = (* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this @@ -208,46 +183,32 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed expr) : match Marked.unmark e with | ETuple (args, _) | EArray args -> conjunction - (List.map (generate_vs_must_not_return_confict ctx) args) + (List.map (generate_vc_must_not_return_conflict ctx) args) (Marked.get_mark e) | EMatch (arg, arms, _) -> conjunction - (List.map (generate_vs_must_not_return_confict ctx) (arg :: arms)) + (List.map (generate_vc_must_not_return_conflict ctx) (arg :: arms)) (Marked.get_mark e) | ETupleAccess (e1, _, _, _) | EInj (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 -> - generate_vs_must_not_return_confict ctx e1 + generate_vc_must_not_return_conflict ctx e1 | EAbs (binder, typs) -> let vars, body = Bindlib.unmbind binder in - let vc_body_expr, vc_body_ty = - (generate_vs_must_not_return_confict ctx) body - in - ( vc_body_expr, - List.fold_left - (fun acc (var, ty) -> Var.Map.add var ty acc) - vc_body_ty - (List.map2 (fun x y -> x, y) (Array.to_list vars) typs) ) + (generate_vc_must_not_return_conflict ctx) body | EApp (f, args) -> conjunction - (List.map (generate_vs_must_not_return_confict ctx) (f :: args)) + (List.map (generate_vc_must_not_return_conflict ctx) (f :: args)) (Marked.get_mark e) | EIfThenElse (e1, e2, e3) -> - let e1_vc, vc_typ1 = generate_vs_must_not_return_confict ctx e1 in - let e2_vc, vc_typ2 = generate_vs_must_not_return_confict ctx e2 in - let e3_vc, vc_typ3 = generate_vs_must_not_return_confict ctx e3 in + let e1_vc = generate_vc_must_not_return_conflict ctx e1 in + let e2_vc = generate_vc_must_not_return_conflict ctx e2 in + let e3_vc = generate_vc_must_not_return_conflict ctx e3 in conjunction - [ - e1_vc, vc_typ1; - ( (EIfThenElse (e1, e2_vc, e3_vc), Marked.get_mark e), - Var.Map.union - (fun _ _ _ -> failwith "should not happen") - vc_typ2 vc_typ3 ); - ] + [e1_vc; EIfThenElse (e1, e2_vc, e3_vc), Marked.get_mark e] (Marked.get_mark e) - | EVar _ | ELit _ | EOp _ -> - Marked.same_mark_as (ELit (LBool true)) e, Var.Map.empty + | EVar _ | ELit _ | EOp _ -> Marked.same_mark_as (ELit (LBool true)) e | EDefault (exceptions, just, cons) -> (* never returns conflict if and only if: - neither e1 nor ... nor en nor ejust nor econs return conflict @@ -269,7 +230,7 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed expr) : in let others = List.map - (generate_vs_must_not_return_confict ctx) + (generate_vc_must_not_return_conflict ctx) (just :: cons :: exceptions) in let out = conjunction (quadratic :: others) (Marked.get_mark e) in @@ -288,7 +249,6 @@ type verification_condition = { vc_kind : verification_condition_kind; vc_scope : ScopeName.t; vc_variable : typed expr Var.t Marked.pos; - vc_free_vars_typ : (typed expr, typ) Var.Map.t; } let rec generate_verification_conditions_scope_body_expr @@ -315,9 +275,7 @@ let rec generate_verification_conditions_scope_body_expr Expr.unbox (Expr.remove_logging_calls scope_let.scope_let_expr) in let e = match_and_ignore_outer_reentrant_default ctx e in - let vc_confl, vc_confl_typs = - generate_vs_must_not_return_confict ctx e - in + let vc_confl = generate_vc_must_not_return_conflict ctx e in let vc_confl = if !Cli.optimize_flag then Bindlib.unbox (Optimizations.optimize_expr ctx.decl vc_confl) @@ -328,10 +286,6 @@ let rec generate_verification_conditions_scope_body_expr { vc_guard = Marked.same_mark_as (Marked.unmark vc_confl) e; vc_kind = NoOverlappingExceptions; - vc_free_vars_typ = - Var.Map.union - (fun _ _ -> failwith "should not happen") - ctx.scope_variables_typs vc_confl_typs; vc_scope = ctx.current_scope_name; vc_variable = scope_let_var, scope_let.scope_let_pos; }; @@ -340,9 +294,7 @@ let rec generate_verification_conditions_scope_body_expr let vc_list = match scope_let.scope_let_kind with | ScopeVarDefinition -> - let vc_empty, vc_empty_typs = - generate_vc_must_not_return_empty ctx e - in + let vc_empty = generate_vc_must_not_return_empty ctx e in let vc_empty = if !Cli.optimize_flag then Bindlib.unbox (Optimizations.optimize_expr ctx.decl vc_empty) @@ -351,10 +303,6 @@ let rec generate_verification_conditions_scope_body_expr { vc_guard = Marked.same_mark_as (Marked.unmark vc_empty) e; vc_kind = NoEmptyError; - vc_free_vars_typ = - Var.Map.union - (fun _ _ -> failwith "should not happen") - ctx.scope_variables_typs vc_empty_typs; vc_scope = ctx.current_scope_name; vc_variable = scope_let_var, scope_let.scope_let_pos; } diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli index cd12bf03..55829300 100644 --- a/compiler/verification/conditions.mli +++ b/compiler/verification/conditions.mli @@ -34,10 +34,6 @@ type verification_condition = { vc_kind : verification_condition_kind; vc_scope : ScopeName.t; vc_variable : typed Dcalc.Ast.expr Var.t Marked.pos; - vc_free_vars_typ : (typed Dcalc.Ast.expr, typ) Var.Map.t; - (** Types of the locally free variables in [vc_guard]. The types of other - free variables linked to scope variables can be obtained with - [Dcalc.Ast.variable_types]. *) } val generate_verification_conditions : From 16c9bae810b65a05ca27da167581d81acec88f98 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Nov 2022 22:13:14 +0100 Subject: [PATCH 8/8] cleanup unused var/module errors --- compiler/verification/conditions.ml | 8 ++++---- compiler/verification/io.ml | 1 - 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index 49649baa..6d76057d 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -113,11 +113,11 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : | EAssert e1 | ErrorOnEmpty e1 -> (generate_vc_must_not_return_empty ctx) e1 - | EAbs (binder, typs) -> + | EAbs (binder, _typs) -> (* Hot take: for a function never to return an empty error when called, it has to do so whatever its input. So we universally quantify over the variable of the function when inspecting the body, resulting in simply traversing through in the code here. *) - let vars, body = Bindlib.unmbind binder in + let _vars, body = Bindlib.unmbind binder in (generate_vc_must_not_return_empty ctx) body | EApp (f, args) -> (* We assume here that function calls never return empty error, which implies @@ -194,8 +194,8 @@ let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) : | EAssert e1 | ErrorOnEmpty e1 -> generate_vc_must_not_return_conflict ctx e1 - | EAbs (binder, typs) -> - let vars, body = Bindlib.unmbind binder in + | EAbs (binder, _typs) -> + let _vars, body = Bindlib.unmbind binder in (generate_vc_must_not_return_conflict ctx) body | EApp (f, args) -> conjunction diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml index 0d0efd94..9d63f485 100644 --- a/compiler/verification/io.ml +++ b/compiler/verification/io.ml @@ -17,7 +17,6 @@ open Utils open Shared_ast -open Dcalc.Ast module type Backend = sig val init_backend : unit -> unit