Skip to content

Commit 84bea09

Browse files
rv-jenkinsrv-jenkins
authored
Update dependency: deps/stable-mir-json_release (#634)
* `stable-mir-json` now adds layout information to type metadata (not parsed yet) * small changes to type metadata
1 parent b8a15a9 commit 84bea09

53 files changed

Lines changed: 29689 additions & 9559 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Dockerfile.kmir‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,8 @@ RUN cd /deps/stable-mir-json && \
5757
ln -s /home/kmir/.stable-mir-json/release.sh /home/kmir/.local/bin/stable-mir-json && \
5858
cargo clean
5959

60+
RUN bash -c 'rustup toolchain list && rustup default $(rustup toolchain list)'
61+
6062
# Fixuid is helpful for 1 time executions of docker containers but is not helpful when relying on `docker exec`
6163
ENTRYPOINT ["fixuid", "-q"]
6264

‎Makefile‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ test: test-unit test-integration smir-parse-tests
1616
##################################################
1717
# for integration tests: build stable-mir-json in-tree
1818

19-
stable-mir-json: CARGO_BUILD_OPTS =
19+
stable-mir-json: CARGO_BUILD_OPTS =
2020
stable-mir-json:
2121
cd deps/stable-mir-json && cargo build ${CARGO_BUILD_OPTS}
2222
cd deps/stable-mir-json && cargo run --bin cargo_stable_mir_json -- ${TOP_DIR}/deps/stable-mir-json ${TOP_DIR}/deps
@@ -120,19 +120,20 @@ pyupgrade:
120120
# Update smir exec tests expectations
121121
.PHONY: update-exec-smir
122122
update-exec-smir:
123-
$(UV_RUN) pytest -k test_exec_smir --update-expected-output
123+
$(UV_RUN) pytest -k test_exec_smir --update-expected-output -v --numprocesses=4
124124

125125
# Update checked-in smir.json files (using stable-mir-json dependency and jq)
126+
# file paths for spans in the the updated smir are truncated to known infixes
126127
.PHONY: update-smir-json
127-
update-smir-json: TARGETS = $(shell git ls-files | grep -e ".*\.smir\.json$$")
128+
update-smir-json: TARGETS = $(shell git ls-files | grep -e ".*\.smir\.json$$" | grep -v -e pinocchio)
128129
update-smir-json: SMIR = cargo -q -Z unstable-options -C deps/stable-mir-json run --
129130
update-smir-json: stable-mir-json
130131
for file in ${TARGETS}; do \
131132
dir=$$(realpath $$(dirname $$file)); \
132133
rust=$$dir/$$(basename $${file%.smir.json}.rs); \
133134
[ -f "$$rust" ] || (echo "Source file $$rust missing."; exit 1); \
134135
${SMIR} -Zno-codegen --out-dir $$dir $$rust; \
135-
jq . $$file > $$file.tmp; \
136+
jq '.spans[].[1].[0] |= sub("/.*lib/rustlib"; "rustlib") | .spans[].[1].[0] |= sub("/.*/integration/data"; "data")' $$file > $$file.tmp; \
136137
mv $$file.tmp $$file; \
137138
done
138139

‎deps/stable-mir-json‎

Submodule stable-mir-json updated 35 files

‎deps/stable-mir-json_release‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
180bfb4a7ec49ec2d999a1aae7364c1001d5e3da
1+
62a239d7102b4871a8d24eb921aab3630b7bd3a9

‎kmir/src/kmir/kast.py‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
161161
case EnumT(_, _, discriminants):
162162
variant_var = self._fresh_var('ARG_VARIDX')
163163
# constraints for variant index being in range
164-
max_variant = max(discriminants.keys())
164+
max_variant = len(discriminants)
165165
idx_range = [
166166
mlEqualsTrue(leInt(token(0), variant_var)),
167167
mlEqualsTrue(leInt(variant_var, token(max_variant))),
@@ -188,11 +188,11 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
188188

189189
case ArrayT(_, None):
190190
elems = self._fresh_var('ARG_ARRAY')
191-
len = self._fresh_var('ARG_ARRAY_LEN')
191+
l = self._fresh_var('ARG_ARRAY_LEN')
192192
return (
193193
KApply('Value::Range', (elems,)),
194-
[mlEqualsTrue(eqInt(KApply('sizeList', (elems,)), len))],
195-
KApply('dynamicSize', (len,)),
194+
[mlEqualsTrue(eqInt(KApply('sizeList', (elems,)), l))],
195+
KApply('dynamicSize', (l,)),
196196
)
197197

198198
case ArrayT(element_type, size) if size is not None:

‎kmir/src/kmir/kdist/mir-semantics/kmir.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -546,7 +546,7 @@ An operand may be a `Reference` (the only way a function could access another fu
546546
#setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
547547
...
548548
</k>
549-
<stack> ListItem(StackFrame(_, _, _, _, CALLERLOCALS => CALLERLOCALS[I <- Moved])) _:List
549+
<stack> (ListItem(StackFrame(_, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List
550550
</stack>
551551
requires 0 <=Int I
552552
andBool I <Int size(CALLERLOCALS)

‎kmir/src/kmir/kdist/mir-semantics/rt/data.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -739,14 +739,14 @@ The `getTyOf` helper applies the projections from the `Place` to determine the `
739739
[preserves-definedness] // valid map lookup and sort coercion
740740
741741
syntax Int ::= #lookupDiscriminant ( TypeInfo , VariantIdx ) [function, total]
742-
| #lookupDiscrAux ( Discriminants , VariantIdx ) [function]
742+
| #lookupDiscrAux ( Discriminants , Int ) [function]
743743
// --------------------------------------------------------------------
744-
rule #lookupDiscriminant(typeInfoEnumType(_, _, DISCRIMINANTS), IDX) => #lookupDiscrAux(DISCRIMINANTS, IDX)
744+
rule #lookupDiscriminant(typeInfoEnumType(_, _, DISCRIMINANTS), variantIdx(IDX)) => #lookupDiscrAux(DISCRIMINANTS, IDX)
745745
requires isInt(#lookupDiscrAux(DISCRIMINANTS, IDX)) [preserves-definedness]
746746
rule #lookupDiscriminant(_OTHER, _) => 0 [owise, preserves-definedness] // default 0. May be undefined behaviour, though.
747747
// --------------------------------------------------------------------
748-
rule #lookupDiscrAux( Discriminant(IDX, RESULT) _ , IDX) => RESULT
749-
rule #lookupDiscrAux( _OTHER:Discriminant MORE:Discriminants, IDX) => #lookupDiscrAux(MORE, IDX) [owise]
748+
rule #lookupDiscrAux( Discriminant(RESULT) _ , IDX) => RESULT requires IDX ==Int 0
749+
rule #lookupDiscrAux( _:Discriminant MORE:Discriminants, IDX) => #lookupDiscrAux(MORE, IDX -Int 1) requires 0 <Int IDX [owise]
750750
```
751751

752752
```k

‎kmir/src/kmir/kdist/mir-semantics/ty.md‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -256,18 +256,20 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
256256
257257
// additional sort to provide type information in stable-mir-json
258258
syntax TypeInfo ::= typeInfoPrimitiveType(PrimitiveType) [symbol(TypeInfo::PrimitiveType), group(mir-enum)]
259-
| typeInfoEnumType(MIRString, AdtDef, Discriminants) [symbol(TypeInfo::EnumType) , group(mir-enum---name--adt-def--discriminants)]
259+
| typeInfoEnumType(MIRString, AdtDef, Discriminants)
260+
[symbol(TypeInfo::EnumType) , group(mir-enum---name--adt-def--discriminants)]
260261
| typeInfoStructType(MIRString, AdtDef, Tys) [symbol(TypeInfo::StructType) , group(mir-enum---name--adt-def--fields)]
261262
| typeInfoUnionType(MIRString, AdtDef) [symbol(TypeInfo::UnionType) , group(mir-enum---name--adt-def)]
262-
| typeInfoArrayType(Ty, MaybeTyConst) [symbol(TypeInfo::ArrayType) , group(mir-enum)]
263-
| typeInfoPtrType(Ty) [symbol(TypeInfo::PtrType) , group(mir-enum)]
264-
| typeInfoRefType(Ty) [symbol(TypeInfo::RefType) , group(mir-enum)]
263+
| typeInfoArrayType(Ty, MaybeTyConst) [symbol(TypeInfo::ArrayType) , group(mir-enum---elem-type--size)]
264+
| typeInfoPtrType(Ty) [symbol(TypeInfo::PtrType) , group(mir-enum---pointee-type)]
265+
| typeInfoRefType(Ty) [symbol(TypeInfo::RefType) , group(mir-enum---pointee-type)]
265266
| typeInfoTupleType(Tys) [symbol(TypeInfo::TupleType) , group(mir-enum---types)]
266267
| typeInfoFunType(MIRString) [symbol(TypeInfo::FunType) , group(mir-enum)]
268+
| "VoidType" [symbol(TypeInfo::VoidType) , group(mir-enum)]
267269
268270
269271
// discriminant information for enum types
270-
syntax Discriminant ::= Discriminant ( VariantIdx , MIRInt ) [group(mir)]
272+
syntax Discriminant ::= Discriminant ( MIRInt ) [group(mir-int)]
271273
272274
syntax Discriminants ::= List{Discriminant, ""} [group(mir-list), symbol(Discriminants::append), terminator-symbol(Discriminants::empty)]
273275

‎kmir/src/kmir/linker.py‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -72,18 +72,18 @@ def apply_offset_typeInfo(typeinfo: dict, offset: int) -> dict:
7272
# 'PrimitiveType' in typeinfo:
7373
if 'EnumType' in typeinfo:
7474
typeinfo['EnumType']['adt_def'] = typeinfo['EnumType']['adt_def'] + offset
75+
typeinfo['EnumType']['fields'] = [[x + offset for x in l] for l in typeinfo['EnumType']['fields']]
7576
elif 'StructType' in typeinfo:
7677
typeinfo['StructType']['fields'] = [x + offset for x in typeinfo['StructType']['fields']]
7778
typeinfo['StructType']['adt_def'] = typeinfo['StructType']['adt_def'] + offset
7879
elif 'UnionType' in typeinfo:
7980
typeinfo['UnionType']['adt_def'] = typeinfo['UnionType']['adt_def'] + offset
8081
elif 'ArrayType' in typeinfo:
81-
assert isinstance(typeinfo['ArrayType'], list)
82-
typeinfo['ArrayType'][0] = typeinfo['ArrayType'][0] + offset
82+
typeinfo['ArrayType']['elem_type'] = typeinfo['ArrayType']['elem_type'] + offset
8383
elif 'PtrType' in typeinfo:
84-
typeinfo['PtrType'] = typeinfo['PtrType'] + offset
84+
typeinfo['PtrType']['pointee_type'] = typeinfo['PtrType']['pointee_type'] + offset
8585
elif 'RefType' in typeinfo:
86-
typeinfo['RefType'] = typeinfo['RefType'] + offset
86+
typeinfo['RefType']['pointee_type'] = typeinfo['RefType']['pointee_type'] + offset
8787
elif 'TupleType' in typeinfo:
8888
typeinfo['TupleType']['types'] = [x + offset for x in typeinfo['TupleType']['types']]
8989
# 'FunType' in typeinfo:

‎kmir/src/kmir/smir.py‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -255,7 +255,7 @@ def _primty_from_json(typeinfo: str | dict) -> PrimitiveType:
255255
class EnumT(TypeMetadata):
256256
name: str
257257
adt_def: int
258-
discriminants: dict
258+
discriminants: list[int]
259259

260260

261261
@dataclass
@@ -302,7 +302,7 @@ def metadata_from_json(typeinfo: dict) -> TypeMetadata:
302302
return _primty_from_json(typeinfo['PrimitiveType'])
303303
elif 'EnumType' in typeinfo:
304304
info = typeinfo['EnumType']
305-
discriminants = dict(info['discriminants'])
305+
discriminants = list(info['discriminants'])
306306
return EnumT(name=info['name'], adt_def=info['adt_def'], discriminants=discriminants)
307307
elif 'StructType' in typeinfo:
308308
return StructT(
@@ -312,13 +312,12 @@ def metadata_from_json(typeinfo: dict) -> TypeMetadata:
312312
return UnionT(typeinfo['UnionType']['name'], typeinfo['UnionType']['adt_def'])
313313
elif 'ArrayType' in typeinfo:
314314
info = typeinfo['ArrayType']
315-
assert isinstance(info, list)
316-
length = None if info[1] is None else _decode(info[1]['kind']['Value'][1]['bytes'])
317-
return ArrayT(info[0], length)
315+
length = None if info['size'] is None else _decode(info['size']['kind']['Value'][1]['bytes'])
316+
return ArrayT(info['elem_type'], length)
318317
elif 'PtrType' in typeinfo:
319-
return PtrT(typeinfo['PtrType'])
318+
return PtrT(typeinfo['PtrType']['pointee_type'])
320319
elif 'RefType' in typeinfo:
321-
return RefT(typeinfo['RefType'])
320+
return RefT(typeinfo['RefType']['pointee_type'])
322321
elif 'TupleType' in typeinfo:
323322
return TupleT(typeinfo['TupleType']['types'])
324323
elif 'FunType' in typeinfo:

0 commit comments

Comments
 (0)