CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

compiler/verification: force a typed AST as input

Browse Source
This commit is contained in:
Louis Gesbert 2022-07-12 15:57:50 +02:00
parent 4726d00df8
commit 97120c4dc2
6 changed files with 31 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
compiler/verification/conditions.ml
View File

@ -21,7 +21,7 @@ open Ast
(** {1 Helpers and type definitions}*) (** {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 (** The return type of VC generators is the VC expression plus the types of any
locally free variable inside that expression. *) locally free variable inside that expression. *)
@ -32,7 +32,7 @@ type ctx = {
scope_variables_typs : typ Marked.pos VarMap.t; 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 = let acc, list =
match args with match args with
| hd :: tl -> hd, tl | 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 )) VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty ))
acc list 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 (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 = let acc, list =
match args with match args with
| hd :: tl -> hd, tl | hd :: tl -> hd, tl
| [] -> ((ELit (LBool false), mark), VarMap.empty), [] | [] -> ((ELit (LBool false), mark), VarMap.empty), []
in in
List.fold_left 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), ( (EApp ((EOp (Binop Or), mark), [arg; acc]), mark),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty )) VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty ))
acc list 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 variables, or [fun () -> e1] for subscope variables. But what we really want
to analyze is only [e1], so we match this outermost structure explicitely to analyze is only [e1], so we match this outermost structure explicitely
and have a clean verification condition generator that only runs on [e1] *) 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) : let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed marked_expr)
'm marked_expr = : typed marked_expr =
match Marked.unmark e with match Marked.unmark e with
| ErrorOnEmpty | ErrorOnEmpty
( EDefault ( 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 [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 also returns a map of all the types of locally free variables inside the
expression. *) expression. *)
let rec generate_vc_must_not_return_empty (ctx : ctx) (e : 'm marked_expr) : let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed marked_expr) :
'm vc_return = vc_return =
let out = let out =
match Marked.unmark e with match Marked.unmark e with
| ETuple (args, _) | EArray args -> | 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. [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 It also returns a map of all the types of locally free variables inside the
expression. *) expression. *)
let rec generate_vs_must_not_return_confict (ctx : ctx) (e : 'm marked_expr) : let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed marked_expr)
'm vc_return = : vc_return =
let out = let out =
(* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this (* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this
function relies on. *) 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 verification_condition_kind = NoEmptyError | NoOverlappingExceptions
type 'm verification_condition = { type verification_condition = {
vc_guard : 'm marked_expr; vc_guard : typed marked_expr;
(* should have type bool *) (* should have type bool *)
vc_kind : verification_condition_kind; vc_kind : verification_condition_kind;
vc_scope : ScopeName.t; vc_scope : ScopeName.t;
@ -291,7 +291,7 @@ type 'm verification_condition = {
let rec generate_verification_conditions_scope_body_expr let rec generate_verification_conditions_scope_body_expr
(ctx : ctx) (ctx : ctx)
(scope_body_expr : ('m expr, 'm) scope_body_expr) : (scope_body_expr : ('m expr, 'm) scope_body_expr) :
ctx * 'm verification_condition list = ctx * verification_condition list =
match scope_body_expr with match scope_body_expr with
| Result _ -> ctx, [] | Result _ -> ctx, []
| ScopeLet scope_let -> | ScopeLet scope_let ->
@ -374,7 +374,7 @@ let rec generate_verification_conditions_scope_body_expr
let rec generate_verification_conditions_scopes let rec generate_verification_conditions_scopes
(decl_ctx : decl_ctx) (decl_ctx : decl_ctx)
(scopes : ('m expr, 'm) scopes) (scopes : ('m expr, 'm) scopes)
(s : ScopeName.t option) : 'm verification_condition list = (s : ScopeName.t option) : verification_condition list =
match scopes with match scopes with
| Nil -> [] | Nil -> []
| ScopeDef scope_def -> | ScopeDef scope_def ->
@ -414,7 +414,7 @@ let rec generate_verification_conditions_scopes
let generate_verification_conditions let generate_verification_conditions
(p : 'm program) (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 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 (* We sort this list by scope name and then variable name to ensure consistent
output for testing*) output for testing*)

8
compiler/verification/conditions.mli
View File

@ -25,8 +25,8 @@ type verification_condition_kind =
(** This verification condition checks whether a definition never returns (** This verification condition checks whether a definition never returns
a conflict error *) a conflict error *)
type 'm verification_condition = { type verification_condition = {
vc_guard : 'm Dcalc.Ast.marked_expr; vc_guard : Dcalc.Ast.typed Dcalc.Ast.marked_expr;
(** This expression should have type [bool]*) (** This expression should have type [bool]*)
vc_kind : verification_condition_kind; vc_kind : verification_condition_kind;
vc_scope : Dcalc.Ast.ScopeName.t; vc_scope : Dcalc.Ast.ScopeName.t;
@ -38,9 +38,9 @@ type 'm verification_condition = {
} }
val generate_verification_conditions : val generate_verification_conditions :
'm Dcalc.Ast.program -> Dcalc.Ast.typed Dcalc.Ast.program ->
Dcalc.Ast.ScopeName.t option -> Dcalc.Ast.ScopeName.t option ->
'm verification_condition list verification_condition list
(** [generate_verification_conditions p None] will generate the verification (** [generate_verification_conditions p None] will generate the verification
conditions for all the variables of all the scopes of the program [p], while 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 [generate_verification_conditions p (Some s)] will focus only on the

13
compiler/verification/io.ml
View File

@ -58,17 +58,17 @@ module type BackendIO = sig
| Success of vc_encoding * backend_context | Success of vc_encoding * backend_context
| Fail of string | Fail of string
val print_positive_result : 'm Conditions.verification_condition -> string val print_positive_result : Conditions.verification_condition -> string
val print_negative_result : val print_negative_result :
'm Conditions.verification_condition -> Conditions.verification_condition ->
backend_context -> backend_context ->
model option -> model option ->
string string
val encode_and_check_vc : val encode_and_check_vc :
Dcalc.Ast.decl_ctx -> Dcalc.Ast.decl_ctx ->
'm Conditions.verification_condition * vc_encoding_result -> Conditions.verification_condition * vc_encoding_result ->
unit unit
end end
@ -89,8 +89,7 @@ module MakeBackendIO (B : Backend) = struct
| Success of B.vc_encoding * B.backend_context | Success of B.vc_encoding * B.backend_context
| Fail of string | 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 match vc.Conditions.vc_kind with
| Conditions.NoEmptyError -> | Conditions.NoEmptyError ->
Format.asprintf "%s This variable never returns an empty error" 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)))) (Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
let print_negative_result let print_negative_result
(vc : 'm Conditions.verification_condition) (vc : Conditions.verification_condition)
(ctx : B.backend_context) (ctx : B.backend_context)
(model : B.model option) : string = (model : B.model option) : string =
let var_and_pos = let var_and_pos =
@ -152,7 +151,7 @@ module MakeBackendIO (B : Backend) = struct
expression [vc] **) expression [vc] **)
let encode_and_check_vc let encode_and_check_vc
(decl_ctx : decl_ctx) (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 let vc, z3_vc = vc in
Cli.debug_print "For this variable:\n%s\n" Cli.debug_print "For this variable:\n%s\n"

6
compiler/verification/io.mli
View File

@ -63,17 +63,17 @@ module type BackendIO = sig
| Success of vc_encoding * backend_context | Success of vc_encoding * backend_context
| Fail of string | Fail of string
val print_positive_result : 'm Conditions.verification_condition -> string val print_positive_result : Conditions.verification_condition -> string
val print_negative_result : val print_negative_result :
'm Conditions.verification_condition -> Conditions.verification_condition ->
backend_context -> backend_context ->
model option -> model option ->
string string
val encode_and_check_vc : val encode_and_check_vc :
Dcalc.Ast.decl_ctx -> Dcalc.Ast.decl_ctx ->
'm Conditions.verification_condition * vc_encoding_result -> Conditions.verification_condition * vc_encoding_result ->
unit unit
end end

2
compiler/verification/solver.ml
View File

@ -21,7 +21,7 @@ open Dcalc.Ast
discharged by Z3, and attempts to solve them **) discharged by Z3, and attempts to solve them **)
let solve_vc let solve_vc
(decl_ctx : decl_ctx) (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 (* Right now we only use the Z3 backend but the functorial interface should
make it easy to mix and match different proof backends. *) make it easy to mix and match different proof backends. *)
Z3backend.Io.init_backend (); Z3backend.Io.init_backend ();

2
compiler/verification/solver.mli
View File

@ -17,4 +17,4 @@
(** Solves verification conditions using various proof backends *) (** Solves verification conditions using various proof backends *)
val solve_vc : val solve_vc :
Dcalc.Ast.decl_ctx -> 'm Conditions.verification_condition list -> unit Dcalc.Ast.decl_ctx -> Conditions.verification_condition list -> unit