CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-16 14:57:13 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'afromher_verif' into afromher_334

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-11-16 22:16:11 +01:00
commit cfba9d456a
8 changed files with 89 additions and 153 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

152
compiler/verification/conditions.ml
View File

@ -23,9 +23,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;
@ -43,31 +42,22 @@ let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) :
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)\]] *)
@ -131,19 +121,12 @@ 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 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 )
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
all functions have been checked never to return empty errors. *)
@ -151,25 +134,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) ->
(* <e1 ... en | ejust :- econs > never returns empty if and only if:
- first we look if e1 .. en ejust can return empty;
@ -181,21 +157,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);
])
@ -204,11 +179,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
@ -216,46 +191,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
| 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 e1
| EAbs (binder, _typs) ->
let _vars, body = Bindlib.unmbind binder in
(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) ->
(* <e1 ... en | ejust :- econs > never returns conflict if and only if:
- neither e1 nor ... nor en nor ejust nor econs return conflict
@ -277,7 +238,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
@ -299,7 +260,6 @@ type verification_condition = {
vc_asserts : typed expr;
vc_scope : ScopeName.t;
vc_variable : typed expr Var.t Marked.pos;
vc_free_vars_typ : (typed expr, typ) Var.Map.t;
}
let trivial_assert e = Marked.same_mark_as (ELit (LBool true)) e
@ -343,9 +303,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)
@ -359,10 +317,6 @@ let rec generate_verification_conditions_scope_body_expr
(* Placeholder until we add all assertions in scope once
* we finished traversing it *)
vc_asserts = trivial_assert e;
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;
};
@ -371,9 +325,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)
@ -383,10 +335,6 @@ let rec generate_verification_conditions_scope_body_expr
vc_guard = Marked.same_mark_as (Marked.unmark vc_empty) e;
vc_kind = NoEmptyError;
vc_asserts = trivial_assert e;
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;
}

4
compiler/verification/conditions.mli
View File

@ -37,10 +37,6 @@ type verification_condition = {
should have type [bool] *)
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 :

5
compiler/verification/io.ml
View File

@ -17,14 +17,13 @@
open Utils
open Shared_ast
open Dcalc.Ast
module type Backend = sig
val init_backend : unit -> unit
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
@ -49,7 +48,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

6
compiler/verification/io.mli
View File

@ -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
@ -50,8 +49,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

2
compiler/verification/solver.ml
View File

@ -29,7 +29,7 @@ let solve_vc
( vc,
try
let ctx =
Z3backend.Io.make_context decl_ctx vc.Conditions.vc_free_vars_typ
Z3backend.Io.make_context decl_ctx
in
let ctx =
Z3backend.Io.encode_asserts ctx vc.Conditions.vc_asserts

2
compiler/verification/z3backend.dummy.ml
View File

@ -27,7 +27,7 @@ module Io = struct
type backend_context = unit
let make_context _ _ = dummy ()
let make_context _ = dummy ()
type vc_encoding = unit

65
compiler/verification/z3backend.real.ml
View File

@ -28,13 +28,10 @@ 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 *)
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 *)
@ -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 **)
@ -72,10 +70,11 @@ 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 **)
let add_z3var (name : string) (v : typed expr Var.t) (ctx : context) : context =
{ ctx with ctx_z3vars = StringMap.add name v ctx.ctx_z3vars }
(** [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 }
(** [add_z3enum] adds the mapping between the Catala enumeration [enum] and the
corresponding Z3 datatype [sort] to the context **)
@ -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_z3var] 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 }
@ -226,11 +225,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
@ -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,24 +385,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
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) :
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
| 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 ctx in
let ctx = add_z3var name v ty ctx in
ctx, fd
| TAny ->
failwith
@ -650,9 +647,9 @@ 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 = 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 =
@ -740,7 +737,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 =
@ -820,9 +818,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"]
@ -832,7 +828,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;

6
flake.lock
View File

@ -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": {