From 97120c4dc2f8d7c97ed025b14075ea3d7c819224 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Tue, 12 Jul 2022 15:57:50 +0200 Subject: [PATCH] compiler/verification: force a typed AST as input --- compiler/verification/conditions.ml | 32 ++++++++++++++-------------- compiler/verification/conditions.mli | 8 +++---- compiler/verification/io.ml | 13 ++++++----- compiler/verification/io.mli | 6 +++--- compiler/verification/solver.ml | 2 +- compiler/verification/solver.mli | 2 +- 6 files changed, 31 insertions(+), 32 deletions(-) diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index bb3a6c68..9b2bf338 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -21,7 +21,7 @@ open Ast (** {1 Helpers and type definitions}*) -type 'm vc_return = 'm marked_expr * typ Marked.pos VarMap.t +type vc_return = typed marked_expr * typ Marked.pos VarMap.t (** The return type of VC generators is the VC expression plus the types of any locally free variable inside that expression. *) @@ -32,7 +32,7 @@ type ctx = { scope_variables_typs : typ Marked.pos VarMap.t; } -let conjunction (args : 'm vc_return list) (mark : 'm mark) : 'm vc_return = +let conjunction (args : vc_return list) (mark : typed mark) : vc_return = let acc, list = match args with | hd :: tl -> hd, tl @@ -44,17 +44,17 @@ let conjunction (args : 'm vc_return list) (mark : 'm mark) : 'm vc_return = VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty )) acc list -let negation ((arg, arg_ty) : 'm vc_return) (mark : 'm mark) : 'm vc_return = +let negation ((arg, arg_ty) : vc_return) (mark : typed mark) : vc_return = (EApp ((EOp (Unop Not), mark), [arg]), mark), arg_ty -let disjunction (args : 'm vc_return list) (mark : 'm mark) : 'm vc_return = +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), VarMap.empty), [] in List.fold_left - (fun ((acc, acc_ty) : 'm vc_return) (arg, arg_ty) -> + (fun ((acc, acc_ty) : vc_return) (arg, arg_ty) -> ( (EApp ((EOp (Binop Or), mark), [arg; acc]), mark), VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty )) acc list @@ -71,8 +71,8 @@ let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list = variables, or [fun () -> e1] for subscope variables. But what we really want to analyze is only [e1], so we match this outermost structure explicitely and have a clean verification condition generator that only runs on [e1] *) -let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : 'm marked_expr) : - 'm marked_expr = +let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed marked_expr) + : typed marked_expr = match Marked.unmark e with | ErrorOnEmpty ( EDefault @@ -103,8 +103,8 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : 'm marked_expr) : [b] such that if [b] is true, then [e] will never return an empty error. It also returns a map of all the types of locally free variables inside the expression. *) -let rec generate_vc_must_not_return_empty (ctx : ctx) (e : 'm marked_expr) : - 'm vc_return = +let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed marked_expr) : + vc_return = let out = match Marked.unmark e with | ETuple (args, _) | EArray args -> @@ -197,8 +197,8 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : 'm marked_expr) : [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 : 'm marked_expr) : - 'm vc_return = +let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed marked_expr) + : vc_return = let out = (* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this function relies on. *) @@ -279,8 +279,8 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : 'm marked_expr) : type verification_condition_kind = NoEmptyError | NoOverlappingExceptions -type 'm verification_condition = { - vc_guard : 'm marked_expr; +type verification_condition = { + vc_guard : typed marked_expr; (* should have type bool *) vc_kind : verification_condition_kind; vc_scope : ScopeName.t; @@ -291,7 +291,7 @@ type 'm verification_condition = { let rec generate_verification_conditions_scope_body_expr (ctx : ctx) (scope_body_expr : ('m expr, 'm) scope_body_expr) : - ctx * 'm verification_condition list = + ctx * verification_condition list = match scope_body_expr with | Result _ -> ctx, [] | ScopeLet scope_let -> @@ -374,7 +374,7 @@ let rec generate_verification_conditions_scope_body_expr let rec generate_verification_conditions_scopes (decl_ctx : decl_ctx) (scopes : ('m expr, 'm) scopes) - (s : ScopeName.t option) : 'm verification_condition list = + (s : ScopeName.t option) : verification_condition list = match scopes with | Nil -> [] | ScopeDef scope_def -> @@ -414,7 +414,7 @@ let rec generate_verification_conditions_scopes let generate_verification_conditions (p : 'm program) - (s : Dcalc.Ast.ScopeName.t option) : 'm verification_condition list = + (s : Dcalc.Ast.ScopeName.t option) : verification_condition list = let vcs = generate_verification_conditions_scopes p.decl_ctx p.scopes s in (* We sort this list by scope name and then variable name to ensure consistent output for testing*) diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli index da5d7b6e..cd39ddbe 100644 --- a/compiler/verification/conditions.mli +++ b/compiler/verification/conditions.mli @@ -25,8 +25,8 @@ type verification_condition_kind = (** This verification condition checks whether a definition never returns a conflict error *) -type 'm verification_condition = { - vc_guard : 'm Dcalc.Ast.marked_expr; +type verification_condition = { + vc_guard : Dcalc.Ast.typed Dcalc.Ast.marked_expr; (** This expression should have type [bool]*) vc_kind : verification_condition_kind; vc_scope : Dcalc.Ast.ScopeName.t; @@ -38,9 +38,9 @@ type 'm verification_condition = { } val generate_verification_conditions : - 'm Dcalc.Ast.program -> + Dcalc.Ast.typed Dcalc.Ast.program -> Dcalc.Ast.ScopeName.t option -> - 'm verification_condition list + verification_condition list (** [generate_verification_conditions p None] will generate the verification conditions for all the variables of all the scopes of the program [p], while [generate_verification_conditions p (Some s)] will focus only on the diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml index 514e7476..adeda41c 100644 --- a/compiler/verification/io.ml +++ b/compiler/verification/io.ml @@ -58,17 +58,17 @@ module type BackendIO = sig | Success of vc_encoding * backend_context | Fail of string - val print_positive_result : 'm Conditions.verification_condition -> string + val print_positive_result : Conditions.verification_condition -> string val print_negative_result : - 'm Conditions.verification_condition -> + Conditions.verification_condition -> backend_context -> model option -> string val encode_and_check_vc : Dcalc.Ast.decl_ctx -> - 'm Conditions.verification_condition * vc_encoding_result -> + Conditions.verification_condition * vc_encoding_result -> unit end @@ -89,8 +89,7 @@ module MakeBackendIO (B : Backend) = struct | Success of B.vc_encoding * B.backend_context | Fail of string - let print_positive_result (vc : 'm Conditions.verification_condition) : string - = + let print_positive_result (vc : Conditions.verification_condition) : string = match vc.Conditions.vc_kind with | Conditions.NoEmptyError -> Format.asprintf "%s This variable never returns an empty error" @@ -104,7 +103,7 @@ module MakeBackendIO (B : Backend) = struct (Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable)))) let print_negative_result - (vc : 'm Conditions.verification_condition) + (vc : Conditions.verification_condition) (ctx : B.backend_context) (model : B.model option) : string = let var_and_pos = @@ -152,7 +151,7 @@ module MakeBackendIO (B : Backend) = struct expression [vc] **) let encode_and_check_vc (decl_ctx : decl_ctx) - (vc : 'm Conditions.verification_condition * vc_encoding_result) : unit = + (vc : Conditions.verification_condition * vc_encoding_result) : unit = let vc, z3_vc = vc in Cli.debug_print "For this variable:\n%s\n" diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli index 52d6ac95..7841887a 100644 --- a/compiler/verification/io.mli +++ b/compiler/verification/io.mli @@ -63,17 +63,17 @@ module type BackendIO = sig | Success of vc_encoding * backend_context | Fail of string - val print_positive_result : 'm Conditions.verification_condition -> string + val print_positive_result : Conditions.verification_condition -> string val print_negative_result : - 'm Conditions.verification_condition -> + Conditions.verification_condition -> backend_context -> model option -> string val encode_and_check_vc : Dcalc.Ast.decl_ctx -> - 'm Conditions.verification_condition * vc_encoding_result -> + Conditions.verification_condition * vc_encoding_result -> unit end diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml index 1ee78920..c47bf8d8 100644 --- a/compiler/verification/solver.ml +++ b/compiler/verification/solver.ml @@ -21,7 +21,7 @@ open Dcalc.Ast discharged by Z3, and attempts to solve them **) let solve_vc (decl_ctx : decl_ctx) - (vcs : 'm Conditions.verification_condition list) : unit = + (vcs : Conditions.verification_condition list) : unit = (* Right now we only use the Z3 backend but the functorial interface should make it easy to mix and match different proof backends. *) Z3backend.Io.init_backend (); diff --git a/compiler/verification/solver.mli b/compiler/verification/solver.mli index a8aa7887..8c972cb1 100644 --- a/compiler/verification/solver.mli +++ b/compiler/verification/solver.mli @@ -17,4 +17,4 @@ (** Solves verification conditions using various proof backends *) val solve_vc : - Dcalc.Ast.decl_ctx -> 'm Conditions.verification_condition list -> unit + Dcalc.Ast.decl_ctx -> Conditions.verification_condition list -> unit