Add a new type of VC for date computation program slicing

compiler/verification/conditions.ml

@@ -289,9 +289,32 @@ let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) :
          e [])
       (Mark.get e)
 
+(** [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 []
+
 (** {1 Interface}*)
 
-type verification_condition_kind = NoEmptyError | NoOverlappingExceptions
+type verification_condition_kind =
+  | NoEmptyError
+  | NoOverlappingExceptions
+  | DateComputation
 
 type verification_condition = {
   vc_guard : typed expr;
@@ -384,6 +407,30 @@ let rec generate_verification_conditions_scope_body_expr
             :: vc_list
           | _ -> vc_list
         in
+        let vc_list =
+          let subexprs_dates : vc_return list =
+            slice_expression_for_date_computations ctx e
+          in
+          let subexprs_dates =
+            List.map
+              (fun e ->
+                if !Cli.optimize_flag then
+                  Expr.unbox (Shared_ast.Optimizations.optimize_expr ctx.decl e)
+                else e)
+              subexprs_dates
+          in
+          vc_list
+          @ List.map
+              (fun subexpr_date ->
+                {
+                  vc_guard = subexpr_date;
+                  vc_kind = DateComputation;
+                  vc_asserts = trivial_assert e;
+                  vc_scope = ctx.current_scope_name;
+                  vc_variable = scope_let_var, scope_let.scope_let_pos;
+                })
+              subexprs_dates
+        in
         ctx, vc_list, []
       | _ -> ctx, [], []
     in

compiler/verification/conditions.mli

@@ -23,10 +23,13 @@ open Shared_ast
 type verification_condition_kind =
   | NoEmptyError
       (** This verification condition checks whether a definition never returns
-          an empty error *)
+          an empty error. Has type [bool]. *)
   | NoOverlappingExceptions
       (** This verification condition checks whether a definition never returns
-          a conflict error *)
+          a conflict error. Has type [bool]. *)
+  | DateComputation
+      (** This verification condition is just a slice of the program (a
+          subexpression) that features computations on dates. *)
 
 type verification_condition = {
   vc_guard : typed Dcalc.Ast.expr;

compiler/verification/io.ml

@@ -70,7 +70,7 @@ module type BackendIO = sig
     model option ->
     string
 
-  val encode_and_check_vc :
+  val check_vc :
     decl_ctx -> Conditions.verification_condition * vc_encoding_result -> bool
 end
 
@@ -113,6 +113,13 @@ module MakeBackendIO (B : Backend) = struct
           ScopeName.format_t vc.vc_scope
           (Bindlib.name_of (Mark.remove vc.vc_variable))
           Pos.format_loc_text (Mark.get vc.vc_variable)
+      | DateComputation ->
+        Format.asprintf
+          "@[<v>@{<yellow>[%a.%s]@} This date computation might be ambiguous:@,\
+           %a@]"
+          ScopeName.format_t vc.vc_scope
+          (Bindlib.name_of (Mark.remove vc.vc_variable))
+          Pos.format_loc_text (Expr.pos vc.vc_guard)
     in
     let counterexample : string option =
       if !Cli.disable_counterexamples then
@@ -139,7 +146,7 @@ module MakeBackendIO (B : Backend) = struct
     | None -> ""
     | Some counterexample -> "\n" ^ counterexample
 
-  let encode_and_check_vc
+  let check_vc
       (_decl_ctx : decl_ctx)
       (vc : Conditions.verification_condition * vc_encoding_result) : bool =
     let vc, z3_vc = vc in
@@ -154,7 +161,8 @@ module MakeBackendIO (B : Backend) = struct
       (match vc.vc_kind with
       | Conditions.NoEmptyError ->
         "the variable definition never to return an empty error"
-      | NoOverlappingExceptions -> "no two exceptions to ever overlap")
+      | NoOverlappingExceptions -> "no two exceptions to ever overlap"
+      | DateComputation -> "this date computation cannot be ambiguous")
       (Print.expr ()) vc.vc_guard (Print.expr ()) vc.vc_asserts;
 
     match z3_vc with

compiler/verification/io.mli

@@ -71,11 +71,10 @@ module type BackendIO = sig
     model option ->
     string
 
-  val encode_and_check_vc :
+  val check_vc :
     decl_ctx -> Conditions.verification_condition * vc_encoding_result -> bool
-  (** [encode_and_check_vc] spawns a new Z3 solver and tries to solve the
-      expression [vc]. Returns [true] if the vs was proven true and [false]
-      otherwise. **)
+  (** [check_vc] spawns a new Z3 solver and tries to solve the expression [vc].
+      Returns [true] if the vs was proven true and [false] otherwise. **)
 end
 
 module MakeBackendIO : functor (B : Backend) ->

compiler/verification/solver.ml

@@ -22,6 +22,21 @@ open Catala_utils
 let solve_vc
     (decl_ctx : Shared_ast.decl_ctx)
     (vcs : Conditions.verification_condition list) : unit =
+  let dates_vc =
+    List.filter
+      (fun vc ->
+        match vc.Conditions.vc_kind with
+        | Conditions.DateComputation -> true
+        | _ -> false)
+      vcs
+  in
+  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;
   (* 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 ();
@@ -39,13 +54,18 @@ let solve_vc
             in
             Z3backend.Io.Success (z3_vc, ctx)
           with Failure msg -> Fail msg ))
-      vcs
+      (List.filter
+         (fun vc ->
+           match vc.Conditions.vc_kind with
+           | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions ->
+             true
+           | Conditions.DateComputation -> false)
+         vcs)
   in
   let all_proven =
     List.fold_left
       (fun all_proven vc ->
-        if Z3backend.Io.encode_and_check_vc decl_ctx vc then all_proven
-        else false)
+        if Z3backend.Io.check_vc decl_ctx vc then all_proven else false)
       true z3_vcs
   in
   if all_proven then

compiler/verification/z3backend.dummy.ml

@@ -37,5 +37,5 @@ module Io = struct
   type vc_encoding_result = Success of model * model | Fail of string
 
   let print_negative_result _ _ _ = dummy ()
-  let encode_and_check_vc _ _ = dummy ()
+  let check_vc _ _ = dummy ()
 end