Skip to content

Commit 62e2ba3

Browse files
committed
min_align_of_val intrinsic implementation (sized)
1 parent 2943129 commit 62e2ba3

1 file changed

Lines changed: 18 additions & 0 deletions

File tree

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -341,6 +341,24 @@ intrinsic stays stuck on them rather than returning a wrong size).
341341
[preserves-definedness]
342342
```
343343

344+
#### Minimum alignment of a value (`std::intrinsics::min_align_of_val`)
345+
346+
`min_align_of_val` returns the minimum alignment of the value its argument points to.
347+
The pointee type is computed from the argument's type and the alignment from the existing `#alignOf`. Again only statically-sized pointee types are handled here.
348+
Dynamically-sized ones are left for later, so the intrinsic stays stuck if one reaches here.
349+
350+
```k
351+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("min_align_of_val")), ARG:Operand .Operands, DEST, _SPAN)
352+
=> #setLocalValue(DEST, Integer(#alignOf(TYPESMAP, lookupTy(TYPESMAP, {pointeeTy(lookupTy(TYPESMAP, {#extractOperandType(TYPESMAP, ARG, LOCALS)}:>Ty))}:>Ty)), 64, false))
353+
... </k>
354+
<locals> LOCALS </locals>
355+
<types> TYPESMAP </types>
356+
requires isTy(#extractOperandType(TYPESMAP, ARG, LOCALS))
357+
andBool isTy(pointeeTy(lookupTy(TYPESMAP, {#extractOperandType(TYPESMAP, ARG, LOCALS)}:>Ty)))
358+
andBool #metadataSize(TYPESMAP, pointeeTy(lookupTy(TYPESMAP, {#extractOperandType(TYPESMAP, ARG, LOCALS)}:>Ty))) =/=K dynamicSize(1)
359+
[preserves-definedness]
360+
```
361+
344362
```k
345363
endmodule
346364
```

0 commit comments

Comments
 (0)