diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 7268cf755..1a30696db 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -73,16 +73,22 @@ def make_call_config( smir_info: SMIRInfo, start_symbol: str, mode: CallConfigMode, + cell_maps: dict[str, KInner] | None = None, ) -> CallConfig: fn_data = _FunctionData.load(smir_info=smir_info, start_symbol=start_symbol) match mode: case ConcreteMode(): + if cell_maps is None: + raise ValueError('cell_maps is required for ConcreteMode') config = _make_concrete_call_config( definition=definition, fn_data=fn_data, + cell_maps=cell_maps, ) return CallConfig(config=config, constraints=()) case SymbolicMode(): + if cell_maps is not None: + raise ValueError('cell_maps must not be provided for SymbolicMode') config, constraints = _make_symbolic_call_config( definition=definition, fn_data=fn_data, @@ -90,11 +96,14 @@ def make_call_config( ) return CallConfig(config=config, constraints=tuple(constraints)) case RandomMode(seed): + if cell_maps is None: + raise ValueError('cell_maps is required for RandomMode') config = _make_random_call_config( definition=definition, fn_data=fn_data, types=smir_info.types, seed=seed, + cell_maps=cell_maps, ) return CallConfig(config=config, constraints=()) @@ -140,6 +149,7 @@ def _make_concrete_call_config( *, definition: KDefinition, fn_data: _FunctionData, + cell_maps: dict[str, KInner], ) -> KInner: if fn_data.args: raise ValueError(f'Cannot create concrete call configuration for {fn_data.symbol}: function has parameters') @@ -149,6 +159,7 @@ def _make_concrete_call_config( fn_data=fn_data, localvars=[], seed=None, + cell_maps=cell_maps, ) @@ -158,6 +169,7 @@ def _make_random_call_config( fn_data: _FunctionData, types: Mapping[Ty, TypeMetadata], seed: int, + cell_maps: dict[str, KInner], ) -> KInner: localvars = _random_locals(Random(seed), fn_data.args, types) return _make_concrete_call_config_with_locals( @@ -165,6 +177,7 @@ def _make_random_call_config( fn_data=fn_data, localvars=localvars, seed=seed, + cell_maps=cell_maps, ) @@ -174,6 +187,7 @@ def _make_concrete_call_config_with_locals( fn_data: _FunctionData, localvars: list[KInner], seed: int | None, + cell_maps: dict[str, KInner], ) -> KInner: def init_subst() -> dict[str, KInner]: init_config = definition.init_config(KSort('GeneratedTopCell')) @@ -199,6 +213,7 @@ def init_subst() -> dict[str, KInner]: 'K_CELL': k_cell, 'LOCALS_CELL': list_of(localvars), }, + **cell_maps, } ) @@ -215,11 +230,15 @@ def _make_symbolic_call_config( types: Mapping[Ty, TypeMetadata], ) -> tuple[KInner, list[KInner]]: locals, constraints = _symbolic_locals(fn_data.args, types) + nomap = KApply('MaybeMap::noMap') subst = Subst( { 'K_CELL': fn_data.call_terminator, 'STACK_CELL': list_empty(), # FIXME see #560, problems matching a symbolic stack 'LOCALS_CELL': list_of(locals), + 'FUNCTIONS_CELL': nomap, + 'TYPES_CELL': nomap, + 'MEMORY_CELL': nomap, }, ) empty_config = definition.empty_config(KSort('GeneratedTopCell')) diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index c4434f6c7..3b31bfe57 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -89,10 +89,11 @@ Execution gets stuck (no matching rule) when operands have different types or un ```k // Raw eq: dereference operands, extract types, and delegate to typed comparison rule #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE, _SPAN) - => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS), - #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS)) + => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(TYPESMAP, #withDeref(ARG1), LOCALS), + #withDeref(ARG2), #extractOperandType(TYPESMAP, #withDeref(ARG2), LOCALS)) ... LOCALS + TYPESMAP // Compare values only if types are identical syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)] @@ -112,17 +113,35 @@ Execution gets stuck (no matching rule) when operands have different types or un rule #withDeref(OP) => OP [owise] // Extract type from operands (locals with projections, constants, fallback to unknown) - syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total, no-evaluators] - rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS) - => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) +``` + +```{.k .concrete} + syntax MaybeTy ::= #extractOperandType(MaybeMap, Operand, List) [function, total] + rule #extractOperandType(TYPESMAP, operandCopy(place(local(I), PROJS)), LOCALS) + => getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) + requires 0 <=Int I andBool I getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) requires 0 <=Int I andBool I getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) +``` + +```{.k .symbolic} + syntax MaybeTy ::= #extractOperandType(MaybeMap, Operand, List) [function, total, no-evaluators] + rule #extractOperandType(_, operandCopy(place(local(I), PROJS)), LOCALS) + => getTyOf(noMap, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) requires 0 <=Int I andBool I TY - rule #extractOperandType(_, _) => TyUnknown [owise] + rule #extractOperandType(_, operandMove(place(local(I), PROJS)), LOCALS) + => getTyOf(noMap, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) + requires 0 <=Int I andBool I TY + rule #extractOperandType(_, _, _) => TyUnknown [owise] ``` #### Volatile Store (`std::intrinsics::volatile_store`, `std::ptr::write_volatile`) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index c14ef496c..2f59d2d2a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -105,8 +105,9 @@ will effectively be no-ops at this level). ... LOCALS + TYPESMAP requires 0 <=Int I andBool I #execStmt(statement(statementKindAssign(place(local(I), _PROJ) #as PLACE, RVAL), _SPAN)) @@ -115,8 +116,9 @@ will effectively be no-ops at this level). ... LOCALS + TYPESMAP requires 0 <=Int I andBool I _ => CALLER // - _ => #getBlocks(CALLER) + _ => #getBlocks(FUNCSMAP, CALLER) CALLER => NEWCALLER DEST => NEWDEST someBasicBlockIdx(TARGET) => NEWTARGET @@ -234,6 +236,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f // // remaining call stack (without top frame) ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK + FUNCSMAP // no value to return, skip writing rule [termReturnNone]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ @@ -242,7 +245,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f _ => CALLER // - _ => #getBlocks(CALLER) + _ => #getBlocks(FUNCSMAP, CALLER) CALLER => NEWCALLER _ => NEWDEST someBasicBlockIdx(TARGET) => NEWTARGET @@ -251,11 +254,22 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f // // remaining call stack (without top frame) ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK + FUNCSMAP - syntax List ::= #getBlocks( Ty ) [function, total, no-evaluators] - | #getBlocksAux( MonoItemKind ) [function, total] +``` + +```{.k .concrete} + syntax List ::= #getBlocks( MaybeMap, Ty ) [function, total] + rule #getBlocks(FUNCSMAP, TY) => #getBlocksAux(lookupFunction(FUNCSMAP, TY)) +``` + +```{.k .symbolic} + syntax List ::= #getBlocks( MaybeMap, Ty ) [function, total, no-evaluators] + rule #getBlocks(_, TY) => #getBlocksAux(lookupFunctionKore(TY)) +``` - rule #getBlocks(TY) => #getBlocksAux(lookupFunction(TY)) +```k + syntax List ::= #getBlocksAux( MonoItemKind ) [function, total] // returns blocks from the body rule #getBlocksAux(monoItemFn(_, _, noBody)) => .List @@ -312,27 +326,44 @@ where the returned result should go. syntax KItem ::= #checkFunctionFilter(MonoItemKind) rule #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), SPAN)) - => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND, SPAN) + => #execTerminatorCall(Ty, lookupFunction(FUNCSMAP, Ty), ARGS, DEST, TARGET, UNWIND, SPAN) ... + FUNCSMAP rule #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN)) - => #execTerminatorCall({#projectedCallTy(I, PROJS, LOCALS)}:>Ty, lookupFunction({#projectedCallTy(I, PROJS, LOCALS)}:>Ty), ARGS, DEST, TARGET, UNWIND, SPAN) + => #execTerminatorCall({#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)}:>Ty, lookupFunction(FUNCSMAP, {#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)}:>Ty), ARGS, DEST, TARGET, UNWIND, SPAN) ... LOCALS - requires isTy(#projectedCallTy(I, PROJS, LOCALS)) + FUNCSMAP + TYPESMAP + requires isTy(#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)) [preserves-definedness] // valid local indexing checked, projected call target must resolve to a Ty +``` - syntax MaybeTy ::= #projectedCallTy(Int, ProjectionElems, List) [function, total, no-evaluators] +```{.k .concrete} + syntax MaybeTy ::= #projectedCallTy(MaybeMap, Int, ProjectionElems, List) [function, total] - rule #projectedCallTy(I, PROJS, LOCALS) - => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) + rule #projectedCallTy(TYPESMAP, I, PROJS, LOCALS) + => getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) requires 0 <=Int I andBool I TyUnknown [owise] +```{.k .symbolic} + syntax MaybeTy ::= #projectedCallTy(MaybeMap, Int, ProjectionElems, List) [function, total, no-evaluators] + + rule #projectedCallTy(_, I, PROJS, LOCALS) + => getTyOf(noMap, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) + requires 0 <=Int I andBool I TyUnknown [owise] // Intrinsic function call - execute directly without state switching rule [termCallIntrinsic]: @@ -537,14 +568,15 @@ Therefore a heuristics is used here: ... + TYPESMAP requires 0 <=Int CLOSURE andBool CLOSURE TypedLocal))) + andBool isTupleType(lookupTy(TYPESMAP, tyOfLocal({LOCALS[TUPLE]}:>TypedLocal))) andBool isTypedLocal(LOCALS[CLOSURE]) andBool ( - typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)) - orBool isFunType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) + typeInfoVoidType ==K lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)) + orBool isFunType(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) ) [priority(40), preserves-definedness] @@ -570,17 +602,18 @@ Therefore a heuristics is used here: ... + TYPESMAP requires 0 <=Int CLOSURE andBool CLOSURE TypedLocal))) + andBool isTupleType(lookupTy(TYPESMAP, tyOfLocal({LOCALS[TUPLE]}:>TypedLocal))) andBool isTypedLocal(LOCALS[CLOSURE]) // or the closure ref type pointee is missing from the type table - andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) - andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))) + andBool isRefType(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) + andBool isTy(pointeeTy(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))) andBool ( - lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType - orBool isFunType(lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty)) + lookupTy(TYPESMAP, {pointeeTy(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType + orBool isFunType(lookupTy(TYPESMAP, {pointeeTy(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty)) ) [priority(45), preserves-definedness] diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md index c5d764361..c0441647b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md @@ -45,6 +45,10 @@ module KMIR-CONFIGURATION // remaining call stack (without top frame) .List + // static data lookup tables (populated in concrete execution, noMap in symbolic execution) + noMap + noMap + noMap ``` @@ -60,6 +64,10 @@ rather than carrying static `Map` structures with the configuration. The functions are defined in the `RT-VALUE` module for now but should have their own module. +The configuration also contains cells for these lookup tables (`functions`, `types`, `memory`) +holding `MaybeMap` values. In concrete execution they are populated with `someMap(M)` for efficient +LLVM execution; in symbolic execution they are `noMap` and lookups use the generated functions instead. + ```k endmodule ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 89211d3f2..d7d49997c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -124,10 +124,11 @@ Constant operands are simply decoded according to their type. ```k rule operandConstant(constOperand(_, _, mirConst(KIND, TY, _))) - => #decodeConstant(KIND, TY, lookupTy(TY)) + => #decodeConstant(KIND, TY, lookupTy(TYPESMAP, TY)) ... - requires typeInfoVoidType =/=K lookupTy(TY) + TYPESMAP + requires typeInfoVoidType =/=K lookupTy(TYPESMAP, TY) ``` Function pointers are zero-sized constants whose `Ty` is a key in the function table instaed of the type table. @@ -137,8 +138,10 @@ Function pointers are zero-sized constants whose `Ty` is a key in the function t => FunPtr(TY) ... - requires typeInfoVoidType ==K lookupTy(TY) // not a valid type info - andBool lookupFunction(TY) =/=K monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(ID), noBody ) // valid function Ty + TYPESMAP + FUNCSMAP + requires typeInfoVoidType ==K lookupTy(TYPESMAP, TY) // not a valid type info + andBool lookupFunction(FUNCSMAP, TY) =/=K monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(ID), noBody ) // valid function Ty ``` ### Copying and Moving @@ -910,14 +913,15 @@ even though this could be supported. ) => #traverseProjection( toAlloc(ALLOC_ID), - {lookupAlloc(ALLOC_ID)}:>Value, + {lookupAlloc(ALLOCSMAP, ALLOC_ID)}:>Value, ALLOC_PROJS, // alloc projections .Contexts // previous contexts obsolete ) ~> #derefTruncate(METADATA_SIZE, PROJS) // then truncate, then continue with remaining projections ... - requires isValue(lookupAlloc(ALLOC_ID)) + ALLOCSMAP + requires isValue(lookupAlloc(ALLOCSMAP, ALLOC_ID)) [preserves-definedness] // sort projection checked ``` @@ -952,15 +956,17 @@ The most basic ones are simply accessing an operand, either directly or by way o rule rvalueUse(OPERAND) => OPERAND ... rule rvalueCast(CASTKIND, operandCopy(place(local(I), PROJS)) #as OPERAND, TY) - => #cast(OPERAND, CASTKIND, getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), TY) ... + => #cast(OPERAND, CASTKIND, getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), TY) ... LOCALS + TYPESMAP requires 0 <=Int I andBool I rvalueCast(CASTKIND, operandMove(place(local(I), PROJS)) #as OPERAND, TY) - => #cast(OPERAND, CASTKIND, getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), TY) ... + => #cast(OPERAND, CASTKIND, getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), TY) ... LOCALS + TYPESMAP requires 0 <=Int I andBool I rvalueRepeat(ELEM, tyConst(KIND, _)) => #mkArray(ELEM, readTyConstInt(KIND)) ... - requires isInt(readTyConstInt(KIND)) + rule rvalueRepeat(ELEM, tyConst(KIND, _)) => #mkArray(ELEM, readTyConstInt(TYPESMAP, KIND)) ... + TYPESMAP + requires isInt(readTyConstInt(TYPESMAP, KIND)) [preserves-definedness] rule #mkArray(ELEMENT:Value, N) => Range(makeList(N, ELEMENT)) ... @@ -1115,7 +1122,7 @@ and an array of the indeicated size gets reconstructed if the provided metadata ... // requires LENGTH +Int PTR_OFFSET <=Int ORIGIN_SIZE // refuse to create an invalid fat pointer - // andBool dynamicSize(1) ==K #metadataSize(lookupTy(_TY)) // expect a slice type + // andBool dynamicSize(1) ==K #metadataSize(lookupTyKore(_TY)) // expect a slice type // andBool hasIndexTail(PROJS) ??? rule ListItem(PtrLocal(OFFSET, PLACE, _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE))) ListItem(Aggregate(_, .List)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT)) @@ -1149,8 +1156,9 @@ The `getTyOf` helper applies the projections from the `Place` to determine the ` ```k rule rvalueDiscriminant(place(local(I), PROJS) #as PLACE) - => #discriminant(operandCopy(PLACE), getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)) ... + => #discriminant(operandCopy(PLACE), getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)) ... LOCALS + TYPESMAP requires 0 <=Int I andBool I #discriminant(Aggregate(IDX, _), TY:Ty) - => Integer(#lookupDiscrAux(discriminantsOf(lookupTy(TY)), IDX), 0, false) // HACK: bit width 0 means "flexible" + => Integer(#lookupDiscrAux(discriminantsOf(lookupTy(TYPESMAP, TY)), IDX), 0, false) // HACK: bit width 0 means "flexible" ... - requires asInt(IDX) TYPESMAP + requires asInt(IDX) rvalueRef(REGION, KIND, place(local(I), PROJS)) ... LOCALS + TYPESMAP requires 0 <=Int I andBool I rvalueRef(_REGION, KIND, place(local(I), PROJS)) => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts) - ~> #forRef(#mutabilityOf(KIND), metadata(#metadataSize(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO: Sus on this rule + ~> #forRef(#mutabilityOf(KIND), metadata(#metadataSize(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO: Sus on this rule ... LOCALS + TYPESMAP requires 0 <=Int I andBool I rvalueAddressOf(MUT, place(local(I), PROJS)) => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts) - ~> #forPtr(MUT, metadata(#metadataSize(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO These initial values might get overwrote + ~> #forPtr(MUT, metadata(#metadataSize(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO These initial values might get overwrote // we should use #alignOf to emulate the address ... LOCALS + TYPESMAP requires 0 <=Int I andBool I #cast(Integer(VAL, WIDTH, _SIGNEDNESS), castKindIntToInt, _, TY) => - #intAsType(VAL, WIDTH, #numTypeOf(lookupTy(TY))) + #intAsType(VAL, WIDTH, #numTypeOf(lookupTy(TYPESMAP, TY))) ... - requires #isIntType(lookupTy(TY)) + TYPESMAP + requires #isIntType(lookupTy(TYPESMAP, TY)) [preserves-definedness] // ensures #numTypeOf is defined ``` @@ -1395,19 +1408,21 @@ Boolean values can also be cast to Integers (encoding `true` as `1`). ```k rule #cast(BoolVal(VAL), castKindIntToInt, _, TY) => - #intAsType(1, 8, #numTypeOf(lookupTy(TY))) + #intAsType(1, 8, #numTypeOf(lookupTy(TYPESMAP, TY))) ... - requires #isIntType(lookupTy(TY)) + TYPESMAP + requires #isIntType(lookupTy(TYPESMAP, TY)) andBool VAL [preserves-definedness] // ensures #numTypeOf is defined rule #cast(BoolVal(VAL), castKindIntToInt, _, TY) => - #intAsType(0, 8, #numTypeOf(lookupTy(TY))) + #intAsType(0, 8, #numTypeOf(lookupTy(TYPESMAP, TY))) ... - requires #isIntType(lookupTy(TY)) + TYPESMAP + requires #isIntType(lookupTy(TYPESMAP, TY)) andBool notBool VAL [preserves-definedness] // ensures #numTypeOf is defined ``` @@ -1439,7 +1454,8 @@ the cast preserves the source pointer and its metadata unchanged. => PtrLocal(OFFSET, PLACE, MUT, META) ... - requires pointeeTy(lookupTy(TY_SOURCE)) ==K pointeeTy(lookupTy(TY_TARGET)) + TYPESMAP + requires pointeeTy(lookupTy(TYPESMAP, TY_SOURCE)) ==K pointeeTy(lookupTy(TYPESMAP, TY_TARGET)) [priority(45), preserves-definedness] // valid map lookups checked ``` @@ -1450,28 +1466,33 @@ Otherwise, compute the type projection and convert metadata accordingly. => PtrLocal( OFFSET, - place(LOCAL, appendP(PROJS, {#typeProjection(lookupTy(TY_SOURCE), lookupTy(TY_TARGET))}:>ProjectionElems)), + place(LOCAL, appendP(PROJS, {#typeProjection(TYPESMAP, lookupTy(TYPESMAP, TY_SOURCE), lookupTy(TYPESMAP, TY_TARGET))}:>ProjectionElems)), MUT, - #convertMetadata(META, lookupTy(TY_TARGET)) + #convertMetadata(TYPESMAP, META, lookupTy(TYPESMAP, TY_TARGET)) ) ... - requires NoProjectionElems =/=K #typeProjection(lookupTy(TY_SOURCE), lookupTy(TY_TARGET)) + TYPESMAP + requires NoProjectionElems =/=K #typeProjection(TYPESMAP, lookupTy(TYPESMAP, TY_SOURCE), lookupTy(TYPESMAP, TY_TARGET)) [preserves-definedness] // valid map lookups checked ``` The pointer's metadata needs to be adapted to the new type. -```k - syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total, no-evaluators] +```{.k .concrete} + syntax Metadata ::= #convertMetadata ( MaybeMap , Metadata , TypeInfo ) [function, total] +``` + +```{.k .symbolic} + syntax Metadata ::= #convertMetadata ( MaybeMap , Metadata , TypeInfo ) [function, total, no-evaluators] ``` Pointers to slices can be converted to pointers to single elements, _losing_ their metadata. ```k - rule #convertMetadata( metadata(SIZE, OFFSET, _) , typeInfoRefType(POINTEE_TY) ) => metadata(noMetadataSize, OFFSET, SIZE) - requires #metadataSize(POINTEE_TY) ==K noMetadataSize [priority(60)] - rule #convertMetadata( metadata(SIZE, OFFSET, _) , typeInfoPtrType(POINTEE_TY) ) => metadata(noMetadataSize, OFFSET, SIZE) - requires #metadataSize(POINTEE_TY) ==K noMetadataSize [priority(60)] + rule #convertMetadata(TYPESMAP, metadata(SIZE, OFFSET, _) , typeInfoRefType(POINTEE_TY) ) => metadata(noMetadataSize, OFFSET, SIZE) + requires #metadataSize(TYPESMAP, POINTEE_TY) ==K noMetadataSize [priority(60)] + rule #convertMetadata(TYPESMAP, metadata(SIZE, OFFSET, _) , typeInfoPtrType(POINTEE_TY) ) => metadata(noMetadataSize, OFFSET, SIZE) + requires #metadataSize(TYPESMAP, POINTEE_TY) ==K noMetadataSize [priority(60)] ``` Conversely, when casting a pointer to an element to a pointer to a slice or array, @@ -1481,17 +1502,17 @@ the original allocation size must be checked to be sufficient. ```k // no metadata to begin with, fill it in from target type (NB dynamicSize(1) if dynamic) - rule #convertMetadata( metadata(noMetadataSize, OFFSET, _) , typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, noMetadataSize) - rule #convertMetadata( metadata(noMetadataSize, OFFSET, ORIGIN_SIZE ) , typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) + rule #convertMetadata(TYPESMAP, metadata(noMetadataSize, OFFSET, _) , typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(TYPESMAP, POINTEE_TY), OFFSET, noMetadataSize) + rule #convertMetadata(TYPESMAP, metadata(noMetadataSize, OFFSET, ORIGIN_SIZE ) , typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(TYPESMAP, POINTEE_TY), OFFSET, ORIGIN_SIZE) ``` Conversion from an array to a slice pointer requires adding metadata (`dynamicSize`) with the previously-static length. ```k // convert static length to dynamic length - rule #convertMetadata(metadata(staticSize(SIZE), OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, staticSize(SIZE)) - requires #metadataSize(POINTEE_TY) ==K dynamicSize(1) - rule #convertMetadata(metadata(staticSize(SIZE), OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, staticSize(SIZE)) - requires #metadataSize(POINTEE_TY) ==K dynamicSize(1) + rule #convertMetadata(TYPESMAP, metadata(staticSize(SIZE), OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, staticSize(SIZE)) + requires #metadataSize(TYPESMAP, POINTEE_TY) ==K dynamicSize(1) + rule #convertMetadata(TYPESMAP, metadata(staticSize(SIZE), OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, staticSize(SIZE)) + requires #metadataSize(TYPESMAP, POINTEE_TY) ==K dynamicSize(1) ``` Conversion from a slice to an array pointer, or between different static length array pointers, is allowed in all cases. @@ -1500,29 +1521,29 @@ It may however be illegal to _dereference_ (i.e., access) the created pointer, d **TODO** we can mark cases of insufficient original length as "InvalidCast" in the future, similar to the above future work. ```k - rule #convertMetadata(metadata(staticSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) - requires #metadataSize(POINTEE_TY) =/=K dynamicSize(1) - rule #convertMetadata(metadata(staticSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) - requires #metadataSize(POINTEE_TY) =/=K dynamicSize(1) + rule #convertMetadata(TYPESMAP, metadata(staticSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(TYPESMAP, POINTEE_TY), OFFSET, ORIGIN_SIZE) + requires #metadataSize(TYPESMAP, POINTEE_TY) =/=K dynamicSize(1) + rule #convertMetadata(TYPESMAP, metadata(staticSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(TYPESMAP, POINTEE_TY), OFFSET, ORIGIN_SIZE) + requires #metadataSize(TYPESMAP, POINTEE_TY) =/=K dynamicSize(1) - rule #convertMetadata(metadata(dynamicSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) - requires #metadataSize(POINTEE_TY) =/=K dynamicSize(1) - rule #convertMetadata(metadata(dynamicSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) - requires #metadataSize(POINTEE_TY) =/=K dynamicSize(1) + rule #convertMetadata(TYPESMAP, metadata(dynamicSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(TYPESMAP, POINTEE_TY), OFFSET, ORIGIN_SIZE) + requires #metadataSize(TYPESMAP, POINTEE_TY) =/=K dynamicSize(1) + rule #convertMetadata(TYPESMAP, metadata(dynamicSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(TYPESMAP, POINTEE_TY), OFFSET, ORIGIN_SIZE) + requires #metadataSize(TYPESMAP, POINTEE_TY) =/=K dynamicSize(1) ``` For a cast bwetween two pointer types with `dynamicSize` metadata (unlikely to occur), the dynamic size value is retained. ```k - rule #convertMetadata(metadata(dynamicSize(SIZE), OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, dynamicSize(SIZE)) - requires #metadataSize(POINTEE_TY) ==K dynamicSize(1) - rule #convertMetadata(metadata(dynamicSize(SIZE), OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, dynamicSize(SIZE)) - requires #metadataSize(POINTEE_TY) ==K dynamicSize(1) + rule #convertMetadata(TYPESMAP, metadata(dynamicSize(SIZE), OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, dynamicSize(SIZE)) + requires #metadataSize(TYPESMAP, POINTEE_TY) ==K dynamicSize(1) + rule #convertMetadata(TYPESMAP, metadata(dynamicSize(SIZE), OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, dynamicSize(SIZE)) + requires #metadataSize(TYPESMAP, POINTEE_TY) ==K dynamicSize(1) ``` ```k // non-pointer and non-ref target type (should not happen!) - rule #convertMetadata( metadata(SIZE, OFFSET, _) , _OTHER_INFO ) => metadata(noMetadataSize, OFFSET, SIZE) [priority(100)] + rule #convertMetadata(_, metadata(SIZE, OFFSET, _) , _OTHER_INFO ) => metadata(noMetadataSize, OFFSET, SIZE) [priority(100)] ``` `PointerCoercion` may achieve a simmilar effect, or deal with function and closure pointers, depending on the coercion type: @@ -1572,13 +1593,16 @@ What can be supported without additional layout consideration is trivial casts b ```k rule #cast(Reference(_, _, _, _) #as REF, castKindTransmute, TY_SOURCE, TY_TARGET) => REF ... - requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET) + TYPESMAP + requires lookupTy(TYPESMAP, TY_SOURCE) ==K lookupTy(TYPESMAP, TY_TARGET) rule #cast(AllocRef(_, _, _) #as REF, castKindTransmute, TY_SOURCE, TY_TARGET) => REF ... - requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET) + TYPESMAP + requires lookupTy(TYPESMAP, TY_SOURCE) ==K lookupTy(TYPESMAP, TY_TARGET) rule #cast(PtrLocal(_, _, _, _) #as PTR, castKindTransmute, TY_SOURCE, TY_TARGET) => PTR ... - requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET) + TYPESMAP + requires lookupTy(TYPESMAP, TY_SOURCE) ==K lookupTy(TYPESMAP, TY_TARGET) ``` Other `Transmute` casts that can be resolved are round-trip casts from type A to type B and then directly back from B to A. @@ -1593,8 +1617,9 @@ The first cast is reified as a `thunk`, the second one resolves it and eliminate ) => DATA ... - requires lookupTy(TY_SRC_INNER) ==K lookupTy(TY_DEST_OUTER) // cast is a round-trip - andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant) + TYPESMAP + requires lookupTy(TYPESMAP, TY_SRC_INNER) ==K lookupTy(TYPESMAP, TY_DEST_OUTER) // cast is a round-trip + andBool lookupTy(TYPESMAP, TY_DEST_INNER) ==K lookupTy(TYPESMAP, TY_SRC_OUTER) // and is well-formed (invariant) ``` Transmuting a value `T` into a single-field wrapper struct `G` (or vice versa) is sound when the struct @@ -1610,7 +1635,8 @@ The layout is the same for the wrapped type and so the cast in either direction Aggregate(variantIdx(0), ListItem(VAL)) ... - requires #transparentFieldTy(lookupTy(TY_TARGET)) ==K TY_SOURCE + TYPESMAP + requires #transparentFieldTy(lookupTy(TYPESMAP, TY_TARGET)) ==K TY_SOURCE // Down: Wrapper(T) -> T rule #cast(Aggregate(variantIdx(0), ListItem(VAL)), castKindTransmute, TY_SOURCE, TY_TARGET) @@ -1618,7 +1644,8 @@ The layout is the same for the wrapped type and so the cast in either direction VAL ... - requires {#transparentFieldTy(lookupTy(TY_SOURCE))}:>Ty ==K TY_TARGET + TYPESMAP + requires {#transparentFieldTy(lookupTy(TYPESMAP, TY_SOURCE))}:>Ty ==K TY_TARGET ``` Casting a byte array/slice to an integer reinterprets the bytes in little-endian order. @@ -1634,12 +1661,13 @@ Casting a byte array/slice to an integer reinterprets the bytes in little-endian #intAsType( #littleEndianFromBytes(ELEMS), size(ELEMS) *Int 8, - #numTypeOf(lookupTy(TY_TARGET)) + #numTypeOf(lookupTy(TYPESMAP, TY_TARGET)) ) ... - requires #isIntType(lookupTy(TY_TARGET)) - andBool size(ELEMS) *Int 8 ==Int #bitWidth(#numTypeOf(lookupTy(TY_TARGET))) + TYPESMAP + requires #isIntType(lookupTy(TYPESMAP, TY_TARGET)) + andBool size(ELEMS) *Int 8 ==Int #bitWidth(#numTypeOf(lookupTy(TYPESMAP, TY_TARGET))) andBool #areLittleEndianBytes(ELEMS) [preserves-definedness] // ensures #numTypeOf is defined @@ -1671,8 +1699,9 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. Range(#littleEndianBytesFromInt(VAL, WIDTH)) ... - requires #isStaticU8Array(lookupTy(TY_TARGET)) - andBool WIDTH ==Int #staticArrayLenBits(lookupTy(TY_TARGET)) + TYPESMAP + requires #isStaticU8Array(TYPESMAP, lookupTy(TYPESMAP, TY_TARGET)) + andBool WIDTH ==Int #staticArrayLenBits(TYPESMAP, lookupTy(TYPESMAP, TY_TARGET)) // andBool WIDTH >=Int 0 ensured by the above // andBool WIDTH % 8 == 0 ensured by the above [preserves-definedness] // ensures element type/length are well-formed @@ -1696,18 +1725,39 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. requires COUNT >Int 0 [preserves-definedness] - syntax Bool ::= #isStaticU8Array ( TypeInfo ) [function, total, no-evaluators] - // ------------------------------------------------------------- - rule #isStaticU8Array(typeInfoArrayType(ELEM_TY, someTyConst(_))) - => lookupTy(ELEM_TY) ==K typeInfoPrimitiveType(primTypeUint(uintTyU8)) - rule #isStaticU8Array(_OTHER) => false [owise] +``` - syntax Int ::= #staticArrayLenBits ( TypeInfo ) [function, total, no-evaluators] - // ------------------------------------------------------------- - rule #staticArrayLenBits(typeInfoArrayType(_, someTyConst(tyConst(KIND, _)))) - => readTyConstInt(KIND) *Int 8 +```{.k .concrete} + syntax Bool ::= #isStaticU8Array ( MaybeMap , TypeInfo ) [function, total] + rule #isStaticU8Array(TYPESMAP, typeInfoArrayType(ELEM_TY, someTyConst(_))) + => lookupTy(TYPESMAP, ELEM_TY) ==K typeInfoPrimitiveType(primTypeUint(uintTyU8)) + rule #isStaticU8Array(_, _OTHER) => false [owise] +``` + +```{.k .symbolic} + syntax Bool ::= #isStaticU8Array ( MaybeMap , TypeInfo ) [function, total, no-evaluators] + rule #isStaticU8Array(_, typeInfoArrayType(ELEM_TY, someTyConst(_))) + => lookupTyKore(ELEM_TY) ==K typeInfoPrimitiveType(primTypeUint(uintTyU8)) + rule #isStaticU8Array(_, _OTHER) => false [owise] +``` + +```{.k .concrete} + syntax Int ::= #staticArrayLenBits ( MaybeMap , TypeInfo ) [function, total] + rule #staticArrayLenBits(TYPESMAP, typeInfoArrayType(_, someTyConst(tyConst(KIND, _)))) + => readTyConstInt(TYPESMAP, KIND) *Int 8 + [preserves-definedness] + rule #staticArrayLenBits(_, _OTHER) => 0 [owise] +``` + +```{.k .symbolic} + syntax Int ::= #staticArrayLenBits ( MaybeMap , TypeInfo ) [function, total, no-evaluators] + rule #staticArrayLenBits(_, typeInfoArrayType(_, someTyConst(tyConst(KIND, _)))) + => readTyConstInt(noMap, KIND) *Int 8 [preserves-definedness] - rule #staticArrayLenBits(_OTHER) => 0 [owise] + rule #staticArrayLenBits(_, _OTHER) => 0 [owise] +``` + +```k ``` A transmutation from an integer to an enum is wellformed if: @@ -1734,17 +1784,19 @@ index; if not, return `#UBErrorInvalidDiscriminantsInEnumCast`. => #UBErrorInvalidDiscriminantsInEnumCast - requires #isEnumWithoutFields(lookupTy(TY_TO)) - andBool notBool #validDiscriminant( truncate(VAL, WIDTH, Unsigned) , lookupTy(TY_TO) ) + TYPESMAP + requires #isEnumWithoutFields(lookupTy(TYPESMAP, TY_TO)) + andBool notBool #validDiscriminant( truncate(VAL, WIDTH, Unsigned) , lookupTy(TYPESMAP, TY_TO) ) rule #cast( Integer ( VAL , WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) => - Aggregate( #findVariantIdxFromTy( truncate(VAL, WIDTH, Unsigned), lookupTy(TY_TO) ) , .List ) + Aggregate( #findVariantIdxFromTy( truncate(VAL, WIDTH, Unsigned), lookupTy(TYPESMAP, TY_TO) ) , .List ) ... - requires #isEnumWithoutFields(lookupTy(TY_TO)) - andBool #validDiscriminant( truncate(VAL, WIDTH, Unsigned) , lookupTy(TY_TO)) + TYPESMAP + requires #isEnumWithoutFields(lookupTy(TYPESMAP, TY_TO)) + andBool #validDiscriminant( truncate(VAL, WIDTH, Unsigned) , lookupTy(TYPESMAP, TY_TO)) syntax VariantIdx ::= #findVariantIdxFromTy ( Int , TypeInfo ) [function, total] //------------------------------------------------------------------------------ @@ -1772,9 +1824,10 @@ mapped to the elements. rule #transmuteElems(VALS, TY_FROM, TY_TO) => - #transmuteElemsAux(.List, VALS, getArrayElemTy(lookupTy(TY_FROM)), getArrayElemTy(lookupTy(TY_TO))) + #transmuteElemsAux(.List, VALS, getArrayElemTy(lookupTy(TYPESMAP, TY_FROM)), getArrayElemTy(lookupTy(TYPESMAP, TY_TO))) ... + TYPESMAP rule #transmuteElemsAux(ACC, .List, _, _) => Range(ACC) ... @@ -1809,9 +1862,10 @@ the safety of this cast. The logic of the semantics and saftey of this cast for #UBInvalidTransmuteMaybeUninit ... - requires #isUnionType(lookupTy(TY_TO)) - andBool #typeNameIs(lookupTy(TY_TO), "std::mem::MaybeUninit<") - andBool TY_FROM =/=K getFieldTy(#lookupMaybeTy(getFieldTy(lookupTy(TY_TO), 1)), 0) + TYPESMAP + requires #isUnionType(lookupTy(TYPESMAP, TY_TO)) + andBool #typeNameIs(lookupTy(TYPESMAP, TY_TO), "std::mem::MaybeUninit<") + andBool TY_FROM =/=K getFieldTy(#lookupMaybeTy(TYPESMAP, getFieldTy(lookupTy(TYPESMAP, TY_TO), 1)), 0) rule #cast( VAL:Value , castKindTransmute , TY_FROM , TY_TO ) @@ -1819,9 +1873,10 @@ the safety of this cast. The logic of the semantics and saftey of this cast for Union( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem(VAL) .List )) ... - requires #isUnionType(lookupTy(TY_TO)) - andBool #typeNameIs(lookupTy(TY_TO), "std::mem::MaybeUninit<") - andBool TY_FROM ==K getFieldTy(#lookupMaybeTy(getFieldTy(lookupTy(TY_TO), 1)), 0) + TYPESMAP + requires #isUnionType(lookupTy(TYPESMAP, TY_TO)) + andBool #typeNameIs(lookupTy(TYPESMAP, TY_TO), "std::mem::MaybeUninit<") + andBool TY_FROM ==K getFieldTy(#lookupMaybeTy(TYPESMAP, getFieldTy(lookupTy(TYPESMAP, TY_TO), 1)), 0) // Converting static or dynamic sized array of `T` to array of `std::mem::MaybeUninit`. // FIXME: Might need to check sizes as this cast could come from transmute_unchecked @@ -1831,13 +1886,14 @@ the safety of this cast. The logic of the semantics and saftey of this cast for #transmuteElems(LIST, TY_FROM, TY_TO) ... - requires #isArrayType(lookupTy(TY_FROM)) andBool #isArrayType(lookupTy(TY_TO)) - andBool #isUnionType(getArrayElemTypeInfo(lookupTy(TY_TO))) - andBool #typeNameIs(getArrayElemTypeInfo(lookupTy(TY_TO)), "std::mem::MaybeUninit<") - andBool getArrayElemTypeInfo(lookupTy(TY_FROM)) - ==K #lookupMaybeTy(getFieldTy( // ManuallyDrop field 0 Ty (T) - #lookupMaybeTy(getFieldTy( // MaybeUninit field 1 Ty (ManuallyDrop) - getArrayElemTypeInfo(lookupTy(TY_TO)), // Array Element Ty + TYPESMAP + requires #isArrayType(lookupTy(TYPESMAP, TY_FROM)) andBool #isArrayType(lookupTy(TYPESMAP, TY_TO)) + andBool #isUnionType(getArrayElemTypeInfo(TYPESMAP, lookupTy(TYPESMAP, TY_TO))) + andBool #typeNameIs(getArrayElemTypeInfo(TYPESMAP, lookupTy(TYPESMAP, TY_TO)), "std::mem::MaybeUninit<") + andBool getArrayElemTypeInfo(TYPESMAP, lookupTy(TYPESMAP, TY_FROM)) + ==K #lookupMaybeTy(TYPESMAP, getFieldTy( // ManuallyDrop field 0 Ty (T) + #lookupMaybeTy(TYPESMAP, getFieldTy( // MaybeUninit field 1 Ty (ManuallyDrop) + getArrayElemTypeInfo(TYPESMAP, lookupTy(TYPESMAP, TY_TO)), // Array Element Ty 1 )), 0 @@ -1870,9 +1926,10 @@ For allocated constants without provenance, the decoder works directly with the _TY, TYPEINFO ) - => #decodeValue(BYTES, TYPEINFO) + => #decodeValue(TYPESMAP, BYTES, TYPEINFO) ... + TYPESMAP ``` Zero-sized types can be decoded trivially into their respective representation. @@ -1906,10 +1963,12 @@ into the `` heap where all allocated constants have been decoded at prog _TY, typeInfoRefType(POINTEE_TY) ) - => AllocRef(ALLOC_ID, .ProjectionElems, metadata(#metadataSize(POINTEE_TY), 0, #metadataSize(POINTEE_TY))) + => AllocRef(ALLOC_ID, .ProjectionElems, metadata(#metadataSize(TYPESMAP, POINTEE_TY), 0, #metadataSize(TYPESMAP, POINTEE_TY))) ... - requires isValue(lookupAlloc(ALLOC_ID)) + ALLOCSMAP + TYPESMAP + requires isValue(lookupAlloc(ALLOCSMAP, ALLOC_ID)) andBool lengthBytes(BYTES) ==Int 8 // no dynamic metadata rule #decodeConstant( @@ -1926,7 +1985,8 @@ into the `` heap where all allocated constants have been decoded at prog // assumes usize == u64 ... - requires isValue(lookupAlloc(ALLOC_ID)) + ALLOCSMAP + requires isValue(lookupAlloc(ALLOCSMAP, ALLOC_ID)) andBool lengthBytes(BYTES) ==Int 16 // fat pointer (assumes usize == u64) [preserves-definedness] // Byte length checked to be sufficient ``` @@ -2315,16 +2375,18 @@ This information is read from the layout in the `TypeInfo` if available, or a fi // FIXME: 64 is hardcoded since usize not supported rule rvalueNullaryOp(nullOpSizeOf, TY) => - Integer(#sizeOf(lookupTy(TY)), 64, false) + Integer(#sizeOf(TYPESMAP, lookupTy(TYPESMAP, TY)), 64, false) ... - requires lookupTy(TY) =/=K typeInfoVoidType + TYPESMAP + requires lookupTy(TYPESMAP, TY) =/=K typeInfoVoidType rule rvalueNullaryOp(nullOpAlignOf, TY) => - Integer(#alignOf(lookupTy(TY)), 64, false) + Integer(#alignOf(TYPESMAP, lookupTy(TYPESMAP, TY)), 64, false) ... - requires lookupTy(TY) =/=K typeInfoVoidType + TYPESMAP + requires lookupTy(TYPESMAP, TY) =/=K typeInfoVoidType ``` `nullOpOffsetOf(VariantAndFieldIndices)` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md index fa040c665..10a8f628e 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md @@ -36,20 +36,29 @@ and arrays (where layout is trivial). ### Decoding `PrimitiveType`s ```k - syntax Evaluation ::= #decodeValue ( Bytes , TypeInfo ) [function, total, symbol(decodeValue), no-evaluators] - | UnableToDecode ( Bytes , TypeInfo ) [symbol(Evaluation::UnableToDecode)] + syntax Evaluation ::= UnableToDecode ( Bytes , TypeInfo ) [symbol(Evaluation::UnableToDecode)] | UnableToDecodePy ( msg: String ) [symbol(Evaluation::UnableToDecodePy)] +``` + +```{.k .concrete} + syntax Evaluation ::= #decodeValue ( MaybeMap , Bytes , TypeInfo ) [function, total, symbol(decodeValue)] +``` +```{.k .symbolic} + syntax Evaluation ::= #decodeValue ( MaybeMap , Bytes , TypeInfo ) [function, total, symbol(decodeValue), no-evaluators] +``` + +```k // Boolean: should be one byte with value one or zero - rule #decodeValue(BYTES, typeInfoPrimitiveType(primTypeBool)) => BoolVal(false) + rule #decodeValue(_, BYTES, typeInfoPrimitiveType(primTypeBool)) => BoolVal(false) requires 0 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1 - rule #decodeValue(BYTES, typeInfoPrimitiveType(primTypeBool)) => BoolVal(true) + rule #decodeValue(_, BYTES, typeInfoPrimitiveType(primTypeBool)) => BoolVal(true) requires 1 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1 // Integer: handled in separate module for numeric operation_s - rule #decodeValue(BYTES, TYPEINFO) => #decodeInteger(BYTES, #intTypeOf(TYPEINFO)) - requires #isIntType(TYPEINFO) andBool lengthBytes(BYTES) ==Int #elemSize(TYPEINFO) + rule #decodeValue(TYPESMAP, BYTES, TYPEINFO) => #decodeInteger(BYTES, #intTypeOf(TYPEINFO)) + requires #isIntType(TYPEINFO) andBool lengthBytes(BYTES) ==Int #elemSize(TYPESMAP, TYPEINFO) [preserves-definedness] // TODO Char type @@ -63,14 +72,24 @@ and arrays (where layout is trivial). Arrays are decoded iteratively, using a known (expected) length or the length of the byte array. -```k -rule #decodeValue(BYTES, typeInfoArrayType(ELEMTY, someTyConst(tyConst(LEN, _)))) - => #decodeArrayAllocation(BYTES, lookupTy(ELEMTY), readTyConstInt(LEN)) - requires isInt(readTyConstInt(LEN)) +```{.k .concrete} +rule #decodeValue(TYPESMAP, BYTES, typeInfoArrayType(ELEMTY, someTyConst(tyConst(LEN, _)))) + => #decodeArrayAllocation(TYPESMAP, BYTES, lookupTy(TYPESMAP, ELEMTY), readTyConstInt(TYPESMAP, LEN)) + requires isInt(readTyConstInt(TYPESMAP, LEN)) + [preserves-definedness] + +rule #decodeValue(TYPESMAP, BYTES, typeInfoArrayType(ELEMTY, noTyConst)) + => #decodeSliceAllocation(TYPESMAP, BYTES, lookupTy(TYPESMAP, ELEMTY)) +``` + +```{.k .symbolic} +rule #decodeValue(_, BYTES, typeInfoArrayType(ELEMTY, someTyConst(tyConst(LEN, _)))) + => #decodeArrayAllocation(noMap, BYTES, lookupTyKore(ELEMTY), readTyConstInt(noMap, LEN)) + requires isInt(readTyConstInt(noMap, LEN)) [preserves-definedness] -rule #decodeValue(BYTES, typeInfoArrayType(ELEMTY, noTyConst)) - => #decodeSliceAllocation(BYTES, lookupTy(ELEMTY)) +rule #decodeValue(_, BYTES, typeInfoArrayType(ELEMTY, noTyConst)) + => #decodeSliceAllocation(noMap, BYTES, lookupTyKore(ELEMTY)) ``` ### Struct decoding @@ -85,22 +104,22 @@ When using layout offsets we always return fields in declaration order within th // Struct decoding rules (top level) // --------------------------------------------------------------------------- // Use the offsets when they are provided and the input length is sufficient. -rule #decodeValue(BYTES, typeInfoStructType(_, _, TYS, LAYOUT)) - => Aggregate(variantIdx(0), #decodeFieldsWithOffsets(BYTES, TYS, #layoutOffsets(LAYOUT))) +rule #decodeValue(TYPESMAP, BYTES, typeInfoStructType(_, _, TYS, LAYOUT)) + => Aggregate(variantIdx(0), #decodeFieldsWithOffsets(TYPESMAP, BYTES, TYS, #layoutOffsets(LAYOUT))) requires #layoutOffsets(LAYOUT) =/=K .MachineSizes - andBool 0 <=Int #neededBytesForOffsets(TYS, #layoutOffsets(LAYOUT)) - andBool lengthBytes(BYTES) >=Int #neededBytesForOffsets(TYS, #layoutOffsets(LAYOUT)) + andBool 0 <=Int #neededBytesForOffsets(TYPESMAP, TYS, #layoutOffsets(LAYOUT)) + andBool lengthBytes(BYTES) >=Int #neededBytesForOffsets(TYPESMAP, TYS, #layoutOffsets(LAYOUT)) [preserves-definedness] -rule #decodeValue(BYTES, typeInfoTupleType(.Tys, _)) +rule #decodeValue(_, BYTES, typeInfoTupleType(.Tys, _)) => Aggregate(variantIdx(0), .List) requires lengthBytes(BYTES) ==Int 0 -rule #decodeValue(BYTES, typeInfoTupleType(TYS, LAYOUT)) - => Aggregate(variantIdx(0), #decodeFieldsWithOffsets(BYTES, TYS, #layoutOffsets(LAYOUT))) +rule #decodeValue(TYPESMAP, BYTES, typeInfoTupleType(TYS, LAYOUT)) + => Aggregate(variantIdx(0), #decodeFieldsWithOffsets(TYPESMAP, BYTES, TYS, #layoutOffsets(LAYOUT))) requires #layoutOffsets(LAYOUT) =/=K .MachineSizes - andBool 0 <=Int #neededBytesForOffsets(TYS, #layoutOffsets(LAYOUT)) - andBool lengthBytes(BYTES) >=Int #neededBytesForOffsets(TYS, #layoutOffsets(LAYOUT)) + andBool 0 <=Int #neededBytesForOffsets(TYPESMAP, TYS, #layoutOffsets(LAYOUT)) + andBool lengthBytes(BYTES) >=Int #neededBytesForOffsets(TYPESMAP, TYS, #layoutOffsets(LAYOUT)) [preserves-definedness] // --------------------------------------------------------------------------- @@ -110,102 +129,152 @@ rule #decodeValue(BYTES, typeInfoTupleType(TYS, LAYOUT)) syntax Int ::= #msBytes ( MachineSize ) [function, total] rule #msBytes(machineSize(mirInt(NBITS))) => NBITS /Int 8 [preserves-definedness] rule #msBytes(machineSize(NBITS)) => NBITS /Int 8 [owise, preserves-definedness] +``` + +Minimum number of input bytes required to decode all fields by the chosen offsets. +Uses builtin maxInt to compute max(offset + size). The lists of types and +offsets must have the same length; if not, this function returns -1 to signal +an invalid layout for decoding. + +```{.k .concrete} +syntax Int ::= #neededBytesForOffsets ( MaybeMap , Tys , MachineSizes ) [function, total] +rule #neededBytesForOffsets(TYPESMAP, TY TYS, OFFSET OFFSETS) + => maxInt(#msBytes(OFFSET) +Int #elemSize(TYPESMAP, lookupTy(TYPESMAP, TY)), #neededBytesForOffsets(TYPESMAP, TYS, OFFSETS)) +``` + +```{.k .symbolic} +syntax Int ::= #neededBytesForOffsets ( MaybeMap , Tys , MachineSizes ) [function, total, no-evaluators] +rule #neededBytesForOffsets(_, TY TYS, OFFSET OFFSETS) + => maxInt(#msBytes(OFFSET) +Int #elemSize(noMap, lookupTyKore(TY)), #neededBytesForOffsets(noMap, TYS, OFFSETS)) +``` -// Minimum number of input bytes required to decode all fields by the chosen offsets. -// Uses builtin maxInt to compute max(offset + size). The lists of types and -// offsets must have the same length; if not, this function returns -1 to signal -// an invalid layout for decoding. -syntax Int ::= #neededBytesForOffsets ( Tys , MachineSizes ) [function, total, no-evaluators] -rule #neededBytesForOffsets(.Tys, .MachineSizes) => 0 -rule #neededBytesForOffsets(TY TYS, OFFSET OFFSETS) - => maxInt(#msBytes(OFFSET) +Int #elemSize(lookupTy(TY)), #neededBytesForOffsets(TYS, OFFSETS)) +```k +rule #neededBytesForOffsets(_, .Tys, .MachineSizes) => 0 // Any remaining pattern indicates a length mismatch between types and offsets. -rule #neededBytesForOffsets(_, _) => -1 [owise] +rule #neededBytesForOffsets(_, _, _) => -1 [owise] +``` + +Decode each field at its byte offset and return values in declaration order. +Any remaining pattern indicates a length mismatch between types and offsets. -// Decode each field at its byte offset and return values in declaration order. -syntax List ::= #decodeFieldsWithOffsets ( Bytes , Tys , MachineSizes ) [function, total, no-evaluators] -rule #decodeFieldsWithOffsets(_, .Tys, _OFFSETS) => .List -rule #decodeFieldsWithOffsets(_, _TYS, .MachineSizes) => .List [owise] -rule #decodeFieldsWithOffsets(BYTES, TY TYS, OFFSET OFFSETS) +```{.k .concrete} +syntax List ::= #decodeFieldsWithOffsets ( MaybeMap , Bytes , Tys , MachineSizes ) [function, total] +rule #decodeFieldsWithOffsets(TYPESMAP, BYTES, TY TYS, OFFSET OFFSETS) => ListItem( - #decodeValue( - substrBytes(BYTES, #msBytes(OFFSET), #msBytes(OFFSET) +Int #elemSize(lookupTy(TY))), - lookupTy(TY) + #decodeValue(TYPESMAP, + substrBytes(BYTES, #msBytes(OFFSET), #msBytes(OFFSET) +Int #elemSize(TYPESMAP, lookupTy(TYPESMAP, TY))), + lookupTy(TYPESMAP, TY) ) ) - #decodeFieldsWithOffsets(BYTES, TYS, OFFSETS) - requires lengthBytes(BYTES) >=Int (#msBytes(OFFSET) +Int #elemSize(lookupTy(TY))) + #decodeFieldsWithOffsets(TYPESMAP, BYTES, TYS, OFFSETS) + requires lengthBytes(BYTES) >=Int (#msBytes(OFFSET) +Int #elemSize(TYPESMAP, lookupTy(TYPESMAP, TY))) [preserves-definedness] ``` +```{.k .symbolic} +syntax List ::= #decodeFieldsWithOffsets ( MaybeMap , Bytes , Tys , MachineSizes ) [function, total, no-evaluators] +rule #decodeFieldsWithOffsets(_, BYTES, TY TYS, OFFSET OFFSETS) + => ListItem( + #decodeValue(noMap, + substrBytes(BYTES, #msBytes(OFFSET), #msBytes(OFFSET) +Int #elemSize(noMap, lookupTyKore(TY))), + lookupTyKore(TY) + ) + ) + #decodeFieldsWithOffsets(noMap, BYTES, TYS, OFFSETS) + requires lengthBytes(BYTES) >=Int (#msBytes(OFFSET) +Int #elemSize(noMap, lookupTyKore(TY))) + [preserves-definedness] +``` + +```k +rule #decodeFieldsWithOffsets(_, _, .Tys, _OFFSETS) => .List +rule #decodeFieldsWithOffsets(_, _, _TYS, .MachineSizes) => .List [owise] +``` + ### Error marker (becomes thunk) for other (unimplemented) cases All unimplemented cases will become thunks by way of this default rule: ```k - rule #decodeValue(BYTES, TYPEINFO) => UnableToDecode(BYTES, TYPEINFO) [owise] + rule #decodeValue(_, BYTES, TYPEINFO) => UnableToDecode(BYTES, TYPEINFO) [owise] ``` ## Helper function to determine the expected byte length for a type -```k +```{.k .concrete} // TODO: this function should go into the rt/types.md module - syntax Int ::= #elemSize ( TypeInfo ) [function, total, no-evaluators] + syntax Int ::= #elemSize ( MaybeMap , TypeInfo ) [function, total] +``` + +```{.k .symbolic} + syntax Int ::= #elemSize ( MaybeMap , TypeInfo ) [function, total, no-evaluators] ``` Known element sizes for common types: ```k // ---- Primitive types ---- - rule #elemSize(typeInfoPrimitiveType(primTypeBool)) => 1 + rule #elemSize(_, typeInfoPrimitiveType(primTypeBool)) => 1 // Rust `char` is a 32-bit Unicode scalar value - rule #elemSize(typeInfoPrimitiveType(primTypeChar)) => 4 - rule #elemSize(TYPEINFO) => #bitWidth(#intTypeOf(TYPEINFO)) /Int 8 + rule #elemSize(_, typeInfoPrimitiveType(primTypeChar)) => 4 + rule #elemSize(_, TYPEINFO) => #bitWidth(#intTypeOf(TYPEINFO)) /Int 8 requires #isIntType(TYPEINFO) // Floating-point sizes - rule #elemSize(typeInfoPrimitiveType(primTypeFloat(floatTyF16))) => 2 - rule #elemSize(typeInfoPrimitiveType(primTypeFloat(floatTyF32))) => 4 - rule #elemSize(typeInfoPrimitiveType(primTypeFloat(floatTyF64))) => 8 - rule #elemSize(typeInfoPrimitiveType(primTypeFloat(floatTyF128))) => 16 + rule #elemSize(_, typeInfoPrimitiveType(primTypeFloat(floatTyF16))) => 2 + rule #elemSize(_, typeInfoPrimitiveType(primTypeFloat(floatTyF32))) => 4 + rule #elemSize(_, typeInfoPrimitiveType(primTypeFloat(floatTyF64))) => 8 + rule #elemSize(_, typeInfoPrimitiveType(primTypeFloat(floatTyF128))) => 16 // `str` is unsized; size only known with metadata (e.g., in fat pointers) - rule #elemSize(typeInfoPrimitiveType(primTypeStr)) => 0 + rule #elemSize(_, typeInfoPrimitiveType(primTypeStr)) => 0 - // ---- Arrays and slices ---- - rule #elemSize(typeInfoArrayType(ELEM_TY, someTyConst(tyConst(LEN, _)))) - => #elemSize(lookupTy(ELEM_TY)) *Int readTyConstInt(LEN) // Slice `[T]` has dynamic size; plain value is unsized - rule #elemSize(typeInfoArrayType(_ELEM_TY, noTyConst)) => 0 + rule #elemSize(_, typeInfoArrayType(_ELEM_TY, noTyConst)) => 0 // ---- thin and fat pointers ---- - rule #elemSize(typeInfoRefType(TY)) => #elemSize(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) - requires dynamicSize(1) ==K #metadataSize(TY) - rule #elemSize(typeInfoRefType(_)) => 2 *Int #elemSize(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) + rule #elemSize(TYPESMAP, typeInfoRefType(TY)) => #elemSize(TYPESMAP, typeInfoPrimitiveType(primTypeUint(uintTyUsize))) + requires dynamicSize(1) ==K #metadataSize(TYPESMAP, TY) + rule #elemSize(TYPESMAP, typeInfoRefType(_)) => 2 *Int #elemSize(TYPESMAP, typeInfoPrimitiveType(primTypeUint(uintTyUsize))) [owise] - rule #elemSize(typeInfoPtrType(TY)) => #elemSize(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) - requires dynamicSize(1) ==K #metadataSize(TY) - rule #elemSize(typeInfoPtrType(_)) => 2 *Int #elemSize(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) + rule #elemSize(TYPESMAP, typeInfoPtrType(TY)) => #elemSize(TYPESMAP, typeInfoPrimitiveType(primTypeUint(uintTyUsize))) + requires dynamicSize(1) ==K #metadataSize(TYPESMAP, TY) + rule #elemSize(TYPESMAP, typeInfoPtrType(_)) => 2 *Int #elemSize(TYPESMAP, typeInfoPrimitiveType(primTypeUint(uintTyUsize))) [owise] // ---- Tuples ---- - rule #elemSize(typeInfoTupleType(_TYS, someLayoutShape(layoutShape(_, _, _, _, SIZE)))) => #msBytes(SIZE) - rule #elemSize(typeInfoTupleType(.Tys, noLayoutShape)) => 0 - rule #elemSize(typeInfoTupleType(TY TYS, noLayoutShape)) - => #elemSize(lookupTy(TY)) +Int #elemSize(typeInfoTupleType(TYS, noLayoutShape)) + rule #elemSize(_, typeInfoTupleType(_TYS, someLayoutShape(layoutShape(_, _, _, _, SIZE)))) => #msBytes(SIZE) + rule #elemSize(_, typeInfoTupleType(.Tys, noLayoutShape)) => 0 // ---- Structs and Enums with layout ---- - rule #elemSize(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, SIZE)))) => #msBytes(SIZE) - rule #elemSize(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, SIZE)))) => #msBytes(SIZE) + rule #elemSize(_, typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, SIZE)))) => #msBytes(SIZE) + rule #elemSize(_, typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, SIZE)))) => #msBytes(SIZE) // ---- Function item types ---- // Function items are zero-sized; function pointers are handled by PtrType - rule #elemSize(typeInfoFunType(_)) => 0 + rule #elemSize(_, typeInfoFunType(_)) => 0 - rule #elemSize(typeInfoVoidType) => 0 + rule #elemSize(_, typeInfoVoidType) => 0 // Fallback to keep the function total for any remaining cases - rule #elemSize(_) => 0 [owise] + rule #elemSize(_, _) => 0 [owise] - rule 0 <=Int #elemSize(_) => true [simplification, preserves-definedness] + rule 0 <=Int #elemSize(_, _) => true [simplification, preserves-definedness] +``` + +Rules that differ between concrete and symbolic execution (array and tuple element lookups): + +```{.k .concrete} + rule #elemSize(TYPESMAP, typeInfoArrayType(ELEM_TY, someTyConst(tyConst(LEN, _)))) + => #elemSize(TYPESMAP, lookupTy(TYPESMAP, ELEM_TY)) *Int readTyConstInt(TYPESMAP, LEN) + + rule #elemSize(TYPESMAP, typeInfoTupleType(TY TYS, noLayoutShape)) + => #elemSize(TYPESMAP, lookupTy(TYPESMAP, TY)) +Int #elemSize(TYPESMAP, typeInfoTupleType(TYS, noLayoutShape)) +``` + +```{.k .symbolic} + rule #elemSize(_, typeInfoArrayType(ELEM_TY, someTyConst(tyConst(LEN, _)))) + => #elemSize(noMap, lookupTyKore(ELEM_TY)) *Int readTyConstInt(noMap, LEN) + + rule #elemSize(_, typeInfoTupleType(TY TYS, noLayoutShape)) + => #elemSize(noMap, lookupTyKore(TY)) +Int #elemSize(noMap, typeInfoTupleType(TYS, noLayoutShape)) ``` @@ -217,7 +286,7 @@ Enum decoding is for now restricted to a few special cases. If there are no fields, the enum can be decoded by using their data as the discriminant. ```k - rule #decodeValue( + rule #decodeValue(_, BYTES , typeInfoEnumType(... name: _ @@ -307,7 +376,7 @@ per-variant layout offsets. ```k // General entry rule: direct-tag enum with at least one field somewhere. - rule #decodeValue( + rule #decodeValue(TYPESMAP, BYTES , typeInfoEnumType(... name: _ @@ -338,6 +407,7 @@ per-variant layout offsets. ) #as ENUM_TYPE ) => #decodeEnumDirectFields( + TYPESMAP, BYTES, #findVariantIdx(#decodeEnumDirectTag(BYTES, TAG_WIDTH), DISCRIMINANTS), FIELD_TYPESS, @@ -349,20 +419,38 @@ per-variant layout offsets. // --------------------------------------------------------------------------- // #decodeEnumDirectFields: given the variant index, decode its fields // --------------------------------------------------------------------------- - syntax Evaluation ::= #decodeEnumDirectFields ( Bytes , VariantIdx , Tyss , LayoutShapes , TypeInfo ) [function, total, no-evaluators] - // -------------------------------------------------------------------------------------------------------------------------- - rule #decodeEnumDirectFields(BYTES, variantIdx(IDX), FIELD_TYPESS, VARIANT_LAYOUTS, _ENUM_TYPE) +``` + +```{.k .concrete} + syntax Evaluation ::= #decodeEnumDirectFields ( MaybeMap , Bytes , VariantIdx , Tyss , LayoutShapes , TypeInfo ) [function, total] + rule #decodeEnumDirectFields(TYPESMAP, BYTES, variantIdx(IDX), FIELD_TYPESS, VARIANT_LAYOUTS, _ENUM_TYPE) => Aggregate( variantIdx(IDX), - #decodeFieldsWithOffsets(BYTES, #nthTys(FIELD_TYPESS, IDX), #nthVariantOffsets(VARIANT_LAYOUTS, IDX)) + #decodeFieldsWithOffsets(TYPESMAP, BYTES, #nthTys(FIELD_TYPESS, IDX), #nthVariantOffsets(VARIANT_LAYOUTS, IDX)) ) requires 0 <=Int IDX [preserves-definedness] +``` +```{.k .symbolic} + syntax Evaluation ::= #decodeEnumDirectFields ( MaybeMap , Bytes , VariantIdx , Tyss , LayoutShapes , TypeInfo ) [function, total, no-evaluators] + rule #decodeEnumDirectFields(_, BYTES, variantIdx(IDX), FIELD_TYPESS, VARIANT_LAYOUTS, _ENUM_TYPE) + => Aggregate( + variantIdx(IDX), + #decodeFieldsWithOffsets(noMap, BYTES, #nthTys(FIELD_TYPESS, IDX), #nthVariantOffsets(VARIANT_LAYOUTS, IDX)) + ) + requires 0 <=Int IDX + [preserves-definedness] +``` + +```k // Error cases: variant not found or other failure - rule #decodeEnumDirectFields(BYTES, _, _FIELD_TYPESS, _VARIANT_LAYOUTS, ENUM_TYPE) + rule #decodeEnumDirectFields(_, BYTES, _, _FIELD_TYPESS, _VARIANT_LAYOUTS, ENUM_TYPE) => UnableToDecode(BYTES, ENUM_TYPE) [owise] +``` + +```k // --------------------------------------------------------------------------- // #decodeEnumDirectTag: read the tag bytes as an unsigned little-endian int @@ -406,7 +494,7 @@ However, in this case only a `None` can actually be decoded. Any pointer or reference would have a very different encoding in KMIR, not a non-zero address. ```k - rule #decodeValue( + rule #decodeValue(_, BYTES , typeInfoEnumType(... name: _ @@ -457,34 +545,57 @@ The byte consumption approach allows for validation - if there are surplus bytes bytes for the declared array length, the function will get stuck rather than produce incorrect results. -```k - syntax Value ::= #decodeArrayAllocation ( Bytes, TypeInfo, Int ) [function, no-evaluators] - // bytes, element type info, array length, type map (for recursion) +```{.k .concrete} + syntax Value ::= #decodeArrayAllocation ( MaybeMap, Bytes, TypeInfo, Int ) [function] + rule #decodeArrayAllocation(TYPESMAP, BYTES, ELEMTYPEINFO, LEN) + => Range(#decodeArrayElements(TYPESMAP, BYTES, ELEMTYPEINFO, LEN, .List)) - rule #decodeArrayAllocation(BYTES, ELEMTYPEINFO, LEN) - => Range(#decodeArrayElements(BYTES, ELEMTYPEINFO, LEN, .List)) - - syntax List ::= #decodeArrayElements ( Bytes, TypeInfo, Int, List ) [function, no-evaluators] - // bytes, elem type info, remaining length, accumulated list - - rule #decodeArrayElements(BYTES, _ELEMTYPEINFO, LEN, ACC) - => ACC - requires LEN <=Int 0 - andBool lengthBytes(BYTES) ==Int 0 // exact match - no surplus bytes + syntax List ::= #decodeArrayElements ( MaybeMap, Bytes, TypeInfo, Int, List ) [function] + // type map, bytes, elem type info, remaining length, accumulated list + rule #decodeArrayElements(TYPESMAP, BYTES, ELEMTYPEINFO, LEN, ACC) + => #decodeArrayElements( + TYPESMAP, + substrBytes(BYTES, #elemSize(TYPESMAP, ELEMTYPEINFO), lengthBytes(BYTES)), + ELEMTYPEINFO, + LEN -Int 1, + ACC ListItem(#decodeValue(TYPESMAP, + substrBytes(BYTES, 0, #elemSize(TYPESMAP, ELEMTYPEINFO)), + ELEMTYPEINFO + )) + ) + requires LEN >Int 0 + andBool lengthBytes(BYTES) >=Int #elemSize(TYPESMAP, ELEMTYPEINFO) // enough bytes remaining [preserves-definedness] +``` - rule #decodeArrayElements(BYTES, ELEMTYPEINFO, LEN, ACC) +```{.k .symbolic} + syntax Value ::= #decodeArrayAllocation ( MaybeMap, Bytes, TypeInfo, Int ) [function, no-evaluators] + rule #decodeArrayAllocation(_, BYTES, ELEMTYPEINFO, LEN) + => Range(#decodeArrayElements(noMap, BYTES, ELEMTYPEINFO, LEN, .List)) + + syntax List ::= #decodeArrayElements ( MaybeMap, Bytes, TypeInfo, Int, List ) [function, no-evaluators] + // type map, bytes, elem type info, remaining length, accumulated list + rule #decodeArrayElements(_, BYTES, ELEMTYPEINFO, LEN, ACC) => #decodeArrayElements( - substrBytes(BYTES, #elemSize(ELEMTYPEINFO), lengthBytes(BYTES)), + noMap, + substrBytes(BYTES, #elemSize(noMap, ELEMTYPEINFO), lengthBytes(BYTES)), ELEMTYPEINFO, LEN -Int 1, - ACC ListItem(#decodeValue( - substrBytes(BYTES, 0, #elemSize(ELEMTYPEINFO)), + ACC ListItem(#decodeValue(noMap, + substrBytes(BYTES, 0, #elemSize(noMap, ELEMTYPEINFO)), ELEMTYPEINFO )) ) requires LEN >Int 0 - andBool lengthBytes(BYTES) >=Int #elemSize(ELEMTYPEINFO) // enough bytes remaining + andBool lengthBytes(BYTES) >=Int #elemSize(noMap, ELEMTYPEINFO) // enough bytes remaining + [preserves-definedness] +``` + +```k + rule #decodeArrayElements(_, BYTES, _ELEMTYPEINFO, LEN, ACC) + => ACC + requires LEN <=Int 0 + andBool lengthBytes(BYTES) ==Int 0 // exact match - no surplus bytes [preserves-definedness] ``` @@ -494,19 +605,35 @@ Slices are arrays with dynamic length. The `#decodeSliceAllocation` function computes the array length by dividing the total byte length by the element size, then uses the same element-by-element decoding approach as arrays. -```k - syntax Value ::= #decodeSliceAllocation ( Bytes, TypeInfo ) [function, no-evaluators] - // ------------------------------------------------------------------- - rule #decodeSliceAllocation(BYTES, ELEMTYPEINFO) +```{.k .concrete} + syntax Value ::= #decodeSliceAllocation ( MaybeMap, Bytes, TypeInfo ) [function] + rule #decodeSliceAllocation(TYPESMAP, BYTES, ELEMTYPEINFO) + => Range(#decodeArrayElements( + TYPESMAP, + BYTES, + ELEMTYPEINFO, + lengthBytes(BYTES) /Int #elemSize(TYPESMAP, ELEMTYPEINFO), + .List + ) + ) + requires lengthBytes(BYTES) %Int #elemSize(TYPESMAP, ELEMTYPEINFO) ==Int 0 + andBool 0 Range(#decodeArrayElements( + noMap, BYTES, ELEMTYPEINFO, - lengthBytes(BYTES) /Int #elemSize(ELEMTYPEINFO), + lengthBytes(BYTES) /Int #elemSize(noMap, ELEMTYPEINFO), .List ) ) - requires lengthBytes(BYTES) %Int #elemSize(ELEMTYPEINFO) ==Int 0 // element size divides cleanly - andBool 0 #pointeeProjection(TYPESMAP, lookupTy(TYPESMAP, TY1), lookupTy(TYPESMAP, TY2)) + rule #typeProjection ( _, _, _ ) => NoProjectionElems [owise] +``` - syntax MaybeProjectionElems ::= #typeProjection ( TypeInfo , TypeInfo ) [function, total, no-evaluators] - // --------------------------------------------------------------------------------------- - rule #typeProjection ( typeInfoPtrType(TY1) , typeInfoPtrType(TY2) ) => #pointeeProjection(lookupTy(TY1), lookupTy(TY2)) - rule #typeProjection ( _, _ ) => NoProjectionElems [owise] +```{.k .symbolic} + syntax MaybeProjectionElems ::= #typeProjection ( MaybeMap , TypeInfo , TypeInfo ) [function, total, no-evaluators] + rule #typeProjection ( _, typeInfoPtrType(TY1), typeInfoPtrType(TY2) ) => #pointeeProjection(noMap, lookupTyKore(TY1), lookupTyKore(TY2)) + rule #typeProjection ( _, _, _ ) => NoProjectionElems [owise] ``` Note that certain projections can cancel each other, such as casting from one transparent wrapper to another. @@ -81,22 +88,26 @@ attempting to unwrap the target type. This eliminates non-deterministic overlap and target-side rules, because a type cannot be both a struct and an array simultaneously. When the source cannot be unwrapped further, target-side unwrapping is handled by `#pointeeProjectionTarget`. -```k - syntax MaybeProjectionElems ::= #pointeeProjection ( TypeInfo , TypeInfo ) [function, total, no-evaluators] +```{.k .concrete} + syntax MaybeProjectionElems ::= #pointeeProjection ( MaybeMap , TypeInfo , TypeInfo ) [function, total] +``` + +```{.k .symbolic} + syntax MaybeProjectionElems ::= #pointeeProjection ( MaybeMap , TypeInfo , TypeInfo ) [function, total, no-evaluators] ``` A short-cut rule for identical types takes preference. ```k - rule #pointeeProjection(T , T) => .ProjectionElems [priority(40)] + rule #pointeeProjection(_, T , T) => .ProjectionElems [priority(40)] ``` Pointers to zero-sized types can be converted from and to. No recursion beyond the ZST. **TODO** Problem: our ZSTs have different representation: compare empty arrays and empty structs/unit tuples. ```k - rule #pointeeProjection(SRC, OTHER) => projectionElemToZST .ProjectionElems + rule #pointeeProjection(_, SRC, OTHER) => projectionElemToZST .ProjectionElems requires #zeroSizedType(OTHER) andBool notBool #zeroSizedType(SRC) [priority(45)] - rule #pointeeProjection(SRC, OTHER) => projectionElemFromZST .ProjectionElems + rule #pointeeProjection(_, SRC, OTHER) => projectionElemFromZST .ProjectionElems requires #zeroSizedType(SRC) andBool notBool #zeroSizedType(OTHER) [priority(45)] ``` @@ -105,28 +116,53 @@ Source-side: unwrap structs and arrays from the source type first. When source is an array and target is a transparent wrapper whose inner type equals the source, the source should be wrapped rather than unwrapped (e.g., `*const [u8;2] → *const Wrapper([u8;2])`). -```k - rule #pointeeProjection(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER) +```{.k .concrete} + rule #pointeeProjection(TYPESMAP, typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER) => maybeConcatProj( projectionElemField(fieldIdx(0), FIELD), - #pointeeProjection(lookupTy(FIELD), OTHER) + #pointeeProjection(TYPESMAP, lookupTy(TYPESMAP, FIELD), OTHER) ) requires #zeroFieldOffset(LAYOUT) - rule #pointeeProjection(SRC:TypeInfo, typeInfoStructType(_NAME, _ADTDEF, FIELD .Tys, LAYOUT)) + rule #pointeeProjection(TYPESMAP, SRC:TypeInfo, typeInfoStructType(_NAME, _ADTDEF, FIELD .Tys, LAYOUT)) => maybeConcatProj( projectionElemWrapStruct, - #pointeeProjection(SRC, lookupTy(FIELD)) + #pointeeProjection(TYPESMAP, SRC, lookupTy(TYPESMAP, FIELD)) ) requires #isArrayType(SRC) andBool #zeroFieldOffset(LAYOUT) - andBool lookupTy(FIELD) ==K SRC + andBool lookupTy(TYPESMAP, FIELD) ==K SRC [priority(42)] - rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2) + rule #pointeeProjection(TYPESMAP, typeInfoArrayType(TY1, _), TY2) => maybeConcatProj( projectionElemConstantIndex(0, 0, false), - #pointeeProjection(lookupTy(TY1), TY2) + #pointeeProjection(TYPESMAP, lookupTy(TYPESMAP, TY1), TY2) + ) +``` + +```{.k .symbolic} + rule #pointeeProjection(_, typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER) + => maybeConcatProj( + projectionElemField(fieldIdx(0), FIELD), + #pointeeProjection(noMap, lookupTyKore(FIELD), OTHER) + ) + requires #zeroFieldOffset(LAYOUT) + + rule #pointeeProjection(_, SRC:TypeInfo, typeInfoStructType(_NAME, _ADTDEF, FIELD .Tys, LAYOUT)) + => maybeConcatProj( + projectionElemWrapStruct, + #pointeeProjection(noMap, SRC, lookupTyKore(FIELD)) + ) + requires #isArrayType(SRC) + andBool #zeroFieldOffset(LAYOUT) + andBool lookupTyKore(FIELD) ==K SRC + [priority(42)] + + rule #pointeeProjection(_, typeInfoArrayType(TY1, _), TY2) + => maybeConcatProj( + projectionElemConstantIndex(0, 0, false), + #pointeeProjection(noMap, lookupTyKore(TY1), TY2) ) ``` @@ -135,45 +171,77 @@ This is actually a 2-step compatibility: The `MaybeUninit` union contains a `ManuallyDrop` (when filled), which is a singleton struct (see above). -```k - rule #pointeeProjection(MAYBEUNINIT_TYINFO, ELEM_TYINFO) +```{.k .concrete} + rule #pointeeProjection(TYPESMAP, MAYBEUNINIT_TYINFO, ELEM_TYINFO) => maybeConcatProj( projectionElemField(fieldIdx(1), {getFieldTy(MAYBEUNINIT_TYINFO, 1)}:>Ty), maybeConcatProj( - projectionElemField(fieldIdx(0), {getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)}:>Ty), + projectionElemField(fieldIdx(0), {getFieldTy(#lookupMaybeTy(TYPESMAP, getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)}:>Ty), .ProjectionElems // TODO recursion? ) ) requires #typeNameIs(MAYBEUNINIT_TYINFO, "std::mem::MaybeUninit<") - andBool #lookupMaybeTy(getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)) ==K ELEM_TYINFO + andBool #lookupMaybeTy(TYPESMAP, getFieldTy(#lookupMaybeTy(TYPESMAP, getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)) ==K ELEM_TYINFO +``` + +```{.k .symbolic} + rule #pointeeProjection(_, MAYBEUNINIT_TYINFO, ELEM_TYINFO) + => maybeConcatProj( + projectionElemField(fieldIdx(1), {getFieldTy(MAYBEUNINIT_TYINFO, 1)}:>Ty), + maybeConcatProj( + projectionElemField(fieldIdx(0), {getFieldTy(#lookupMaybeTy(noMap, getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)}:>Ty), + .ProjectionElems // TODO recursion? + ) + ) + requires #typeNameIs(MAYBEUNINIT_TYINFO, "std::mem::MaybeUninit<") + andBool #lookupMaybeTy(noMap, getFieldTy(#lookupMaybeTy(noMap, getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)) ==K ELEM_TYINFO ``` Fallback: source is not unwrappable, delegate to target-side. ```k - rule #pointeeProjection(SRC, TGT) => #pointeeProjectionTarget(SRC, TGT) [owise] + rule #pointeeProjection(TYPESMAP, SRC, TGT) => #pointeeProjectionTarget(TYPESMAP, SRC, TGT) [owise] ``` Target-side fallback: only reached when source cannot be unwrapped further. After one step of target unwrapping, recurse back to `#pointeeProjection` to maintain the source-first strategy. -```k - syntax MaybeProjectionElems ::= #pointeeProjectionTarget ( TypeInfo , TypeInfo ) [function, total, no-evaluators] +```{.k .concrete} + syntax MaybeProjectionElems ::= #pointeeProjectionTarget ( MaybeMap , TypeInfo , TypeInfo ) [function, total] + + rule #pointeeProjectionTarget(TYPESMAP, TY1, typeInfoArrayType(TY2, _)) + => maybeConcatProj( + projectionElemSingletonArray, + #pointeeProjection(TYPESMAP, TY1, lookupTy(TYPESMAP, TY2)) + ) + + rule #pointeeProjectionTarget(TYPESMAP, OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) + => maybeConcatProj( + projectionElemWrapStruct, + #pointeeProjection(TYPESMAP, OTHER, lookupTy(TYPESMAP, FIELD)) + ) + requires #zeroFieldOffset(LAYOUT) +``` + +```{.k .symbolic} + syntax MaybeProjectionElems ::= #pointeeProjectionTarget ( MaybeMap , TypeInfo , TypeInfo ) [function, total, no-evaluators] - rule #pointeeProjectionTarget(TY1, typeInfoArrayType(TY2, _)) + rule #pointeeProjectionTarget(_, TY1, typeInfoArrayType(TY2, _)) => maybeConcatProj( projectionElemSingletonArray, - #pointeeProjection(TY1, lookupTy(TY2)) + #pointeeProjection(noMap, TY1, lookupTyKore(TY2)) ) - rule #pointeeProjectionTarget(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) + rule #pointeeProjectionTarget(_, OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) => maybeConcatProj( projectionElemWrapStruct, - #pointeeProjection(OTHER, lookupTy(FIELD)) + #pointeeProjection(noMap, OTHER, lookupTyKore(FIELD)) ) requires #zeroFieldOffset(LAYOUT) +``` - rule #pointeeProjectionTarget(_, _) => NoProjectionElems [owise] +```k + rule #pointeeProjectionTarget(_, _, _) => NoProjectionElems [owise] ``` ```k @@ -250,35 +318,70 @@ To make this function total, an optional `MaybeTy` is used. rule getArrayElemTy(typeInfoArrayType(ELEM_TY, _)) => ELEM_TY rule getArrayElemTy(_) => ty(-1) [owise] - syntax TypeInfo ::= getArrayElemTypeInfo ( TypeInfo ) [function, total, no-evaluators] - // -------------------------------------------------------------------- - rule getArrayElemTypeInfo(typeInfoArrayType(ELEM_TY, _)) => lookupTy(ELEM_TY) - rule getArrayElemTypeInfo(_) => typeInfoVoidType [owise] +``` + +```{.k .concrete} + syntax TypeInfo ::= getArrayElemTypeInfo ( MaybeMap , TypeInfo ) [function, total] + rule getArrayElemTypeInfo(TYPESMAP, typeInfoArrayType(ELEM_TY, _)) => lookupTy(TYPESMAP, ELEM_TY) + + syntax TypeInfo ::= #lookupMaybeTy ( MaybeMap , MaybeTy ) [function, total] + rule #lookupMaybeTy(TYPESMAP, TY:Ty) => lookupTy(TYPESMAP, TY) +``` - syntax TypeInfo ::= #lookupMaybeTy ( MaybeTy ) [function, total, no-evaluators] - // ------------------------------------------------------------- - rule #lookupMaybeTy(TY:Ty) => lookupTy(TY) - rule #lookupMaybeTy(TyUnknown) => typeInfoVoidType +```{.k .symbolic} + syntax TypeInfo ::= getArrayElemTypeInfo ( MaybeMap , TypeInfo ) [function, total, no-evaluators] + rule getArrayElemTypeInfo(_, typeInfoArrayType(ELEM_TY, _)) => lookupTyKore(ELEM_TY) - syntax MaybeTy ::= getTyOf( MaybeTy , ProjectionElems ) [function, total, no-evaluators] + syntax TypeInfo ::= #lookupMaybeTy ( MaybeMap , MaybeTy ) [function, total, no-evaluators] + rule #lookupMaybeTy(_, TY:Ty) => lookupTyKore(TY) +``` + +```k + rule getArrayElemTypeInfo(_, _) => typeInfoVoidType [owise] + rule #lookupMaybeTy(_, TyUnknown) => typeInfoVoidType +``` + +```{.k .concrete} + syntax MaybeTy ::= getTyOf( MaybeMap , MaybeTy , ProjectionElems ) [function, total] // ---------------------------------------------------------------------- - rule getTyOf(TyUnknown, _ ) => TyUnknown - rule getTyOf(TY, .ProjectionElems ) => TY + rule getTyOf(TYPESMAP, TY, projectionElemDeref PROJS ) => getTyOf(TYPESMAP, pointeeTy(lookupTy(TYPESMAP, TY)), PROJS) + rule getTyOf(TYPESMAP, _, projectionElemField(_, TY) PROJS ) => getTyOf(TYPESMAP, TY, PROJS) - rule getTyOf(TY, projectionElemDeref PROJS ) => getTyOf(pointeeTy(lookupTy(TY)), PROJS) - rule getTyOf( _, projectionElemField(_, TY) PROJS ) => getTyOf(TY, PROJS) // could also look it up - - rule getTyOf(TY, projectionElemIndex(_) PROJS) => getTyOf(elemTy(lookupTy(TY)), PROJS) - rule getTyOf(TY, projectionElemConstantIndex(_, _, _) PROJS) => getTyOf(elemTy(lookupTy(TY)), PROJS) - rule getTyOf(TY, projectionElemSubslice(_, _, _) PROJS) => getTyOf(TY, PROJS) // TODO assumes TY is already a slice type + rule getTyOf(TYPESMAP, TY, projectionElemIndex(_) PROJS) => getTyOf(TYPESMAP, elemTy(lookupTy(TYPESMAP, TY)), PROJS) + rule getTyOf(TYPESMAP, TY, projectionElemConstantIndex(_, _, _) PROJS) => getTyOf(TYPESMAP, elemTy(lookupTy(TYPESMAP, TY)), PROJS) + rule getTyOf(TYPESMAP, TY, projectionElemSubslice(_, _, _) PROJS) => getTyOf(TYPESMAP, TY, PROJS) // TODO assumes TY is already a slice type - rule getTyOf(TY, projectionElemDowncast(_) PROJS) => getTyOf(TY, PROJS) // unchanged type, just setting variantIdx + rule getTyOf(TYPESMAP, TY, projectionElemDowncast(_) PROJS) => getTyOf(TYPESMAP, TY, PROJS) - rule getTyOf( _, projectionElemOpaqueCast(TY) PROJS) => getTyOf(TY, PROJS) + rule getTyOf(TYPESMAP, _, projectionElemOpaqueCast(TY) PROJS) => getTyOf(TYPESMAP, TY, PROJS) - rule getTyOf( _, projectionElemSubtype(TY) PROJS) => getTyOf(TY, PROJS) - // ----------------------------------------------------------- - rule getTyOf(_, _) => TyUnknown [owise] + rule getTyOf(TYPESMAP, _, projectionElemSubtype(TY) PROJS) => getTyOf(TYPESMAP, TY, PROJS) +``` + +```{.k .symbolic} + syntax MaybeTy ::= getTyOf( MaybeMap , MaybeTy , ProjectionElems ) [function, total, no-evaluators] + // ---------------------------------------------------------------------- + rule getTyOf(_, TY, projectionElemDeref PROJS ) => getTyOf(noMap, pointeeTy(lookupTyKore(TY)), PROJS) + rule getTyOf(_, _, projectionElemField(_, TY) PROJS ) => getTyOf(noMap, TY, PROJS) + + rule getTyOf(_, TY, projectionElemIndex(_) PROJS) => getTyOf(noMap, elemTy(lookupTyKore(TY)), PROJS) + rule getTyOf(_, TY, projectionElemConstantIndex(_, _, _) PROJS) => getTyOf(noMap, elemTy(lookupTyKore(TY)), PROJS) + rule getTyOf(_, TY, projectionElemSubslice(_, _, _) PROJS) => getTyOf(noMap, TY, PROJS) // TODO assumes TY is already a slice type + + rule getTyOf(_, TY, projectionElemDowncast(_) PROJS) => getTyOf(noMap, TY, PROJS) + + rule getTyOf(_, _, projectionElemOpaqueCast(TY) PROJS) => getTyOf(noMap, TY, PROJS) + + rule getTyOf(_, _, projectionElemSubtype(TY) PROJS) => getTyOf(noMap, TY, PROJS) +``` + +```k + rule getTyOf(_, TyUnknown, _ ) => TyUnknown + rule getTyOf(_, TY, .ProjectionElems ) => TY + rule getTyOf(_, _, _) => TyUnknown [owise] +``` + +```k syntax MaybeTy ::= pointeeTy ( TypeInfo ) [function, total] @@ -302,34 +405,68 @@ NB that the need for metadata is determined for the _pointee_ type, not the poin A [similar function exists in `rustc`](https://doc.rust-lang.org/nightly/nightly-rustc/src/rustc_middle/ty/util.rs.html#224-235) to determine whether or not a type needs dynamic metadata. Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does not. -```k - syntax MetadataSize ::= #metadataSize ( Ty , ProjectionElems ) [function, total, no-evaluators] - | #metadataSize ( MaybeTy ) [function, total, no-evaluators] - | #metadataSizeAux ( TypeInfo ) [function, total, no-evaluators] +```{.k .concrete} + syntax MetadataSize ::= #metadataSize ( MaybeMap , Ty , ProjectionElems ) [function, total] + | #metadataSize ( MaybeMap , MaybeTy ) [function, total] // -------------------------------------------------------------------------------------- - rule #metadataSize(TY, PROJS) => #metadataSize(getTyOf(TY, PROJS)) + rule #metadataSize(TYPESMAP, TY, PROJS) => #metadataSize(TYPESMAP, getTyOf(TYPESMAP, TY, PROJS)) + rule #metadataSize(TYPESMAP, TY) => #metadataSizeAux(TYPESMAP, lookupTy(TYPESMAP, TY)) +``` - rule #metadataSize(TyUnknown) => noMetadataSize - rule #metadataSize(TY) => #metadataSizeAux(lookupTy(TY)) +```{.k .symbolic} + syntax MetadataSize ::= #metadataSize ( MaybeMap , Ty , ProjectionElems ) [function, total, no-evaluators] + | #metadataSize ( MaybeMap , MaybeTy ) [function, total, no-evaluators] + // -------------------------------------------------------------------------------------- + rule #metadataSize(_, TY, PROJS) => #metadataSize(noMap, getTyOf(noMap, TY, PROJS)) + rule #metadataSize(_, TY) => #metadataSizeAux(noMap, lookupTyKore(TY)) +``` + +```k + rule #metadataSize(_, TyUnknown) => noMetadataSize +``` - rule #metadataSizeAux(typeInfoArrayType(_, noTyConst )) => dynamicSize(1) - rule #metadataSizeAux(typeInfoArrayType(_, someTyConst(tyConst(CONST, _)))) => staticSize(readTyConstInt(CONST)) - rule #metadataSizeAux( _OTHER ) => noMetadataSize [owise] +```{.k .concrete} + syntax MetadataSize ::= #metadataSizeAux ( MaybeMap , TypeInfo ) [function, total] + rule #metadataSizeAux(TYPESMAP, typeInfoArrayType(_, someTyConst(tyConst(CONST, _)))) => staticSize(readTyConstInt(TYPESMAP, CONST)) ``` +```{.k .symbolic} + syntax MetadataSize ::= #metadataSizeAux ( MaybeMap , TypeInfo ) [function, total, no-evaluators] + rule #metadataSizeAux(_, typeInfoArrayType(_, someTyConst(tyConst(CONST, _)))) => staticSize(readTyConstInt(noMap, CONST)) +``` ```k + rule #metadataSizeAux(_, typeInfoArrayType(_, noTyConst )) => dynamicSize(1) + rule #metadataSizeAux(_, _OTHER ) => noMetadataSize [owise] +``` + + +```{.k .concrete} // reading Int-valued TyConsts from allocated bytes - syntax Int ::= readTyConstInt ( TyConstKind ) [function, no-evaluators] + syntax Int ::= readTyConstInt ( MaybeMap , TyConstKind ) [function] // ----------------------------------------------------------- - rule readTyConstInt( tyConstKindValue(TY, allocation(BYTES, _, _, _))) => Bytes2Int(BYTES, LE, Unsigned) - requires isUintTy(#numTypeOf(lookupTy(TY))) - andBool lengthBytes(BYTES) ==Int #bitWidth(#numTypeOf(lookupTy(TY))) /Int 8 + rule readTyConstInt( TYPESMAP, tyConstKindValue(TY, allocation(BYTES, _, _, _))) => Bytes2Int(BYTES, LE, Unsigned) + requires isUintTy(#numTypeOf(lookupTy(TYPESMAP, TY))) + andBool lengthBytes(BYTES) ==Int #bitWidth(#numTypeOf(lookupTy(TYPESMAP, TY))) /Int 8 + [preserves-definedness] + + rule readTyConstInt( TYPESMAP, tyConstKindValue(TY, allocation(BYTES, _, _, _))) => Bytes2Int(BYTES, LE, Signed ) + requires isIntTy(#numTypeOf(lookupTy(TYPESMAP, TY))) + andBool lengthBytes(BYTES) ==Int #bitWidth(#numTypeOf(lookupTy(TYPESMAP, TY))) /Int 8 + [preserves-definedness] +``` + +```{.k .symbolic} + syntax Int ::= readTyConstInt ( MaybeMap , TyConstKind ) [function, no-evaluators] + + rule readTyConstInt( _, tyConstKindValue(TY, allocation(BYTES, _, _, _))) => Bytes2Int(BYTES, LE, Unsigned) + requires isUintTy(#numTypeOf(lookupTyKore(TY))) + andBool lengthBytes(BYTES) ==Int #bitWidth(#numTypeOf(lookupTyKore(TY))) /Int 8 [preserves-definedness] - rule readTyConstInt( tyConstKindValue(TY, allocation(BYTES, _, _, _))) => Bytes2Int(BYTES, LE, Signed ) - requires isIntTy(#numTypeOf(lookupTy(TY))) - andBool lengthBytes(BYTES) ==Int #bitWidth(#numTypeOf(lookupTy(TY))) /Int 8 + rule readTyConstInt( _, tyConstKindValue(TY, allocation(BYTES, _, _, _))) => Bytes2Int(BYTES, LE, Signed ) + requires isIntTy(#numTypeOf(lookupTyKore(TY))) + andBool lengthBytes(BYTES) ==Int #bitWidth(#numTypeOf(lookupTyKore(TY))) /Int 8 [preserves-definedness] ``` @@ -354,65 +491,83 @@ Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does The `alignOf` and `sizeOf` nullary operations return the alignment / size in bytes as a `usize`. This information is either hard-wired for primitive types (numbers, first and foremost), or read from the layout in `TypeInfo`. +```{.k .concrete} + syntax Int ::= #sizeOf ( MaybeMap , TypeInfo ) [function, total] + | #alignOf ( MaybeMap , TypeInfo ) [function, total] +``` + +```{.k .symbolic} + syntax Int ::= #sizeOf ( MaybeMap , TypeInfo ) [function, total, no-evaluators] + | #alignOf ( MaybeMap , TypeInfo ) [function, total, no-evaluators] +``` + ```k - syntax Int ::= #sizeOf ( TypeInfo ) [function, total, no-evaluators] - | #alignOf ( TypeInfo ) [function, total, no-evaluators] // primitive int types: use bit width (both for size and alignment) - rule #sizeOf(typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] - rule #alignOf(typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoPrimitiveType(primTypeUint(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] - rule #alignOf(typeInfoPrimitiveType(primTypeUint(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoPrimitiveType(primTypeFloat(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] - rule #alignOf(typeInfoPrimitiveType(primTypeFloat(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] + rule #alignOf(_, typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoPrimitiveType(primTypeUint(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] + rule #alignOf(_, typeInfoPrimitiveType(primTypeUint(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoPrimitiveType(primTypeFloat(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] + rule #alignOf(_, typeInfoPrimitiveType(primTypeFloat(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] // bool and char - rule #sizeOf(typeInfoPrimitiveType(primTypeBool)) => 1 - rule #alignOf(typeInfoPrimitiveType(primTypeBool)) => 1 - rule #sizeOf(typeInfoPrimitiveType(primTypeChar)) => 4 - rule #alignOf(typeInfoPrimitiveType(primTypeChar)) => 4 + rule #sizeOf(_, typeInfoPrimitiveType(primTypeBool)) => 1 + rule #alignOf(_, typeInfoPrimitiveType(primTypeBool)) => 1 + rule #sizeOf(_, typeInfoPrimitiveType(primTypeChar)) => 4 + rule #alignOf(_, typeInfoPrimitiveType(primTypeChar)) => 4 // The str primitive has alignment of a Char but size 0 (indicating dynamic size) - rule #sizeOf(typeInfoPrimitiveType(primTypeStr)) => 0 - rule #alignOf(typeInfoPrimitiveType(primTypeStr)) => 4 + rule #sizeOf(_, typeInfoPrimitiveType(primTypeStr)) => 0 + rule #alignOf(_, typeInfoPrimitiveType(primTypeStr)) => 4 // enums, structs , and tuples provide the values from their layout information - rule #sizeOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoEnumType(_, _, _, _, noLayoutShape)) => 0 - rule #alignOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES - rule #alignOf(typeInfoEnumType(_, _, _, _, noLayoutShape)) => 1 + rule #sizeOf(_, typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoEnumType(_, _, _, _, noLayoutShape)) => 0 + rule #alignOf(_, typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES + rule #alignOf(_, typeInfoEnumType(_, _, _, _, noLayoutShape)) => 1 // struct - rule #sizeOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoStructType(_, _, _, noLayoutShape)) => 0 - rule #alignOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES - rule #alignOf(typeInfoStructType(_, _, _, noLayoutShape)) => 1 + rule #sizeOf(_, typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoStructType(_, _, _, noLayoutShape)) => 0 + rule #alignOf(_, typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES + rule #alignOf(_, typeInfoStructType(_, _, _, noLayoutShape)) => 1 // tuple - rule #sizeOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoTupleType(_, noLayoutShape)) => 0 - rule #alignOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES - rule #alignOf(typeInfoTupleType(_, noLayoutShape)) => 1 + rule #sizeOf(_, typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoTupleType(_, noLayoutShape)) => 0 + rule #alignOf(_, typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES + rule #alignOf(_, typeInfoTupleType(_, noLayoutShape)) => 1 // union - rule #sizeOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness] - rule #sizeOf(typeInfoUnionType(_, _, _, noLayoutShape)) => 0 - rule #alignOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES - rule #alignOf(typeInfoUnionType(_, _, _, noLayoutShape)) => 1 - // arrays with known length have the alignment of the element type, and a size multiplying element count and element size - rule #sizeOf(typeInfoArrayType(ELEM_TY, someTyConst(tyConst(KIND, _)))) => #sizeOf(lookupTy(ELEM_TY)) *Int readTyConstInt(KIND) - rule #sizeOf(typeInfoArrayType( _ , noTyConst )) => 0 - rule #alignOf(typeInfoArrayType(ELEM_TY, _)) => #alignOf(lookupTy(ELEM_TY)) + rule #sizeOf(_, typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness] + rule #sizeOf(_, typeInfoUnionType(_, _, _, noLayoutShape)) => 0 + rule #alignOf(_, typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES + rule #alignOf(_, typeInfoUnionType(_, _, _, noLayoutShape)) => 1 + // arrays with no known length + rule #sizeOf(_, typeInfoArrayType( _ , noTyConst )) => 0 // thin ptr and ref types have the size of `usize` and twice that for fat pointers/refs. Alignment is that of `usize` - rule #sizeOf(typeInfoPtrType(POINTEE_TY)) - => #sizeOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) - *Int (#if #metadataSize(POINTEE_TY) ==K dynamicSize(1) #then 2 #else 1 #fi) - rule #sizeOf(typeInfoRefType(POINTEE_TY)) - => #sizeOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) - *Int (#if #metadataSize(POINTEE_TY) ==K dynamicSize(1) #then 2 #else 1 #fi) - rule #alignOf(typeInfoPtrType(_)) => #alignOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) - rule #alignOf(typeInfoRefType(_)) => #alignOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) + rule #sizeOf(TYPESMAP, typeInfoPtrType(POINTEE_TY)) + => #sizeOf(TYPESMAP, typeInfoPrimitiveType(primTypeUint(uintTyUsize))) + *Int (#if #metadataSize(TYPESMAP, POINTEE_TY) ==K dynamicSize(1) #then 2 #else 1 #fi) + rule #sizeOf(TYPESMAP, typeInfoRefType(POINTEE_TY)) + => #sizeOf(TYPESMAP, typeInfoPrimitiveType(primTypeUint(uintTyUsize))) + *Int (#if #metadataSize(TYPESMAP, POINTEE_TY) ==K dynamicSize(1) #then 2 #else 1 #fi) + rule #alignOf(TYPESMAP, typeInfoPtrType(_)) => #alignOf(TYPESMAP, typeInfoPrimitiveType(primTypeUint(uintTyUsize))) + rule #alignOf(TYPESMAP, typeInfoRefType(_)) => #alignOf(TYPESMAP, typeInfoPrimitiveType(primTypeUint(uintTyUsize))) // other types (fun and void types) have size and alignment 0 - rule #sizeOf(_) => 0 [owise] - rule #alignOf(_) => 0 [owise] + rule #sizeOf(_, _) => 0 [owise] + rule #alignOf(_, _) => 0 [owise] +``` + +Arrays with known length have the alignment of the element type, and a size multiplying element count and element size: + +```{.k .concrete} + rule #sizeOf(TYPESMAP, typeInfoArrayType(ELEM_TY, someTyConst(tyConst(KIND, _)))) => #sizeOf(TYPESMAP, lookupTy(TYPESMAP, ELEM_TY)) *Int readTyConstInt(TYPESMAP, KIND) + rule #alignOf(TYPESMAP, typeInfoArrayType(ELEM_TY, _)) => #alignOf(TYPESMAP, lookupTy(TYPESMAP, ELEM_TY)) +``` + +```{.k .symbolic} + rule #sizeOf(_, typeInfoArrayType(ELEM_TY, someTyConst(tyConst(KIND, _)))) => #sizeOf(noMap, lookupTyKore(ELEM_TY)) *Int readTyConstInt(noMap, KIND) + rule #alignOf(_, typeInfoArrayType(ELEM_TY, _)) => #alignOf(noMap, lookupTyKore(ELEM_TY)) ``` ```k diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index 595facf64..aba74e612 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -13,6 +13,7 @@ module RT-VALUE-SYNTAX imports BODY imports LIB imports MONO + imports MAP ``` ## Values in MIR @@ -136,19 +137,81 @@ The basic operations of reading and writing those values can use K's "heating" a # Static data -These functions are global static data accessed from many places, and will be extended for the particular program. +In symbolic execution (Haskell/booster backend), static data is stored as generated, hardcoded functions that return KORE. +In concrete execution (LLVM backend), it is stored in `Map`s in the configuration. +The `MaybeMap` sort wraps this choice: `someMap(M)` means use map lookups. `noMap` means use generated functions. + +```k + syntax MaybeMap ::= "noMap" [symbol(MaybeMap::noMap)] + | someMap(Map) [symbol(MaybeMap::someMap)] +``` + +## Lookup functions (for symbolic execution) + +These functions are global static data accessed from many places, and will be extended for the particular program. ```k // // function store, Ty -> MonoItemFn - syntax MonoItemKind ::= lookupFunction ( Ty ) [function, total, symbol(lookupFunction), no-evaluators] + syntax MonoItemKind ::= lookupFunctionKore ( Ty ) [function, total, symbol(lookupFunctionKore), no-evaluators] // // static allocations: AllocId -> AllocData (Value or error) - syntax Evaluation ::= lookupAlloc ( AllocId ) [function, total, symbol(lookupAlloc), no-evaluators] + syntax Evaluation ::= lookupAllocKore ( AllocId ) [function, total, symbol(lookupAllocKore), no-evaluators] | InvalidAlloc ( AllocId ) // error marker // // static information about the base type interning in the MIR: Ty -> TypeInfo - syntax TypeInfo ::= lookupTy ( Ty ) [function, total, symbol(lookupTy), no-evaluators] + syntax TypeInfo ::= lookupTyKore ( Ty ) [function, total, symbol(lookupTyKore), no-evaluators] +``` + +## Lookup functions (for concrete execution) + +These functions perform lookups from Maps stored in the configuration, used in concrete execution (LLVM backend). +They return the same defaults as the Kore versions when a key is not found. + +```k + syntax MonoItemKind ::= lookupFunctionMap ( Map , Ty ) [function, total] + rule lookupFunctionMap(M, ty(I)) => {M [ ty(I) ] orDefault monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(I), noBody)}:>MonoItemKind + + syntax TypeInfo ::= lookupTyMap ( Map , Ty ) [function, total] + rule lookupTyMap(M, TY) => {M [ TY ] orDefault typeInfoVoidType}:>TypeInfo + + syntax Evaluation ::= lookupAllocMap ( Map , AllocId ) [function, total] + rule lookupAllocMap(M, AID) => {M [ AID ] orDefault InvalidAlloc(AID)}:>Evaluation +``` + +## Top-level lookup functions + +These dispatch to either the map-based or Kore-based lookup depending on the backend. + +In **concrete execution** (LLVM), the cells hold `someMap(M)` and the functions dispatch to map lookups. +The `noMap` case should not occur in concrete execution, so it returns a default/error. + +```{.k .concrete} + syntax MonoItemKind ::= lookupFunction ( MaybeMap , Ty ) [function, total] + rule lookupFunction(someMap(M), TY) => lookupFunctionMap(M, TY) + rule lookupFunction(noMap, ty(I)) => monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(I), noBody) + + syntax TypeInfo ::= lookupTy ( MaybeMap , Ty ) [function, total] + rule lookupTy(someMap(M), TY) => lookupTyMap(M, TY) + rule lookupTy(noMap, _) => typeInfoVoidType + + syntax Evaluation ::= lookupAlloc ( MaybeMap , AllocId ) [function, total] + rule lookupAlloc(someMap(M), AID) => lookupAllocMap(M, AID) + rule lookupAlloc(noMap, AID) => InvalidAlloc(AID) +``` + +In **symbolic execution** (Haskell/booster), the cells hold `noMap` and the functions are `[no-evaluators]`, +with per-program axioms injected into `definition.kore` providing the actual equations. + +```{.k .symbolic} + syntax MonoItemKind ::= lookupFunction ( MaybeMap , Ty ) [function, total, no-evaluators] + rule lookupFunction(_, TY) => lookupFunctionKore(TY) + + syntax TypeInfo ::= lookupTy ( MaybeMap , Ty ) [function, total, no-evaluators] + rule lookupTy(_, TY) => lookupTyKore(TY) + + syntax Evaluation ::= lookupAlloc ( MaybeMap , AllocId ) [function, total, no-evaluators] + rule lookupAlloc(_, AID) => lookupAllocKore(AID) ``` ```k diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index f4030edc5..895e250c5 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -8,9 +8,12 @@ from pyk.cli.utils import bug_report_arg from pyk.cterm import cterm_symbolic from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KToken +from pyk.kast.prelude.collections import map_of +from pyk.kast.prelude.utils import token from pyk.kcfg.explore import KCFGExplore from pyk.kcfg.semantics import DefaultSemantics from pyk.kcfg.show import NodePrinter +from pyk.kore.syntax import App from pyk.ktool.kprove import KProve from pyk.ktool.krun import KRun from pyk.proof.show import APRProofNodePrinter @@ -84,6 +87,30 @@ class Symbols: END_PROGRAM: Final = KApply('#EndProgram_KMIR-CONTROL-FLOW_KItem') THUNK: Final = KLabel('thunk(_)_RT-DATA_Value_Evaluation') + _MAP_CELL_LABELS: Final = frozenset( + { + "Lbl'-LT-'functions'-GT-'", + "Lbl'-LT-'types'-GT-'", + "Lbl'-LT-'memory'-GT-'", + } + ) + + _NOMAP: Final = App("LblMaybeMap'ColnColn'noMap") + + @staticmethod + def strip_map_cells(pattern: Pattern) -> Pattern: + """Replace contents of , , cells with noMap.""" + + def _strip(p: Pattern) -> Pattern: + if isinstance(p, App) and p.symbol in KMIR._MAP_CELL_LABELS: + return App(p.symbol, p.sorts, (KMIR._NOMAP,)) + return p + + return pattern.top_down(_strip) + + def kore_to_pretty(self, pattern: Pattern) -> str: + return super().kore_to_pretty(self.strip_map_cells(pattern)) + @cached_property def parser(self) -> Parser: return Parser(self.definition) @@ -110,16 +137,54 @@ def run_smir( ) -> Pattern: smir_info = smir_info.reduce_to(start_symbol) mode = RandomMode(seed) if seed is not None else ConcreteMode() + cell_maps = self._make_smir_maps(smir_info) init_config, _ = make_call_config( self.definition, smir_info=smir_info, start_symbol=start_symbol, mode=mode, + cell_maps=cell_maps, ) init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell')) result = self.run_pattern(init_kore, depth=depth) return result + def _make_smir_maps(self, smir_info: SMIRInfo) -> dict[str, KInner]: + """Build map cell substitutions for concrete execution.""" + from .kompile import _decode_alloc, _functions + + some_map = 'MaybeMap::someMap' + + # Functions map: ty(N) |-> MonoItemKind + func_entries: dict[KInner, KInner] = {} + for ty, body in _functions(self, smir_info).items(): + func_entries[KApply('ty', (token(ty),))] = body + functions_map = KApply(some_map, (map_of(func_entries),)) + + # Types map: ty(N) |-> TypeInfo + type_entries: dict[KInner, KInner] = {} + for type_json in smir_info._smir['types']: + parse_result = self.parser.parse_mir_json(type_json, 'TypeMapping') + if parse_result is not None: + type_mapping, _ = parse_result + if isinstance(type_mapping, KApply) and len(type_mapping.args) == 2: + ty_key, tyinfo = type_mapping.args + type_entries[ty_key] = tyinfo + types_map = KApply(some_map, (map_of(type_entries),)) + + # Allocs map: allocId(N) |-> Value + alloc_entries: dict[KInner, KInner] = {} + for raw_alloc in smir_info._smir['allocs']: + alloc_id_term, value_term = _decode_alloc(smir_info=smir_info, raw_alloc=raw_alloc) + alloc_entries[alloc_id_term] = value_term + allocs_map = KApply(some_map, (map_of(alloc_entries),)) + + return { + 'FUNCTIONS_CELL': functions_map, + 'TYPES_CELL': types_map, + 'MEMORY_CELL': allocs_map, + } + @staticmethod def prove_programs(opts: ProveOpts) -> list[APRProof]: from ._prove import prove diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index b56d89511..add631a82 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -310,45 +310,12 @@ def kompile_smir( return KompiledSymbolic(haskell_dir=target_hs_path, llvm_lib_dir=kdist.which(llvm_lib_target)) else: - target_llvmdt_path = target_llvm_path / 'dt' - _LOGGER.info(f'Creating directory {target_llvmdt_path}') - target_llvmdt_path.mkdir(parents=True, exist_ok=True) - - # Process LLVM definition (only SMIR rules for concrete execution) - _LOGGER.info('Writing LLVM definition file') + # No per-program LLVM kompile needed: program data goes into map cells in the + # initial configuration, not into definition.kore. Use the pre-built kdist definition. llvm_def_dir = kdist.which(llvm_target) - llvm_def_file = llvm_def_dir / 'definition.kore' - llvm_def_output = target_llvm_path / 'definition.kore' - _insert_rules_and_write(llvm_def_file, smir_rules, llvm_def_output) - - import subprocess - - _LOGGER.info('Running llvm-kompile-matching') - subprocess.run( - ['llvm-kompile-matching', str(llvm_def_output), 'qbaL', str(target_llvmdt_path), '1/2'], check=True - ) - _LOGGER.info('Running llvm-kompile') - subprocess.run( - [ - 'llvm-kompile', - str(llvm_def_output), - str(target_llvmdt_path), - 'main', - '-O2', - '--', - '-o', - target_llvm_path / 'interpreter', - ], - check=True, - ) - blacklist = ['definition.kore', 'interpreter', 'dt'] - to_copy = [file.name for file in llvm_def_dir.iterdir() if file.name not in blacklist] - for file in to_copy: - _LOGGER.info(f'Copying file {file}') - shutil.copy2(llvm_def_dir / file, target_llvm_path / file) - + _LOGGER.info(f'Using pre-built LLVM definition: {llvm_def_dir}') kompile_digest.write(target_dir) - return KompiledConcrete(llvm_dir=target_llvm_path) + return KompiledConcrete(llvm_dir=llvm_def_dir) def _make_stratified_rules( @@ -451,14 +418,14 @@ def make_kore_rules( ), ) default_function = _mk_equation( - kmir, 'lookupFunction', KApply('ty', (KVariable('TY'),)), 'Ty', unknown_function, 'MonoItemKind' + kmir, 'lookupFunctionKore', KApply('ty', (KVariable('TY'),)), 'Ty', unknown_function, 'MonoItemKind' ).let_attrs(((App('owise')),)) equations: list[Axiom] = [default_function] for fty, kind in _functions(kmir, smir_info).items(): equations.append( - _mk_equation(kmir, 'lookupFunction', KApply('ty', (intToken(fty),)), 'Ty', kind, 'MonoItemKind') + _mk_equation(kmir, 'lookupFunctionKore', KApply('ty', (intToken(fty),)), 'Ty', kind, 'MonoItemKind') ) # stratify type and alloc lookups @@ -478,7 +445,7 @@ def get_int_arg(app: KInner) -> int: for ty, info in (type_mapping.args for type_mapping in type_mappings if isinstance(type_mapping, KApply)) ] - type_equations = _make_stratified_rules(kmir, 'lookupTy', 'Ty', 'TypeInfo', 'ty', type_assocs, invalid_type) + type_equations = _make_stratified_rules(kmir, 'lookupTyKore', 'Ty', 'TypeInfo', 'ty', type_assocs, invalid_type) invalid_alloc_n = KApply( 'InvalidAlloc(_)_RT-VALUE-SYNTAX_Evaluation_AllocId', (KApply('allocId', (KVariable('N'),)),) @@ -486,7 +453,7 @@ def get_int_arg(app: KInner) -> int: decoded_allocs = [_decode_alloc(smir_info=smir_info, raw_alloc=alloc) for alloc in smir_info._smir['allocs']] allocs = [(get_int_arg(alloc_id), value) for (alloc_id, value) in decoded_allocs] alloc_equations = _make_stratified_rules( - kmir, 'lookupAlloc', 'AllocId', 'Evaluation', 'allocId', allocs, invalid_alloc_n + kmir, 'lookupAllocKore', 'AllocId', 'Evaluation', 'allocId', allocs, invalid_alloc_n ) # Generate break-on-function filter rule if filters are provided @@ -494,7 +461,12 @@ def get_int_arg(app: KInner) -> int: if break_on_function: break_on_rules.append(_mk_break_on_functions_rule(kmir, break_on_function)) - return [*equations, *type_equations, *alloc_equations, *break_on_rules] + # Bridge axioms: lookupX(MaybeMap, Key) => lookupXKore(Key) + # In symbolic execution, lookupX is [no-evaluators] so its K rules are not compiled. + # These axioms delegate to lookupXKore which has the per-program equations. + bridge_axioms = _make_lookup_bridge_axioms() + + return [*equations, *type_equations, *alloc_equations, *break_on_rules, *bridge_axioms] def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: @@ -537,6 +509,106 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: return functions +def _make_lookup_bridge_axioms() -> list[Axiom]: + """Generate bridge axioms: lookupX(MaybeMap, Key) => lookupXKore(Key). + + In symbolic execution, lookupX is [no-evaluators], so its K rules are not compiled. + These axioms bridge from the two-argument wrapper to the single-argument Kore + version, which has per-program equations. + """ + from pyk.kore.rule import FunctionRule + + maybemap_sort = SortApp('SortMaybeMap') + ty_sort = SortApp('SortTy') + allocid_sort = SortApp('SortAllocId') + mono_sort = SortApp('SortMonoItemKind') + typeinfo_sort = SortApp('SortTypeInfo') + eval_sort = SortApp('SortEvaluation') + + mm_var = EVar('VarMM', maybemap_sort) + ty_var = EVar('VarTY', ty_sort) + aid_var = EVar('VarAID', allocid_sort) + + list_sort = SortApp('SortList') + + bridges = [ + # #getBlocks(MM, TY) => #getBlocksAux(lookupFunctionKore(TY)) + FunctionRule( + lhs=App( + "Lbl'Hash'getBlocks'LParUndsCommUndsRParUnds'KMIR-CONTROL-FLOW'Unds'List'Unds'MaybeMap'Unds'Ty", + (), + (mm_var, ty_var), + ), + rhs=App( + "Lbl'Hash'getBlocksAux'LParUndsRParUnds'KMIR-CONTROL-FLOW'Unds'List'Unds'MonoItemKind", + (), + (App('LbllookupFunctionKore', (), (ty_var,)),), + ), + req=None, + ens=None, + sort=list_sort, + arg_sorts=(maybemap_sort, ty_sort), + anti_left=None, + priority=50, + uid='getBlocks-bridge', + label='getBlocks-bridge', + ), + # lookupFunction(MM, TY) => lookupFunctionKore(TY) + FunctionRule( + lhs=App( + "LbllookupFunction'LParUndsCommUndsRParUnds'RT-VALUE-SYNTAX'Unds'MonoItemKind'Unds'MaybeMap'Unds'Ty", + (), + (mm_var, ty_var), + ), + rhs=App('LbllookupFunctionKore', (), (ty_var,)), + req=None, + ens=None, + sort=mono_sort, + arg_sorts=(maybemap_sort, ty_sort), + anti_left=None, + priority=50, + uid='lookupFunction-bridge', + label='lookupFunction-bridge', + ), + # lookupTy(MM, TY) => lookupTyKore(TY) + FunctionRule( + lhs=App( + "LbllookupTy'LParUndsCommUndsRParUnds'RT-VALUE-SYNTAX'Unds'TypeInfo'Unds'MaybeMap'Unds'Ty", + (), + (mm_var, ty_var), + ), + rhs=App('LbllookupTyKore', (), (ty_var,)), + req=None, + ens=None, + sort=typeinfo_sort, + arg_sorts=(maybemap_sort, ty_sort), + anti_left=None, + priority=50, + uid='lookupTy-bridge', + label='lookupTy-bridge', + ), + # lookupAlloc(MM, AID) => lookupAllocKore(AID) + FunctionRule( + lhs=App( + "LbllookupAlloc'LParUndsCommUndsRParUnds'RT-VALUE-SYNTAX'Unds'Evaluation'Unds'MaybeMap'Unds'AllocId", + (), + (mm_var, aid_var), + ), + rhs=App('LbllookupAllocKore', (), (aid_var,)), + req=None, + ens=None, + sort=eval_sort, + arg_sorts=(maybemap_sort, allocid_sort), + anti_left=None, + priority=50, + uid='lookupAlloc-bridge', + label='lookupAlloc-bridge', + ), + ] + + return [r.to_axiom().let_attrs((App("UNIQUE'Unds'ID", (), (String(r.uid),)),)) for r in bridges] + + def _mk_equation(kmir: KMIR, fun: str, arg: KInner, arg_sort: str, result: KInner, result_sort: str) -> Axiom: from pyk.kore.rule import FunctionRule from pyk.kore.syntax import App, SortApp diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state b/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state index 5c2707c89..b3c3f4a6f 100644 --- a/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state +++ b/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state @@ -49,4 +49,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state b/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state index 6c3fa5051..615fb9d41 100644 --- a/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state +++ b/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state @@ -65,4 +65,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state b/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state index a1a21b0dc..9f203a65f 100644 --- a/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state +++ b/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state @@ -75,4 +75,13 @@ ListItem ( newLocal ( ty ( 69 ) , mutabilityNot ) ) ) ) ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/option_consts.state b/kmir/src/tests/integration/data/exec-smir/allocs/option_consts.state index 4186cc79a..2fa74f789 100644 --- a/kmir/src/tests/integration/data/exec-smir/allocs/option_consts.state +++ b/kmir/src/tests/integration/data/exec-smir/allocs/option_consts.state @@ -112,4 +112,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state index 09d56cea7..cd59cd6a9 100644 --- a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state +++ b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state @@ -54,4 +54,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.state b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.state index a2940d22a..0bfd448dc 100644 --- a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.state +++ b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.state @@ -67,4 +67,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/arithmetic/unary.state b/kmir/src/tests/integration/data/exec-smir/arithmetic/unary.state index 97333b1b7..6168da334 100644 --- a/kmir/src/tests/integration/data/exec-smir/arithmetic/unary.state +++ b/kmir/src/tests/integration/data/exec-smir/arithmetic/unary.state @@ -41,4 +41,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state index d905964fc..eade196ae 100644 --- a/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state +++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state @@ -49,4 +49,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state index 7e5876270..50c2f9c9c 100644 --- a/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state +++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state @@ -92,4 +92,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state index 861180b8d..91313d7b1 100644 --- a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state +++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state @@ -58,4 +58,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/assign-cast/assign-cast.state b/kmir/src/tests/integration/data/exec-smir/assign-cast/assign-cast.state index b2f9a3ef5..cc4930f2a 100644 --- a/kmir/src/tests/integration/data/exec-smir/assign-cast/assign-cast.state +++ b/kmir/src/tests/integration/data/exec-smir/assign-cast/assign-cast.state @@ -46,4 +46,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state index db13358c2..4a8a68d73 100644 --- a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state @@ -48,4 +48,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state index 056091d15..de0505a08 100644 --- a/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state @@ -36,4 +36,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ) ) ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/enum/enum.state b/kmir/src/tests/integration/data/exec-smir/enum/enum.state index 16e4c197d..3e66b34f1 100644 --- a/kmir/src/tests/integration/data/exec-smir/enum/enum.state +++ b/kmir/src/tests/integration/data/exec-smir/enum/enum.state @@ -55,4 +55,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox.state b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox.state index b05e88c0e..542e329fd 100644 --- a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox.state +++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox.state @@ -50,4 +50,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state b/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state index baeb2b64a..c00481caa 100644 --- a/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state +++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state @@ -40,4 +40,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.run.state b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.run.state index 596624cb4..c43b9a535 100644 --- a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.run.state +++ b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.run.state @@ -32,4 +32,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state index a8b20314b..0d1c3db6c 100644 --- a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state +++ b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state @@ -34,4 +34,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ) ) ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/newtype-pubkey/newtype-pubkey.state b/kmir/src/tests/integration/data/exec-smir/newtype-pubkey/newtype-pubkey.state index ac4b58c68..267694697 100644 --- a/kmir/src/tests/integration/data/exec-smir/newtype-pubkey/newtype-pubkey.state +++ b/kmir/src/tests/integration/data/exec-smir/newtype-pubkey/newtype-pubkey.state @@ -68,4 +68,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/niche-enum/niche-enum.state b/kmir/src/tests/integration/data/exec-smir/niche-enum/niche-enum.state index 2f67853c8..6af3accb9 100644 --- a/kmir/src/tests/integration/data/exec-smir/niche-enum/niche-enum.state +++ b/kmir/src/tests/integration/data/exec-smir/niche-enum/niche-enum.state @@ -76,4 +76,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state b/kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state index 93cab02ec..015c57b93 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state @@ -50,4 +50,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/offset_read.state b/kmir/src/tests/integration/data/exec-smir/pointers/offset_read.state index db78dd210..1a1c8afbd 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/offset_read.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/offset_read.state @@ -46,4 +46,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/offset_struct_field_read.state b/kmir/src/tests/integration/data/exec-smir/pointers/offset_struct_field_read.state index 57c58de76..1fddf5845 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/offset_struct_field_read.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/offset_struct_field_read.state @@ -47,4 +47,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/offset_struct_field_write.state b/kmir/src/tests/integration/data/exec-smir/pointers/offset_struct_field_write.state index fb4462dbf..aa47eaa32 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/offset_struct_field_write.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/offset_struct_field_write.state @@ -50,4 +50,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/offset_write.state b/kmir/src/tests/integration/data/exec-smir/pointers/offset_write.state index 1919e7923..930280859 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/offset_write.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/offset_write.state @@ -49,4 +49,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state index 133db0c7a..72107d4dc 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state @@ -86,4 +86,13 @@ ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 31 ) , mutabilityNot ) ) ) ) ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state index 691092911..3cc57314c 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state @@ -47,4 +47,13 @@ ListItem ( newLocal ( ty ( 35 ) , mutabilityMut ) ) ) ) ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/ref_ptr_cases.state b/kmir/src/tests/integration/data/exec-smir/pointers/ref_ptr_cases.state index 06612f321..3797ad6f4 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/ref_ptr_cases.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/ref_ptr_cases.state @@ -39,4 +39,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state b/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state index c90e1b425..2e320e7a4 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state +++ b/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state @@ -45,4 +45,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state b/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state index de694867d..6cb07fda2 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state +++ b/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state @@ -49,4 +49,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state b/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state index 951a10279..6cd7cc09d 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state +++ b/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state @@ -44,4 +44,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state b/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state index 043aae9d7..211bb5fd3 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state +++ b/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state @@ -39,4 +39,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state b/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state index 043aae9d7..211bb5fd3 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state +++ b/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state @@ -39,4 +39,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/refReturned.state b/kmir/src/tests/integration/data/exec-smir/references/refReturned.state index 7301205f2..218d58ee6 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/refReturned.state +++ b/kmir/src/tests/integration/data/exec-smir/references/refReturned.state @@ -40,4 +40,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/simple.state b/kmir/src/tests/integration/data/exec-smir/references/simple.state index 86f6e5353..0dbc2ab18 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/simple.state +++ b/kmir/src/tests/integration/data/exec-smir/references/simple.state @@ -38,4 +38,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state index 454f37867..4483e10a1 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state +++ b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state @@ -67,4 +67,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/struct-multi/struct-multi.state b/kmir/src/tests/integration/data/exec-smir/struct-multi/struct-multi.state index 17f4708f6..9857b7191 100644 --- a/kmir/src/tests/integration/data/exec-smir/struct-multi/struct-multi.state +++ b/kmir/src/tests/integration/data/exec-smir/struct-multi/struct-multi.state @@ -55,4 +55,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state index 57665d4db..52c132fc6 100644 --- a/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state +++ b/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state @@ -39,4 +39,13 @@ ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state index 47b68a635..16cc797fc 100644 --- a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state +++ b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state @@ -50,4 +50,13 @@ ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) ) ) ) ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + noMap + + + noMap + + + noMap + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/modules/test-add-module-multiple.k b/kmir/src/tests/integration/data/modules/test-add-module-multiple.k index eea9602de..aab768c6e 100644 --- a/kmir/src/tests/integration/data/modules/test-add-module-multiple.k +++ b/kmir/src/tests/integration/data/modules/test-add-module-multiple.k @@ -34,6 +34,9 @@ module TEST-ADD-MODULE ( .List => ListItem ( StackFrame ( CALLER_CELL:Ty , DEST_CELL:Place , TARGET_CELL:MaybeBasicBlockIdx , UNWIND_CELL:UnwindAction , ListItem ( newLocal ( ty ( 0 ) , mutabilityNot ) ) ) ) ) + _FUNCTIONS_CELL + _TYPES_CELL + _MEMORY_CELL [priority(20), label(BASIC-BLOCK-1-TO-3)] diff --git a/kmir/src/tests/integration/data/modules/test-add-module.k b/kmir/src/tests/integration/data/modules/test-add-module.k index fe59569cc..3340bed49 100644 --- a/kmir/src/tests/integration/data/modules/test-add-module.k +++ b/kmir/src/tests/integration/data/modules/test-add-module.k @@ -34,6 +34,9 @@ module TEST-ADD-MODULE ( .List => ListItem ( StackFrame ( CALLER_CELL:Ty , DEST_CELL:Place , TARGET_CELL:MaybeBasicBlockIdx , UNWIND_CELL:UnwindAction , ListItem ( newLocal ( ty ( 0 ) , mutabilityNot ) ) ) ) ) + _FUNCTIONS_CELL + _TYPES_CELL + _MEMORY_CELL [priority(20), label(BASIC-BLOCK-1-TO-3)] diff --git a/kmir/src/tests/integration/data/modules/test-add-module.md b/kmir/src/tests/integration/data/modules/test-add-module.md index 06776ba27..b1dd1ae64 100644 --- a/kmir/src/tests/integration/data/modules/test-add-module.md +++ b/kmir/src/tests/integration/data/modules/test-add-module.md @@ -37,6 +37,9 @@ module TEST-ADD-MODULE ( .List => ListItem ( StackFrame ( CALLER_CELL:Ty , DEST_CELL:Place , TARGET_CELL:MaybeBasicBlockIdx , UNWIND_CELL:UnwindAction , ListItem ( newLocal ( ty ( 0 ) , mutabilityNot ) ) ) ) ) + _FUNCTIONS_CELL + _TYPES_CELL + _MEMORY_CELL [priority(20), label(BASIC-BLOCK-1-TO-3)] diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.json b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.json index 28389199c..187392885 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.json +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.json @@ -859,9 +859,78 @@ ], "arity": 1, "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "MaybeMap::noMap", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "MaybeMap::noMap", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "MaybeMap::noMap", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + ], + "arity": 1, + "variable": false } ], - "arity": 5, + "arity": 8, "variable": false }, { diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.k b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.k index 58b96e706..339905a7c 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.k +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.k @@ -34,6 +34,15 @@ module ASSERT-TRUE-MAIN-SUMMARY ( .List => ListItem ( StackFrame ( CALLER_CELL:Ty , DEST_CELL:Place , TARGET_CELL:MaybeBasicBlockIdx , UNWIND_CELL:UnwindAction , ListItem ( newLocal ( ty ( 0 ) , mutabilityNot ) ) ) ) ) + + noMap + + + noMap + + + noMap + [priority(20), label(BASIC-BLOCK-1-TO-3)] diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected index c8bee9fef..4df1ee996 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected @@ -172,4 +172,13 @@ ListItem ( Integer ( -1714975244 , 32 , true ) ) ListItem ( Integer ( -282729822 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected index 50fb59617..dc05381ec 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected @@ -169,4 +169,13 @@ ListItem ( Integer ( 1296334389 , 32 , true ) ) ListItem ( Integer ( -784133741 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected index 66dbadacc..61d3a4c39 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected @@ -173,4 +173,13 @@ ListItem ( Integer ( 1751273387 , 32 , true ) ) ListItem ( Integer ( -1385399937 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected index d408600a9..8fdbfb7d2 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected @@ -175,4 +175,13 @@ ListItem ( Integer ( 1870830728 , 32 , true ) ) ListItem ( Integer ( 1627219933 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected index 2b6e8720c..75f95d39c 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected @@ -188,4 +188,13 @@ ListItem ( Integer ( 1776105656 , 32 , true ) ) ListItem ( Integer ( -252750415 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected index 73d82794e..9c502a6da 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected @@ -191,4 +191,13 @@ ListItem ( Integer ( 1368024730 , 32 , true ) ) ListItem ( Integer ( -791162561 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected index 3a3a93c89..1f726bf41 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected @@ -198,4 +198,13 @@ ListItem ( Integer ( 1422748784 , 32 , true ) ) ListItem ( Integer ( 1271734833 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-7.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-7.expected index 8bdd69426..24996c869 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-7.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-7.expected @@ -145,4 +145,13 @@ ListItem ( Integer ( 281121487 , 32 , true ) ) ListItem ( Integer ( 1921781853 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected index 056a32057..ebbdbce5f 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected @@ -195,4 +195,13 @@ ListItem ( Integer ( -328986497 , 32 , true ) ) ListItem ( Integer ( -528598575 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected index 92a082106..b433d58dd 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected @@ -176,4 +176,13 @@ ListItem ( Integer ( -939805772 , 32 , true ) ) ListItem ( Integer ( 1329338341 , 32 , true ) ) ) , ty ( 26 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected index 7e6b4e60a..e5768ef19 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected @@ -48,4 +48,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected index 8d4f34f7d..4a81c9ce4 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected @@ -47,4 +47,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected index 6bbd4c726..77029a80b 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected @@ -51,4 +51,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected index a46aea65e..c9e735075 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected @@ -53,4 +53,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected index 77d20383f..ae6ff6199 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected @@ -66,4 +66,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected index b2eeca22a..3c3dbdff1 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected @@ -66,4 +66,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected index 175fabdab..2df7d2f74 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected @@ -73,4 +73,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected index d186da3b3..4142b18ac 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected @@ -46,4 +46,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-8.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-8.expected index 5a1813338..693fab834 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-8.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-8.expected @@ -73,4 +73,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-9.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-9.expected index edca97d9f..2f285e198 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-9.expected @@ -52,4 +52,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-0.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-0.expected index f041f3897..4a7601aef 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-0.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-0.expected @@ -80,4 +80,13 @@ ListItem ( typedValue ( Integer ( 197 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( -341142443 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-1.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-1.expected index d4175ed23..e587eee6e 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-1.expected @@ -81,4 +81,13 @@ ListItem ( typedValue ( Integer ( 32 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( -1051970500 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-2.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-2.expected index c9b4a3ba5..b960d74c0 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-2.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-2.expected @@ -80,4 +80,13 @@ ListItem ( typedValue ( Integer ( 28 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( -1754129965 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-3.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-3.expected index 09fef980f..f02e9aadd 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-3.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-3.expected @@ -81,4 +81,13 @@ ListItem ( typedValue ( Integer ( 66 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 446333181 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-4.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-4.expected index fe0fc56a4..92f1333f6 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-4.expected @@ -81,4 +81,13 @@ ListItem ( typedValue ( Integer ( 155 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( -446426455 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-5.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-5.expected index 451c52bb4..b363707fe 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-5.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-5.expected @@ -81,4 +81,13 @@ ListItem ( typedValue ( Integer ( 130 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 1038467225 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-6.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-6.expected index 0ccc56705..6fa521d3d 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-6.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-6.expected @@ -80,4 +80,13 @@ ListItem ( typedValue ( Integer ( 41 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( -1023827911 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-7.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-7.expected index f39dc9787..3bd93d693 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-7.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-7.expected @@ -81,4 +81,13 @@ ListItem ( typedValue ( Integer ( 77 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( -1940095024 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-8.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-8.expected index ef460d19e..1a2b98ea9 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-8.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-8.expected @@ -81,4 +81,13 @@ ListItem ( typedValue ( Integer ( 189 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 1985542055 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-9.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-9.expected index 3bd535f28..e5318c885 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-9.expected @@ -81,4 +81,13 @@ ListItem ( typedValue ( Integer ( 191 , 8 , false ) , ty ( 9 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( -1000150020 , 32 , true ) , ty ( 8 ) , mutabilityNot ) ) ) ) - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-0.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-0.expected index 821e11dd2..4ad0e2777 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-0.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-0.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-1.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-1.expected index 49c6c69f5..21f2d1992 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-1.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-2.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-2.expected index d28072381..2d5724dd1 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-2.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-2.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-3.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-3.expected index 27c8bd0af..565bd796b 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-3.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-3.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-4.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-4.expected index 56e7fffcf..b95df21b5 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-4.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-5.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-5.expected index 23a47f9da..46f3ae6b5 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-5.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-5.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-6.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-6.expected index 5d3b0ff0c..81485dc9c 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-6.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-6.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-7.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-7.expected index 6d7802d4e..bd44c9b31 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-7.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-7.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-8.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-8.expected index c2dccad40..7ebc7a807 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-8.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-8.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-9.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-9.expected index cf31f963d..636d1e6f6 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-9.expected @@ -34,4 +34,13 @@ .List - \ No newline at end of file + + noMap + + + noMap + + + noMap + + diff --git a/kmir/src/tests/integration/test_decode_value.py b/kmir/src/tests/integration/test_decode_value.py index afbcb2560..0b29b3f7e 100644 --- a/kmir/src/tests/integration/test_decode_value.py +++ b/kmir/src/tests/integration/test_decode_value.py @@ -16,35 +16,31 @@ @pytest.fixture(scope='session') -def definition_dir(): # -> Path: - import time +def kmir_instance(): + import tempfile from kmir.kmir import KMIR - from .utils import TEST_DATA_DIR + with tempfile.TemporaryDirectory() as target_dir: + from pathlib import Path + + kmir = KMIR.from_kompiled_kore(TEST_SMIR, target_dir=Path(target_dir), symbolic=False) + yield kmir + - target_dir = TEST_DATA_DIR / 'decode-value' / 'tmp' +@pytest.fixture(scope='session') +def definition_dir(kmir_instance): # -> Path: + return kmir_instance.definition_dir - # prevent other processes from concurrently trying to compile - # (the scope='session' above does not actually work in pytest-xdist) - lock_file = TEST_DATA_DIR / 'decode-value' / 'tmp.lock' - try: - with open(lock_file, 'x') as _: - # generate and compile an LLVM interpreter with the type-table - _ = KMIR.from_kompiled_kore(TEST_SMIR, target_dir=target_dir, symbolic=False) - lock_file.unlink() - except FileExistsError: - # wait loop until interpreter exists, max 1min - secs = 0 - while lock_file.exists() and secs < 60: - time.sleep(1) - if not (target_dir / 'llvm' / 'interpreter').exists(): - raise Exception('Waited in vain for interpreter to arise. Exiting') from None - yield target_dir / 'llvm' +@pytest.fixture(scope='session') +def types_cell_kore(kmir_instance): + """Build the types map cell as a Kore pattern for use in the test template.""" + from pyk.kast.inner import KSort - # should remove the target_dir but other processes are probably still using it - print(f'Remove {target_dir} if you want to clean up') + cell_maps = kmir_instance._make_smir_maps(TEST_SMIR) + types_kast = cell_maps['TYPES_CELL'] + return kmir_instance.kast_to_kore(types_kast, KSort('MaybeMap')).text @pytest.fixture(scope='session') @@ -85,6 +81,9 @@ def dedent(s: str) -> str: Lbl'-LT-'locals'-GT-'{}(Lbl'Stop'List{}()) ), Lbl'-LT-'stack'-GT-'{}(Lbl'Stop'List{}()), + Lbl'-LT-'functions'-GT-'{}(LblMaybeMap'ColnColn'noMap{}()), /* noMap: not needed for decode tests; use someMap otherwise */ + Lbl'-LT-'types'-GT-'{}($types_cell), + Lbl'-LT-'memory'-GT-'{}(LblMaybeMap'ColnColn'noMap{}()) /* noMap: not needed for decode tests; use someMap otherwise */ ), Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")) ) @@ -98,7 +97,7 @@ class _TestData(NamedTuple): type_info: dict[str, Any] expected: str - def to_pattern(self, definition: KDefinition) -> Pattern: + def to_pattern(self, definition: KDefinition, types_cell_pattern: Pattern) -> Pattern: from pyk.kore.prelude import bytes_dv from pyk.kore.syntax import App @@ -106,6 +105,7 @@ def to_pattern(self, definition: KDefinition) -> Pattern: 'LbldecodeValue', (), ( + types_cell_pattern, bytes_dv(self.bytez), self._json_type_info_to_kore(self.type_info, definition), ), @@ -192,6 +192,7 @@ def test_decode_value( test_data: _TestData, definition_dir: Path, definition: KDefinition, + types_cell_kore: str, tmp_path: Path, ) -> None: from pyk.kore import match as km @@ -204,8 +205,9 @@ def test_decode_value( pytest.skip() # Given - evaluation = test_data.to_pattern(definition) - kore_text = KORE_TEMPLATE.substitute(evaluation=evaluation.text) + types_pattern = KoreParser(types_cell_kore).pattern() + evaluation = test_data.to_pattern(definition, types_cell_pattern=types_pattern) + kore_text = KORE_TEMPLATE.substitute(evaluation=evaluation.text, types_cell=types_cell_kore) parser = KoreParser(kore_text) init_pattern = parser.pattern() assert parser.eof diff --git a/kmir/src/tests/integration/test_run_smir_random.py b/kmir/src/tests/integration/test_run_smir_random.py index 7fcb220ca..9cdf8353a 100644 --- a/kmir/src/tests/integration/test_run_smir_random.py +++ b/kmir/src/tests/integration/test_run_smir_random.py @@ -6,7 +6,6 @@ import pytest from pyk.kast.prelude.k import GENERATED_TOP_CELL -from pyk.kore.tools import kore_print from pyk.ktool.krun import llvm_interpret from kmir.kast import RandomMode, make_call_config @@ -97,18 +96,16 @@ def test_run_smir_random( update_expected_output: bool, ) -> None: # When + cell_maps = kmir._make_smir_maps(smir_info) init_kast, _ = make_call_config( kmir.definition, smir_info=smir_info, start_symbol='test', mode=RandomMode(seed), + cell_maps=cell_maps, ) init_kore = kmir.kast_to_kore(init_kast, sort=GENERATED_TOP_CELL) - actual_init = kore_print( - definition_dir=kmir.definition_dir, - pattern=init_kore, - output='pretty', - ) + actual_init = kmir.kore_to_pretty(init_kore) # Then if update_expected_output: @@ -121,11 +118,7 @@ def test_run_smir_random( definition_dir=kmir.definition_dir, pattern=init_kore, ) - actual_final = kore_print( - definition_dir=kmir.definition_dir, - pattern=final_kore, - output='pretty', - ) + actual_final = kmir.kore_to_pretty(final_kore) # Then if update_expected_output: