Remove logging calls for vc generation

compiler/dcalc/ast.ml

@@ -580,3 +580,43 @@ let rec expr_size (e : expr Pos.marked) : int =
         (fun acc except -> acc + expr_size except)
         (1 + expr_size just + expr_size cons)
         exceptions
+
+let rec remove_logging_calls (e : expr Pos.marked) : expr Pos.marked Bindlib.box
+    =
+  match Pos.unmark e with
+  | EVar (v, _pos) -> evar v (Pos.get_position e)
+  | EApp ((EOp (Unop (Log _)), _), [ arg ]) -> remove_logging_calls arg
+  | EApp (f, args) ->
+      eapp (remove_logging_calls f)
+        (List.map remove_logging_calls args)
+        (Pos.get_position e)
+  | EAbs ((binder, binder_pos), typs) ->
+      eabs
+        (Bindlib.box_mbinder remove_logging_calls binder)
+        binder_pos typs (Pos.get_position e)
+  | ETuple (args, s) ->
+      etuple (List.map remove_logging_calls args) s (Pos.get_position e)
+  | ETupleAccess (e1, n, s_name, typs) ->
+      etupleaccess (remove_logging_calls e1) n s_name typs (Pos.get_position e)
+  | EInj (e1, i, e_name, typs) ->
+      einj (remove_logging_calls e1) i e_name typs (Pos.get_position e)
+  | EMatch (arg, arms, e_name) ->
+      ematch (remove_logging_calls arg)
+        (List.map remove_logging_calls arms)
+        e_name (Pos.get_position e)
+  | EArray args ->
+      earray (List.map remove_logging_calls args) (Pos.get_position e)
+  | ELit l -> elit l (Pos.get_position e)
+  | EAssert e1 -> eassert (remove_logging_calls e1) (Pos.get_position e)
+  | EOp op -> Bindlib.box (EOp op, Pos.get_position e)
+  | EDefault (excepts, just, cons) ->
+      edefault
+        (List.map remove_logging_calls excepts)
+        (remove_logging_calls just)
+        (remove_logging_calls cons)
+        (Pos.get_position e)
+  | EIfThenElse (e1, e2, e3) ->
+      eifthenelse (remove_logging_calls e1) (remove_logging_calls e2)
+        (remove_logging_calls e3) (Pos.get_position e)
+  | ErrorOnEmpty e1 ->
+      eerroronempty (remove_logging_calls e1) (Pos.get_position e)

compiler/dcalc/ast.mli

@@ -336,3 +336,7 @@ val build_whole_program_expr :
 
 val expr_size : expr Pos.marked -> int
 (** Used by the optimizer to know when to stop *)
+
+val remove_logging_calls : expr Pos.marked -> expr Pos.marked Bindlib.box
+(** Removes all calls to [Log] unary operators in the AST, replacing them by
+    their argument. *)

compiler/verification/conditions.ml

@@ -76,34 +76,20 @@ let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list =
 let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Pos.marked) :
     expr Pos.marked =
   match Pos.unmark e with
-  | EApp
-      ( (EOp (Unop (Log _)), _),
-        [
-          ( ErrorOnEmpty
-              ( EDefault
-                  ( [ (EApp ((EVar (x, _), _), [ (ELit LUnit, _) ]), _) ],
-                    (ELit (LBool true), _),
-                    cons ),
-                _ ),
-            _ );
-        ] )
+  | ErrorOnEmpty
+      ( EDefault
+          ( [ (EApp ((EVar (x, _), _), [ (ELit LUnit, _) ]), _) ],
+            (ELit (LBool true), _),
+            cons ),
+        _ )
     when List.exists (fun x' -> Bindlib.eq_vars x x') ctx.input_vars ->
       (* scope variables*)
       cons
-  | EAbs ((binder, _), [ (TLit TUnit, _) ]) -> (
+  | EAbs ((binder, _), [ (TLit TUnit, _) ]) ->
       (* context sub-scope variables *)
       let _, body = Bindlib.unmbind binder in
-      match Pos.unmark body with
-      | EApp ((EOp (Unop (Log _)), _), [ arg ]) -> arg
-      | _ ->
-          Errors.raise_spanned_error (Pos.get_position e)
-            "Internal error: this expression does not have the structure \
-             expected by the VC generator:\n\
-             %a"
-            (Print.format_expr ~debug:true ctx.decl)
-            e)
-  | ErrorOnEmpty (EApp ((EOp (Unop (Log _)), _), [ d ]), _)
-  | EApp ((EOp (Unop (Log _)), _), [ (ErrorOnEmpty d, _) ]) ->
+      body
+  | ErrorOnEmpty d ->
       d (* input subscope variables and non-input scope variable *)
   | _ ->
       Errors.raise_spanned_error (Pos.get_position e)
@@ -323,9 +309,9 @@ let rec generate_verification_conditions_scope_body_expr
                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
+              Bindlib.unbox (remove_logging_calls scope_let.scope_let_expr)
             in
+            let e = match_and_ignore_outer_reentrant_default ctx e in
             let vc_confl, vc_confl_typs =
               generate_vs_must_not_return_confict ctx e
             in