Support internal_assume with -dmagic_hash for debugging

src/lib/chunk_ast.ml

@@ -976,6 +976,11 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) =
               { repeat_until = true; termination_measure = measure_chunks_opt; cond = cond_chunks; body = body_chunks }
             |> add_chunk chunks
       end
+  | E_internal_assume (nc, exp) ->
+      let nc_chunks = Queue.create () in
+      chunk_atyp comments nc_chunks nc;
+      let exp_chunks = rec_chunk_exp exp in
+      Queue.add (App (Id_aux (Id "internal_assume", l), [nc_chunks; exp_chunks])) chunks
 
 and chunk_vector_update comments (E_aux (aux, l) as exp) =
   let rec_chunk_exp exp =

src/lib/initial_check.ml

@@ -570,6 +570,9 @@ and to_ast_exp ctx (P.E_aux (exp, l) : P.exp) =
         | P.E_internal_return exp ->
             if !opt_magic_hash then E_internal_return (to_ast_exp ctx exp)
             else raise (Reporting.err_general l "Internal return construct found without -dmagic_hash")
+        | P.E_internal_assume (nc, exp) ->
+            if !opt_magic_hash then E_internal_assume (to_ast_constraint ctx nc, to_ast_exp ctx exp)
+            else raise (Reporting.err_general l "Internal assume construct found without -dmagic_hash")
         | P.E_deref exp -> E_app (Id_aux (Id "__deref", l), [to_ast_exp ctx exp])
       in
       E_aux (aux, (l, empty_uannot))

src/lib/lexer.mll

@@ -207,6 +207,7 @@ let kw_table =
      ("backwards",               (fun _ -> Backwards));
      ("internal_plet",           (fun _ -> InternalPLet));
      ("internal_return",         (fun _ -> InternalReturn));
+     ("internal_assume",         (fun _ -> InternalAssume));
    ]
 
 type comment_type = Comment_block | Comment_line

src/lib/parse_ast.ml

@@ -263,6 +263,7 @@ and exp_aux =
   | E_attribute of string * string * exp
   | E_internal_plet of pat * exp * exp
   | E_internal_return of exp
+  | E_internal_assume of atyp * exp
 
 and exp = E_aux of exp_aux * l
 

src/lib/parser.mly

@@ -226,7 +226,7 @@ let warn_extern_effect l =
 %token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant
 %token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure Instantiation Impl
-%token InternalPLet InternalReturn
+%token InternalPLet InternalReturn InternalAssume
 %token Forwards Backwards
 
 %nonassoc Then
@@ -899,6 +899,8 @@ exp:
     { mk_exp (E_internal_plet ($2,$4,$6)) $startpos $endpos }
   | InternalReturn exp
     { mk_exp (E_internal_return($2)) $startpos $endpos }
+  | InternalAssume typ In exp
+    { mk_exp (E_internal_assume($2,$4)) $startpos $endpos }
 
 /* The following implements all nine levels of user-defined precedence for
 operators in expressions, with both left, right and non-associative operators */