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

Code builds but bugguy [skip ci]

Browse Source
This commit is contained in:
Denis Merigoux 2022-04-04 08:56:48 +02:00
parent f40d2a4b8f
commit 7ca5ef283a
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
5 changed files with 147 additions and 106 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
compiler/driver.ml
View File

@ -249,7 +249,7 @@ let driver source_file (options : Cli.options) : int =
| None -> None
| Some _ -> Some scope_uid)
in
Verification.Solver.solve_vc prgm prgm.decl_ctx vcs;
Verification.Solver.solve_vc prgm.decl_ctx vcs;
0
| Cli.Interpret ->
Cli.debug_print "Starting interpretation...";

27
compiler/scopelang/scope_to_dcalc.ml
View File

@ -888,18 +888,9 @@ let translate_program (prgm : Ast.program) :
in
(* the resulting expression is the list of definitions of all the scopes,
ending with the top-level scope. *)
let (scopes, decl_ctx)
: (Ast.ScopeName.t * Dcalc.Ast.expr Bindlib.var * Dcalc.Ast.scope_body)
list
* _ =
let (scopes, decl_ctx) : Dcalc.Ast.scopes Bindlib.box * _ =
List.fold_right
(fun scope_name
((scopes, decl_ctx) :
(Ast.ScopeName.t
* Dcalc.Ast.expr Bindlib.var
* Dcalc.Ast.scope_body)
list
* _) ->
(fun scope_name (scopes, decl_ctx) ->
let scope = Ast.ScopeMap.find scope_name prgm.program_scopes in
let scope_body, scope_out_struct =
translate_scope_decl struct_ctx enum_ctx sctx scope_name scope
@ -914,7 +905,15 @@ let translate_program (prgm : Ast.program) :
decl_ctx.Dcalc.Ast.ctx_structs scope_out_struct;
}
in
((scope_name, dvar, scope_body) :: scopes, decl_ctx))
scope_ordering ([], decl_ctx)
let scope_next = Bindlib.bind_var dvar scopes in
let new_scopes =
Bindlib.box_apply2
(fun scope_body scope_next ->
Dcalc.Ast.ScopeDef { scope_name; scope_body; scope_next })
scope_body scope_next
in
(new_scopes, decl_ctx))
scope_ordering
(Bindlib.box Dcalc.Ast.Nil, decl_ctx)
in
({ scopes; decl_ctx }, types_ordering)
({ scopes = Bindlib.unbox scopes; decl_ctx }, types_ordering)

207
compiler/verification/conditions.ml
View File

@ -25,7 +25,12 @@ type vc_return = expr Pos.marked * typ Pos.marked VarMap.t
(** The return type of VC generators is the VC expression plus the types of any
locally free variable inside that expression. *)
type ctx = { decl : decl_ctx; input_vars : Var.t list }
type ctx = {
current_scope_name : ScopeName.t;
decl : decl_ctx;
input_vars : Var.t list;
scope_variables_typs : typ Pos.marked VarMap.t;
}
let conjunction (args : vc_return list) (pos : Pos.t) : vc_return =
let acc, list =
@ -298,86 +303,132 @@ type verification_condition = {
vc_free_vars_typ : typ Pos.marked VarMap.t;
}
let generate_verification_conditions
(p : program) (s : Dcalc.Ast.ScopeName.t option) :
let rec generate_verification_conditions_scope_body_expr
(ctx : ctx) (scope_body_expr : scope_body_expr) :
ctx * verification_condition list =
match scope_body_expr with
| Result _ -> (ctx, [])
| ScopeLet scope_let ->
let scope_let_var, scope_let_next =
Bindlib.unbind scope_let.scope_let_next
in
let new_ctx, vc_list =
match scope_let.scope_let_kind with
| DestructuringInputStruct ->
({ ctx with input_vars = scope_let_var :: ctx.input_vars }, [])
| ScopeVarDefinition | SubScopeVarDefinition ->
(* For scope variables, we should check both that they never
evaluate to emptyError nor conflictError. But for subscope
variable definitions, what we're really doing is adding
exceptions to something defined in the subscope so we just ought
to verify only that the exceptions overlap. *)
let e =
match_and_ignore_outer_reentrant_default ctx
scope_let.scope_let_expr
in
let vc_confl, vc_confl_typs =
generate_vs_must_not_return_confict ctx e
in
let vc_confl =
if !Cli.optimize_flag then
Bindlib.unbox (Optimizations.optimize_expr ctx.decl vc_confl)
else vc_confl
in
let vc_list =
[
{
vc_guard = Pos.same_pos_as (Pos.unmark vc_confl) e;
vc_kind = NoOverlappingExceptions;
vc_free_vars_typ =
VarMap.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);
};
]
in
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 =
if !Cli.optimize_flag then
Bindlib.unbox
(Optimizations.optimize_expr ctx.decl vc_empty)
else vc_empty
in
{
vc_guard = Pos.same_pos_as (Pos.unmark vc_empty) e;
vc_kind = NoEmptyError;
vc_free_vars_typ =
VarMap.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);
}
:: vc_list
| _ -> vc_list
in
(ctx, vc_list)
| _ -> (ctx, [])
in
let new_ctx, new_vcs =
generate_verification_conditions_scope_body_expr
{
new_ctx with
scope_variables_typs =
VarMap.add scope_let_var scope_let.scope_let_typ
new_ctx.scope_variables_typs;
}
scope_let_next
in
(new_ctx, vc_list @ new_vcs)
let rec generate_verification_conditions_scopes
(decl_ctx : decl_ctx) (scopes : scopes) (s : ScopeName.t option) :
verification_condition list =
List.fold_left
(fun acc (s_name, _s_var, s_body) ->
match scopes with
| Nil -> []
| ScopeDef scope_def ->
let is_selected_scope =
match s with
| Some s when Dcalc.Ast.ScopeName.compare s s_name = 0 -> true
| Some s when Dcalc.Ast.ScopeName.compare s scope_def.scope_name = 0 ->
true
| None -> true
| _ -> false
in
if is_selected_scope then
let ctx = { decl = p.decl_ctx; input_vars = [] } in
let acc, _ =
List.fold_left
(fun (acc, ctx) s_let ->
match s_let.scope_let_kind with
| DestructuringInputStruct ->
( acc,
{
ctx with
input_vars =
Pos.unmark s_let.scope_let_var :: ctx.input_vars;
} )
| ScopeVarDefinition | SubScopeVarDefinition ->
(* For scope variables, we should check both that they never
evaluate to emptyError nor conflictError. But for subscope
variable definitions, what we're really doing is adding
exceptions to something defined in the subscope so we just
ought to verify only that the exceptions overlap. *)
let e =
match_and_ignore_outer_reentrant_default ctx
(Bindlib.unbox s_let.scope_let_expr)
in
let vc_confl, vc_confl_typs =
generate_vs_must_not_return_confict ctx e
in
let vc_confl =
if !Cli.optimize_flag then
Bindlib.unbox
(Optimizations.optimize_expr p.decl_ctx vc_confl)
else vc_confl
in
let vc_list =
[
{
vc_guard = Pos.same_pos_as (Pos.unmark vc_confl) e;
vc_kind = NoOverlappingExceptions;
vc_free_vars_typ = vc_confl_typs;
vc_scope = s_name;
vc_variable = s_let.scope_let_var;
};
]
in
let vc_list =
match s_let.scope_let_kind with
| ScopeVarDefinition ->
let vc_empty, vc_empty_typs =
generate_vc_must_not_return_empty ctx e
in
let vc_empty =
if !Cli.optimize_flag then
Bindlib.unbox
(Optimizations.optimize_expr p.decl_ctx vc_empty)
else vc_empty
in
{
vc_guard = Pos.same_pos_as (Pos.unmark vc_empty) e;
vc_kind = NoEmptyError;
vc_free_vars_typ = vc_empty_typs;
vc_scope = s_name;
vc_variable = s_let.scope_let_var;
}
:: vc_list
| _ -> vc_list
in
(vc_list @ acc, ctx)
| _ -> (acc, ctx))
(acc, ctx) s_body.scope_body_lets
in
acc
else acc)
[] p.scopes
let vcs =
if is_selected_scope then
let _scope_input_var, scope_body_expr =
Bindlib.unbind scope_def.scope_body.scope_body_expr
in
let ctx =
{
current_scope_name = scope_def.scope_name;
decl = decl_ctx;
input_vars = [];
scope_variables_typs =
VarMap.empty
(* We don't need to add the typ of the scope input var here
because it will never appear in an expression for which we
generate a verification conditions (the big struct is
destructured with a series of let bindings just after. )*);
}
in
let _, vcs =
generate_verification_conditions_scope_body_expr ctx scope_body_expr
in
vcs
else []
in
let _scope_var, next = Bindlib.unbind scope_def.scope_next in
generate_verification_conditions_scopes decl_ctx next s @ vcs
let generate_verification_conditions
(p : program) (s : Dcalc.Ast.ScopeName.t option) :
verification_condition list =
generate_verification_conditions_scopes p.decl_ctx p.scopes s

12
compiler/verification/solver.ml
View File

@ -20,9 +20,8 @@ open Dcalc.Ast
expressions [vcs] corresponding to verification conditions that must be
discharged by Z3, and attempts to solve them **)
let solve_vc
(prgm : program)
(decl_ctx : decl_ctx)
(vcs : Conditions.verification_condition list) : unit =
(decl_ctx : decl_ctx) (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 ();
@ -34,12 +33,7 @@ let solve_vc
let ctx, z3_vc =
Z3backend.Io.translate_expr
(Z3backend.Io.make_context decl_ctx
(VarMap.union
(fun _ _ _ ->
failwith
"[Proof encoding]: A Variable cannot be both free \
and bound")
(variable_types prgm) vc.Conditions.vc_free_vars_typ))
vc.Conditions.vc_free_vars_typ)
(Bindlib.unbox
(Dcalc.Optimizations.remove_all_logs vc.Conditions.vc_guard))
in

5
compiler/verification/solver.mli
View File

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