diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 0f0261a69..a14906759 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmir" -version = "0.3.37" +version = "0.3.38" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index b95c81c38..269c06dc2 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.37' +VERSION: Final = '0.3.38' diff --git a/kmir/src/kmir/kdist/mir-semantics/abi.k b/kmir/src/kmir/kdist/mir-semantics/abi.k deleted file mode 100644 index 267a6c438..000000000 --- a/kmir/src/kmir/kdist/mir-semantics/abi.k +++ /dev/null @@ -1,85 +0,0 @@ -module ABI - imports LIB-SORTS - imports TARGET-SORTS - imports TYPES-SORTS - imports INT - -syntax RangeInclusiveForVariantIdx ::= rangeInclusiveForVariantIdx(start: VariantIdx, end: VariantIdx) - -syntax FnAbi ::= fnAbi(args: ArgAbis, ret: ArgAbi, fixedCount: MIRInt, conv: CallConvention, cVariadic: MIRBool) - -syntax ArgAbi ::= argAbi(ty: Ty, layout: Layout, mode: PassMode) -syntax ArgAbis ::= List {ArgAbi, ""} - -syntax Layout ::= layout(Int) -syntax TyAndLayout ::= tyAndLayout(ty: Ty, layout: Layout) - -syntax PassMode ::= "passModeIgnore" - | passModeDirect(Opaque) - | passModePair(Opaque, Opaque) - | passModeCast(padI32: MIRBool, cast: Opaque) - | passModeIndirect(attrs: Opaque, metaAttrs: Opaque, onStack: MIRBool) - -syntax LayoutShape ::= layoutShape(fields: FieldsShape, variants: VariantsShape, abi: ValueAbi, abiAlign: Align, layoutSize: MachineSize) -syntax LayoutShapes ::= List {LayoutShape, ""} - -syntax FieldsShape ::= "fieldsShapePrimitive" - | fieldsShapeUnion(NonZero) - | fieldsShapeArray(stride: MachineSize, count: MIRInt) - | fieldsShapeArbitrary(offsets: MachineSizeList) - -syntax VariantsShape ::= variantsShapeSingle(index: VariantIdx) - | variantsShapeMultiple(tag: Scalar, tagEncoding: TagEncoding, tagField: MIRInt, variants: LayoutShapes) - -syntax ValueAbi ::= "valueAbiUninhabited" - | valueAbiScalar(Scalar) - | valueAbiScalarPair(Scalar, Scalar) - | valueAbiVector(element: Scalar, count: MIRInt) - | valueAbiAggregate(sized: Bool) - -syntax NonZero ::= nonZero(Int) -syntax MachineSizeList ::= List {MachineSize, ""} - -syntax TagEncoding ::= "tagEncodingDirect" - | tagEncodingNiche(untaggedVariant: VariantIdx, nicheVariants: RangeInclusiveForVariantIdx, nicheStart: MIRInt) - -syntax Scalar ::= scalarInitialized(value: Primitive, validRange: WrappingRange) - | scalarUnion(value: Primitive) -syntax Primitive ::= primitiveInt(length: IntegerLength, signed: MIRBool) - | primitiveFloat(length: FloatLength) - | primitivePointer(addressSpace: AddressSpace) -syntax IntegerLength ::= "integerLengthI8" - | "integerLengthI16" - | "integerLengthI32" - | "integerLengthI64" - | "integerLengthI128" -syntax FloatLength ::= "floatLengthF16" - | "floatLengthF32" - | "floatLengthF64" - | "floatLengthF128" - -syntax AddressSpace ::= addressSpace(Int) - -syntax WrappingRange ::= wrappingRange(start: MIRInt, end: MIRInt) - -syntax CallConvention ::= "callConventionC" - | "callConventionRust" - | "callConventionCold" - | "callConventionPreserveMost" - | "callConventionPreserveAll" - | "callConventionArmAapcs" - | "callConventionCCmseNonSecureCall" - | "callConventionMsp430Intr" - | "callConventionPtxKernel" - | "callConventionX86Fastcall" - | "callConventionX86Intr" - | "callConventionX86Stdcall" - | "callConventionX86ThisCall" - | "callConventionX86VectorCall" - | "callConventionX8664SysV" - | "callConventionX8664Win64" - | "callConventionAvrInterrupt" - | "callConventionAvrNonBlockingInterrupt" - | "callConventionRiscvInterrupt" - -endmodule diff --git a/kmir/src/kmir/kdist/mir-semantics/abi.md b/kmir/src/kmir/kdist/mir-semantics/abi.md new file mode 100644 index 000000000..509a83063 --- /dev/null +++ b/kmir/src/kmir/kdist/mir-semantics/abi.md @@ -0,0 +1,146 @@ +```k +module ABI + imports LIB-SORTS + imports TARGET-SORTS + imports TYPES-SORTS + imports INT +``` + +#### Internal MIR +- [FnAbi](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_target/src/abi/call/mod.rs#L786-L815) +- [ArgAbi](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_target/src/abi/call/mod.rs#L569-L575) +- [Layout](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_target/src/abi/mod.rs#L71-L73) +- [TyAndLayout](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_target/src/abi/mod.rs#L133-L144) +- [PassMode](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_target/src/abi/call/mod.rs#L34-L70) +- [LayoutS](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L1553-L1594) +- [FieldsShape](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L1162-L1204) +- [Variants](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L1421-L1440) +- [Abi](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L1297-L1313) +- [TagEncoding](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L1442-L1465) +- [Scalar](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L1068-L1088) +- [Primitive](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L957-L971) +- [Integer](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L797-L806) +- [Float](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L922-L930) +- [AddressSpace](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L1285-L1290) +- [WrappingRange](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_abi/src/lib.rs#L1003-L1017) +- [Conv](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_target/src/abi/call/mod.rs#L730-L762) + +#### SMIR (Bridge) +- [FnAbi](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L67-L81) +- [ArgAbi](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L83-L93) +- [Layout](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L43-L49) +- [TyAndLayout](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L35-L41) +- [PassMode](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L123-L145) +- [LayoutShape](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L51-L65) +- [FieldsShape](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L147-L162) +- [VariantsShape](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L164-L184) +- [ValueAbi](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L203-L219) +- [TagEncoding](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L186-L201) +- [Scalar](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L237-L249) +- [Primitive](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L251-L265) +- [IntegerLength](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L275-L287) +- [FloatLength](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L289-L300) +- [AddressSpace](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L267-L273) +- [WrappingRange](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L302-L308) +- [CallConvention](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/abi.rs#L95-L121) + +#### Stable MIR +- [FnAbi](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L13-L32) +- [ArgAbi](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L34-L40) +- [Layout](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L112-L113) +- [TyAndLayout](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L64-L68) +- [PassMode](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L42-L61) +- [LayoutShape](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L70-L92) +- [FieldsShape](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L130-L156) +- [VariantsShape](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L181-L198) +- [ValueAbi](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L223-L238) +- [TagEncoding](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L200-L221) +- [Scalar](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L253-L270) +- [Primitive](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L283-L301) +- [IntegerLength](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L313-L321) +- [FloatLength](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L323-L330) +- [AddressSpace](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L355-L359) +- [WrappingRange](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L366-L377) +- [CallConvention](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/abi.rs#L423-L454) + +```k +syntax RangeInclusiveForVariantIdx ::= rangeInclusiveForVariantIdx(start: VariantIdx, end: VariantIdx) + +syntax FnAbi ::= fnAbi(args: ArgAbis, ret: ArgAbi, fixedCount: MIRInt, conv: CallConvention, cVariadic: MIRBool) + +syntax ArgAbi ::= argAbi(ty: Ty, layout: Layout, mode: PassMode) +syntax ArgAbis ::= List {ArgAbi, ""} + +syntax Layout ::= layout(Int) +syntax TyAndLayout ::= tyAndLayout(ty: Ty, layout: Layout) + +syntax PassMode ::= "passModeIgnore" + | passModeDirect(Opaque) + | passModePair(Opaque, Opaque) + | passModeCast(padI32: MIRBool, cast: Opaque) + | passModeIndirect(attrs: Opaque, metaAttrs: Opaque, onStack: MIRBool) + +syntax LayoutShape ::= layoutShape(fields: FieldsShape, variants: VariantsShape, abi: ValueAbi, abiAlign: Align, layoutSize: MachineSize) +syntax LayoutShapes ::= List {LayoutShape, ""} + +syntax FieldsShape ::= "fieldsShapePrimitive" + | fieldsShapeUnion(NonZero) + | fieldsShapeArray(stride: MachineSize, count: MIRInt) + | fieldsShapeArbitrary(offsets: MachineSizeList) + +syntax VariantsShape ::= variantsShapeSingle(index: VariantIdx) + | variantsShapeMultiple(tag: Scalar, tagEncoding: TagEncoding, tagField: MIRInt, variants: LayoutShapes) + +syntax ValueAbi ::= "valueAbiUninhabited" + | valueAbiScalar(Scalar) + | valueAbiScalarPair(Scalar, Scalar) + | valueAbiVector(element: Scalar, count: MIRInt) + | valueAbiAggregate(sized: Bool) + +syntax NonZero ::= nonZero(Int) +syntax MachineSizeList ::= List {MachineSize, ""} + +syntax TagEncoding ::= "tagEncodingDirect" + | tagEncodingNiche(untaggedVariant: VariantIdx, nicheVariants: RangeInclusiveForVariantIdx, nicheStart: MIRInt) + +syntax Scalar ::= scalarInitialized(value: Primitive, validRange: WrappingRange) + | scalarUnion(value: Primitive) +syntax Primitive ::= primitiveInt(length: IntegerLength, signed: MIRBool) + | primitiveFloat(length: FloatLength) + | primitivePointer(addressSpace: AddressSpace) +syntax IntegerLength ::= "integerLengthI8" + | "integerLengthI16" + | "integerLengthI32" + | "integerLengthI64" + | "integerLengthI128" +syntax FloatLength ::= "floatLengthF16" + | "floatLengthF32" + | "floatLengthF64" + | "floatLengthF128" + +syntax AddressSpace ::= addressSpace(Int) + +syntax WrappingRange ::= wrappingRange(start: MIRInt, end: MIRInt) + +syntax CallConvention ::= "callConventionC" + | "callConventionRust" + | "callConventionCold" + | "callConventionPreserveMost" + | "callConventionPreserveAll" + | "callConventionArmAapcs" + | "callConventionCCmseNonSecureCall" + | "callConventionMsp430Intr" + | "callConventionPtxKernel" + | "callConventionX86Fastcall" + | "callConventionX86Intr" + | "callConventionX86Stdcall" + | "callConventionX86ThisCall" + | "callConventionX86VectorCall" + | "callConventionX8664SysV" + | "callConventionX8664Win64" + | "callConventionAvrInterrupt" + | "callConventionAvrNonBlockingInterrupt" + | "callConventionRiscvInterrupt" + +endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/alloc.k b/kmir/src/kmir/kdist/mir-semantics/alloc.md similarity index 50% rename from kmir/src/kmir/kdist/mir-semantics/alloc.k rename to kmir/src/kmir/kdist/mir-semantics/alloc.md index 10791a9c9..a23a7359a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/alloc.k +++ b/kmir/src/kmir/kdist/mir-semantics/alloc.md @@ -1,3 +1,4 @@ +```k module ALLOC-SORTS syntax AllocId @@ -10,7 +11,21 @@ module ALLOC imports MONO-SORTS imports TYPES-SORTS imports INT +``` +#### Internal MIR +- [AllocId](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_middle/src/mir/interpret/mod.rs#L104-L105) +- [GlobalAlloc](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_middle/src/mir/interpret/mod.rs#L270-L288) + +#### SMIR (Bridge) +- [AllocId](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs#L701-L706) +- [GlobalAlloc](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs#L708-L725) + +#### Stable MIR +- [AllocId](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/alloc.rs#L45-L47) +- [GlobalAlloc](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/alloc.rs#L11-L25) + +```k syntax BinderForExistentialTraitRef ::= binderForExistentialTraitRef(value: ExistentialTraitRef, boundVars: BoundVariableKindList) syntax MaybeBinderForExistentialTraitRef ::= someBinderForExistentialTraitRef(BinderForExistentialTraitRef) | "noBinderForExistentialTraitRef" @@ -24,3 +39,4 @@ syntax GlobalAllocsMap ::= List {GlobalAllocEntry, ""} [symbol(globalAllocsMap), syntax AllocId ::= allocId(Int) [symbol(allocId)] endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/body.k b/kmir/src/kmir/kdist/mir-semantics/body.md similarity index 85% rename from kmir/src/kmir/kdist/mir-semantics/body.k rename to kmir/src/kmir/kdist/mir-semantics/body.md index a29f4ca20..c9e6ab72f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/body.k +++ b/kmir/src/kmir/kdist/mir-semantics/body.md @@ -1,3 +1,4 @@ +```k module BODY-SORTS syntax Body @@ -18,6 +19,48 @@ module BODY imports TYPES-SORTS imports INT imports STRING +``` + +#### Internal MIR +- [DefId](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_span/src/def_id.rs#L216-L235) +- LocalDefId - not present ? +- Coverage - not present ? +- [Mutability](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_ast_ir/src/lib.rs#L21-L27) +- [Safety](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_hir/src/hir.rs#L3221-L3226) +- BasicBlockIdx - not present +- [Operand](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_middle/src/mir/syntax.rs#L1155-L1200) +- [Local](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_middle/src/mir/mod.rs#L901-L909) +- [ProjectionElem](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_middle/src/mir/syntax.rs#L1065-L1148) [PlaceElem](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_middle/src/mir/syntax.rs#L1150-L1152) +- [Place](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_middle/src/mir/syntax.rs#L979-L1063) +- [SwitchTargets](https://github.com/runtimeverification/rust/blob/85f90a461262f7ca37a6e629933d455fa9c3ee48/compiler/rustc_middle/src/mir/syntax.rs#L877-L896) + +#### SMIR (Bridge) +- [DefId](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_internal/mod.rs#L148-L150) +- LocalDefId - not present +- Coverage - not present +- [Mutability](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs#L221-L230) +- [Safety](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mod.rs#L14-L22) +- BasicBlockIdx - not present +- [Operand](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs#L318-L328) +- [Local](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs#L394-L399) +- [ProjectionElem](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs#L352-L384) +- [Place](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs#L342-L350) +- [SwitchTargets](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs#L613-L619) + +#### Stable MIR +- [DefId](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/crate_def.rs#L8-L10) +- [LocalDefId](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L383) +- [Coverage](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L387) +- [Mutability](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L916-L920) +- [Safety](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L922-L926) +- [BasicBlockIdx](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L38) +- [Operand](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L637-L641) +- [Local](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L811) +- [ProjectionElem](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L725-L802) +- [Place](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L644-L649) +- [SwitchTargets](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/stable_mir/src/mir/body.rs#L833-L842) + +```k syntax DefId ::= defId(Int) [group(mir-int)] syntax LocalDefId ::= localDefId(Opaque) [group(mir)] @@ -277,3 +320,4 @@ syntax Body ::= body(blocks: BasicBlocks, locals: LocalDecls, argCount: MIRInt, syntax Bodies ::= List {Body, ""} [group(mir-list), symbol(Bodies::append), terminator-symbol(Bodies::empty)] endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir-ast.k b/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md similarity index 58% rename from kmir/src/kmir/kdist/mir-semantics/kmir-ast.k rename to kmir/src/kmir/kdist/mir-semantics/kmir-ast.md index a43a4cbb9..2608dada2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir-ast.k +++ b/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md @@ -1,10 +1,11 @@ -requires "abi.k" -requires "alloc.k" -requires "body.k" -requires "lib.k" -requires "mono.k" -requires "target.k" -requires "ty.k" +```k +requires "abi.md" +requires "alloc.md" +requires "body.md" +requires "lib.md" +requires "mono.md" +requires "target.md" +requires "ty.md" module KMIR-AST imports ABI @@ -18,3 +19,4 @@ module KMIR-AST syntax Pgm ::= Symbol GlobalAllocsMap MonoItems [symbol(pgm)] endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.k b/kmir/src/kmir/kdist/mir-semantics/kmir.md similarity index 99% rename from kmir/src/kmir/kdist/mir-semantics/kmir.k rename to kmir/src/kmir/kdist/mir-semantics/kmir.md index f0b7db5eb..c539c385b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.k +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -1,4 +1,5 @@ -requires "kmir-ast.k" +```k +requires "kmir-ast.md" requires "utils.k" module KMIR-SYNTAX @@ -811,3 +812,4 @@ module KMIR rule #numLocals( _:LocalDecl Rest:LocalDecls ) => 1 +Int #numLocals( Rest ) rule #numLocals( .LocalDecls ) => 0 endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/lib.k b/kmir/src/kmir/kdist/mir-semantics/lib.md similarity index 99% rename from kmir/src/kmir/kdist/mir-semantics/lib.k rename to kmir/src/kmir/kdist/mir-semantics/lib.md index b10e3e296..79fbe6d94 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lib.k +++ b/kmir/src/kmir/kdist/mir-semantics/lib.md @@ -1,3 +1,4 @@ +```k module LIB-SORTS syntax CrateItem @@ -32,3 +33,4 @@ syntax CtorKind ::= "ctorKindConst" | "ctorKindFn" endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/mono.k b/kmir/src/kmir/kdist/mir-semantics/mono.md similarity index 99% rename from kmir/src/kmir/kdist/mir-semantics/mono.k rename to kmir/src/kmir/kdist/mir-semantics/mono.md index 36ad5cbe8..d7c84a87c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/mono.k +++ b/kmir/src/kmir/kdist/mir-semantics/mono.md @@ -1,3 +1,4 @@ +```k module MONO-SORTS syntax Instance @@ -31,3 +32,4 @@ syntax InstanceKind ::= "instanceKindItem" [symbol(instanceKindItem)] syntax InstanceDef ::= instanceDef(Int) endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/target.k b/kmir/src/kmir/kdist/mir-semantics/target.md similarity index 97% rename from kmir/src/kmir/kdist/mir-semantics/target.k rename to kmir/src/kmir/kdist/mir-semantics/target.md index 09e36879d..a43df98f6 100644 --- a/kmir/src/kmir/kdist/mir-semantics/target.k +++ b/kmir/src/kmir/kdist/mir-semantics/target.md @@ -1,3 +1,4 @@ +```k module TARGET-SORTS syntax MachineSize @@ -13,3 +14,4 @@ syntax Endian ::= "endianLittle" | "endianBig" syntax MachineSize ::= machineSize(numBits: Int) endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/ty.k b/kmir/src/kmir/kdist/mir-semantics/ty.md similarity index 99% rename from kmir/src/kmir/kdist/mir-semantics/ty.k rename to kmir/src/kmir/kdist/mir-semantics/ty.md index 1ea97e7f5..b93f3c157 100644 --- a/kmir/src/kmir/kdist/mir-semantics/ty.k +++ b/kmir/src/kmir/kdist/mir-semantics/ty.md @@ -1,3 +1,4 @@ +```k module TYPES-SORTS syntax AdtDef @@ -326,3 +327,4 @@ syntax PredicatePolarity ::= "predicatePolarityPositive" | "predicatePolarityNegative" endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/plugin.py b/kmir/src/kmir/kdist/plugin.py index 8afe3d176..c2d2f6f43 100644 --- a/kmir/src/kmir/kdist/plugin.py +++ b/kmir/src/kmir/kdist/plugin.py @@ -52,14 +52,14 @@ def _default_args(src_dir: Path) -> dict[str, Any]: 'source': SourceTarget(), 'llvm': KompileTarget( lambda src_dir: { - 'main_file': src_dir / 'mir-semantics/kmir.k', + 'main_file': src_dir / 'mir-semantics/kmir.md', 'backend': PykBackend.LLVM, **_default_args(src_dir), }, ), 'llvm-library': KompileTarget( lambda src_dir: { - 'main_file': src_dir / 'mir-semantics/kmir.k', + 'main_file': src_dir / 'mir-semantics/kmir.md', 'backend': PykBackend.LLVM, 'llvm_kompile_type': LLVMKompileType.C, **_default_args(src_dir), @@ -67,7 +67,7 @@ def _default_args(src_dir: Path) -> dict[str, Any]: ), 'haskell': KompileTarget( lambda src_dir: { - 'main_file': src_dir / 'mir-semantics/kmir.k', + 'main_file': src_dir / 'mir-semantics/kmir.md', 'backend': PykBackend.HASKELL, **_default_args(src_dir), }, diff --git a/package/version b/package/version index ba61ff307..b2ccc30ee 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.37 +0.3.38