Fix a minor issue with the use of const generics

6 files changed, 40 insertions, 13 deletions

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index bbfd31e6..a30ed0f1 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -241,7 +241,11 @@ type eval_ctx = {
   const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t;
       (** The map from const generic vars to their values. Those values
           can be symbolic values or concrete values (in the latter case:
-          if we run in interpreter mode) *)
+          if we run in interpreter mode).
+
+          TODO: this is actually not used in symbolic mode, where we
+          directly introduce fresh symbolic values.
+       *)
   norm_trait_types : ty TraitTypeRefMap.t;
       (** The normalized trait types (a map from trait types to their representatives).
           Note that this doesn't take into account higher-order type constraints
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index be556ade..6a7ac095 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -448,8 +448,8 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
   | SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
     ->
       ()
-  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate
-  | ConstGeneric | TraitConst ->
+  | FunCallRet | SynthInput | Global | KindConstGeneric | LoopOutput | LoopJoin
+  | Aggregate | ConstGeneric | TraitConst ->
       raise (Failure "Unreachable"));
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index eeb6ae1e..af545fb9 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -300,13 +300,29 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                          e ))))
       | CVar vid -> (
           let ctx0 = ctx in
-          (* Lookup the const generic value *)
-          let cv = ctx_lookup_const_generic_value ctx vid in
-          (* Copy the value *)
-          let allow_adt_copy = false in
-          let ctx, v = copy_value allow_adt_copy config ctx cv in
+          (* In concrete mode: lookup the const generic value.
+             In symbolic mode: introduce a fresh symbolic value.
+
+             We have nothing to do: the value is copyable, so we can freely
+             duplicate it.
+          *)
+          let ctx, cv =
+            let cv = ctx_lookup_const_generic_value ctx vid in
+            match config.mode with
+            | ConcreteMode ->
+                (* Copy the value - this is more of a sanity check *)
+                let allow_adt_copy = false in
+                copy_value allow_adt_copy config ctx cv
+            | SymbolicMode ->
+                (* We use the looked up value only for its type *)
+                let v = mk_fresh_symbolic_typed_value KindConstGeneric cv.ty in
+                (ctx, v)
+          in
           (* Continue *)
-          let e = cf v ctx in
+          let e = cf cv ctx in
+          (* If we are synthesizing a symbolic AST, it means that we are in symbolic
+             mode: the value of the const generic is necessarily symbolic. *)
+          assert (e = None || is_symbolic cv.value);
           (* We have to wrap the generated expression *)
           match e with
           | None -> None
@@ -319,7 +335,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                 (SymbolicAst.IntroSymbolic
                    ( ctx0,
                      None,
-                     value_as_symbolic v.value,
+                     value_as_symbolic cv.value,
                      SymbolicAst.VaCgValue vid,
                      e )))
       | CFnPtr _ -> raise (Failure "TODO"))
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 612d6903..d3f8f4fa 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -273,8 +273,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx)
               raise Found
             else ()
         | SynthInput | SynthInputGivenBack | FunCallGivenBack
-        | SynthRetGivenBack | Global | LoopGivenBack | Aggregate | ConstGeneric
-        | TraitConst ->
+        | SynthRetGivenBack | Global | KindConstGeneric | LoopGivenBack
+        | Aggregate | ConstGeneric | TraitConst ->
             ()
     end
   in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index b4611b7e..3b30549c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1086,6 +1086,8 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
   (* Return *)
   (ctx, state_pat)
 
+(** WARNING: do not call this function directly.
+    Call [fresh_named_var_for_symbolic_value] instead. *)
 let fresh_var_llbc_ty (basename : string option) (ty : T.ty) (ctx : bs_ctx) :
     bs_ctx * var =
   (* Generate the fresh variable *)
@@ -2506,9 +2508,13 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
 and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
     (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression)
     (ctx : bs_ctx) : texpression =
+  log#ldebug
+    (lazy
+      ("translate_intro_symbolic:" ^ "\n- value aggregate: "
+     ^ S.show_value_aggregate v));
   let mplace = translate_opt_mplace p in
 
-  (* Introduce a fresh variable for the symbolic value *)
+  (* Introduce a fresh variable for the symbolic value. *)
   let ctx, var = fresh_var_for_symbolic_value sv ctx in
 
   (* Translate the next expression *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index c1ff9804..60cbcc8b 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -42,6 +42,7 @@ type sv_kind =
   | SynthInputGivenBack
       (** The value was given back upon ending one of the input abstractions *)
   | Global  (** The value is a global *)
+  | KindConstGeneric  (** The value is a const generic *)
   | LoopOutput  (** The output of a loop (seen as a forward computation) *)
   | LoopGivenBack
       (** A value given back by a loop (when ending abstractions while going backwards) *)