Generate possible values for variables in scope

compiler/verification/conditions.ml

@@ -31,6 +31,7 @@ type scope_conditions_ctx = {
   scope_cond_input_vars : typed expr Var.t list;
   scope_cond_variables_typs : (typed expr, typ) Var.Map.t;
   scope_cond_asserts : typed expr list;
+  scope_cond_possible_values : (typed expr, typed expr list) Var.Map.t;
 }
 
 let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) :
@@ -313,6 +314,15 @@ let rec slice_expression_for_date_computations
       (fun e acc -> slice_expression_for_date_computations ctx e @ acc)
       e []
 
+(* Expects a top [EDefault] node and below the tree of defaults. *)
+let rec generate_possible_values (ctx : scope_conditions_ctx) (e : typed expr) :
+    typed expr list =
+  match Mark.remove e with
+  | EDefault { excepts; just = _; cons = c } ->
+    generate_possible_values ctx c
+    @ List.flatten (List.map (generate_possible_values ctx) excepts)
+  | _ -> [e]
+
 (** {1 Interface}*)
 
 type verification_condition_kind =
@@ -327,8 +337,6 @@ type verification_condition = {
   vc_variable : typed expr Var.t Mark.pos;
 }
 
-let trivial_assert e = Mark.copy e (ELit (LBool true))
-
 let rec generate_verification_conditions_scope_body_expr
     (ctx : scope_conditions_ctx)
     (scope_body_expr : 'm expr scope_body_expr) :
@@ -372,6 +380,9 @@ let rec generate_verification_conditions_scope_body_expr
         in
         let e = match_and_ignore_outer_reentrant_default ctx e in
         let vc_confl = generate_vc_must_not_return_conflict ctx e in
+        let possible_values : typed expr list =
+          generate_possible_values ctx e
+        in
         let vc_confl =
           if !Cli.optimize_flag then
             Expr.unbox
@@ -433,7 +444,13 @@ let rec generate_verification_conditions_scope_body_expr
                 })
               subexprs_dates
         in
-        ctx, vc_list
+        ( {
+            ctx with
+            scope_cond_possible_values =
+              Var.Map.add scope_let_var possible_values
+                ctx.scope_cond_possible_values;
+          },
+          vc_list )
       | _ -> ctx, []
     in
     let new_ctx, new_vcs =
@@ -478,7 +495,11 @@ let generate_verification_conditions_code_items
             {
               scope_cond_decls = decl_ctx;
               scope_cond_asserts = [];
+              (* To be filled later *)
               scope_cond_input_vars = [];
+              (* To be filled later *)
+              scope_cond_possible_values = Var.Map.empty;
+              (* To be filled later *)
               scope_cond_variables_typs =
                 Var.Map.empty
                 (* We don't need to add the typ of the scope input var here
@@ -498,8 +519,7 @@ let generate_verification_conditions_code_items
             {
               vc_scope_asserts = combined_assert;
               vc_scope_list = scope_vcs;
-              vc_scope_possible_variable_values =
-                Var.Map.empty (* TODO: implement that!*);
+              vc_scope_possible_variable_values = ctx.scope_cond_possible_values;
             }
             vcs
         else vcs)

compiler/verification/io.ml

@@ -165,13 +165,27 @@ module MakeBackendIO (B : Backend) = struct
       "@[<v>This verification condition was generated for @{<yellow>%s@}:@,\
        %a@,\
        with assertions:@,\
+       %a@,\
+       and possible values for variables:@,\
        %a@]"
       (match vc.vc_kind with
       | Conditions.NoEmptyError ->
         "the variable definition never to return an empty error"
       | NoOverlappingExceptions -> "no two exceptions to ever overlap"
       | DateComputation -> "this date computation cannot be ambiguous")
-      (Print.expr ()) vc.vc_guard (Print.expr ()) vc_scope_ctx.vc_scope_asserts;
+      (Print.expr ()) vc.vc_guard (Print.expr ()) vc_scope_ctx.vc_scope_asserts
+      (fun fmt vars_possible_values ->
+        Format.pp_print_list
+          ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+          (fun fmt (var, values) ->
+            Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
+              (Format.pp_print_list
+                 ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
+                 (Print.expr ()))
+              values)
+          fmt
+          (Var.Map.bindings vars_possible_values))
+      vc_scope_ctx.vc_scope_possible_variable_values;
 
     match z3_vc with
     | Success (encoding, backend_ctx) -> (