From df3587d14b1137d0961f5607b3d8309eddbe69ce Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 5 Dec 2023 16:01:30 +0100 Subject: Fix a minor issue with the use of const generics --- compiler/Contexts.ml | 6 +++++- compiler/InterpreterBorrows.ml | 4 ++-- compiler/InterpreterExpressions.ml | 30 +++++++++++++++++++++++------- compiler/InterpreterUtils.ml | 4 ++-- compiler/SymbolicToPure.ml | 8 +++++++- compiler/Values.ml | 1 + 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) *) -- cgit v1.2.3