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

Merge branch 'master' into allocations_logement

Browse Source
This commit is contained in:
Denis Merigoux 2022-03-17 17:55:47 +01:00
commit 01bbf1230e
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
3 changed files with 86 additions and 68 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
compiler/driver.ml
View File

@ -238,6 +238,9 @@ let driver source_file (options : Cli.options) : int =
| Cli.Proof ->
let vcs =
Verification.Conditions.generate_verification_conditions prgm
(match options.ex_scope with
| None -> None
| Some _ -> Some scope_uid)
in
Verification.Solver.solve_vc prgm prgm.decl_ctx vcs;
0

143
compiler/verification/conditions.ml
View File

@ -298,77 +298,86 @@ type verification_condition = {
vc_free_vars_typ : typ Pos.marked VarMap.t;
}
let generate_verification_conditions (p : program) : verification_condition list
=
let generate_verification_conditions
(p : program) (s : Dcalc.Ast.ScopeName.t option) :
verification_condition list =
List.fold_left
(fun acc (s_name, _s_var, s_body) ->
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 =
[
let is_selected_scope =
match s with
| Some s when Dcalc.Ast.ScopeName.compare s s_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,
{
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
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_empty) e;
vc_kind = NoEmptyError;
vc_free_vars_typ = vc_empty_typs;
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;
}
:: vc_list
| _ -> vc_list
in
(vc_list @ acc, ctx)
| _ -> (acc, ctx))
(acc, ctx) s_body.scope_body_lets
in
acc)
};
]
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

8
compiler/verification/conditions.mli
View File

@ -38,4 +38,10 @@ type verification_condition = {
}
val generate_verification_conditions :
Dcalc.Ast.program -> verification_condition list
Dcalc.Ast.program ->
Dcalc.Ast.ScopeName.t option ->
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
variables of scope [s]. *)