summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-12-05 16:01:30 +0100
committerSon Ho2023-12-05 16:01:30 +0100
commitdf3587d14b1137d0961f5607b3d8309eddbe69ce (patch)
tree30bae1933291f619d38b992297fa6a9c501112ef
parent60ce69b83cbd749781543bb16becb5357f0e1a0a (diff)
Fix a minor issue with the use of const generics
-rw-r--r--compiler/Contexts.ml6
-rw-r--r--compiler/InterpreterBorrows.ml4
-rw-r--r--compiler/InterpreterExpressions.ml30
-rw-r--r--compiler/InterpreterUtils.ml4
-rw-r--r--compiler/SymbolicToPure.ml8
-rw-r--r--compiler/Values.ml1
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) *)