Program slicing for ambiguous dates computation

[denismerigoux]

This PR adds a new kind of verification conditions that can be handled by the verification backends : a subexpression that could raise Dates_calc.AmbiguousComputation.

[denismerigoux]

The place where you can tweak which subexpressions are extracted is here :

catala/compiler/verification/conditions.ml

Lines 292 to 310 in 123b9c7

	(** [slice_expression_for_date_computations ctx e] returns a list of
	subexpressions of [e] whose top AST node is a computation on dates that can
	raise [Dates_calc.AmbiguousComputation], that is [Dates_calc.add_dates]. The
	list is ordered from the smallest subexpressions to the biggest. *)
	let rec slice_expression_for_date_computations (ctx : ctx) (e : typed expr) :
	vc_return list =
	match Mark.remove e with
	| EApp
	{
	f =
	EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound; tys = _ }, _;
	args;
	} ->
	List.flatten (List.map (slice_expression_for_date_computations ctx) args)
	@ [e]
	| _ ->
	Expr.shallow_fold
	(fun e acc -> slice_expression_for_date_computations ctx e @ acc)
	e []

The place where you can take all the subexpressions that have been extraced and do something with them (like plug them in Mopsa) is here:

catala/compiler/verification/solver.ml

Lines 33 to 39 in 123b9c7

	List.iter
	(fun dates_vc ->
	Message.emit_result "%s"
	(Z3backend.Io.print_negative_result dates_vc
	(Z3backend.Io.make_context decl_ctx)
	None))
	dates_vc;

The command to test what you're getting is :

dune exec catala --display=quiet -- Proof examples/aides_logement/aides_logement.catala_fr

[denismerigoux]

The information about possible values for each scope variables are here:

catala/compiler/verification/solver.ml

Line 31 in a58e488

(fun scope_name scope_vcs all_proven ->

The type of this thing is

catala/compiler/verification/conditions.mli

Lines 41 to 51 in a58e488

	type verification_conditions_scope = {
	vc_scope_asserts : typed Dcalc.Ast.expr;
	(** A conjunction of all assertions in scope. This expression should have
	type [bool] *)
	vc_scope_possible_variable_values :
	(typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
	(** For each variable, a list containing all the possible values that this
	variable can have. This is a conservative analysis based on the
	traversal of the default tree. *)
	vc_scope_list : verification_condition list;
	}

[rmonat]

@AltGr could you please resolve conflicts in this PR when you have time? If you want to run it, you'll need Mopsa on my private branch, feature/dates. Let me know if you encounter any issue. Thanks a lot!

The command to run the current tests

dune build && dune exec catala -- Proof examples/aides_logement/aides_logement.catala_fr