diff options
Diffstat (limited to 'compiler/InterpreterExpressions.ml')
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 30 |
1 files changed, 23 insertions, 7 deletions
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")) |