Added nullaryOpAlignOf for primitives (#578)

`nullaryOpAlignOf` for primitives:
- Returns correct values for `u{8,16,32,64,128}`, `i{8,16,32,64,128}`,
`bool`, `char`, `floats`;
- Assumes `usize` and `isize` are `64bit`;
- Hardcoded return size of `64bit` since `isize` and `usize` assume
`64bit` currently;

We already have tests that trigger this however they are going to
require `thunk` to be implemented to get past the casts.

Also I feel alignment should be platform specific, so I added a FIXME
because I believe this values are essentially assumptions. Or am I
misunderstanding?

---------

Co-authored-by: devops <[email protected]>

Author: dkcumming

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.154"
+version = "0.3.155"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.154'
+VERSION: Final = '0.3.155'

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

@@ -1305,6 +1305,22 @@ One important use case of `UbChecks` is to determine overflows in unchecked arit
 `nullOpAlignOf`
 `nullOpOffsetOf(VariantAndFieldIndices)`
 
+```k
+// FIXME: 64 is hardcoded since usize not supported
+rule <k> rvalueNullaryOp(nullOpAlignOf, TY)
+      =>
+         typedValue(
+           Integer(#alignOf({TYPEMAP[TY]}:>TypeInfo), 64, false),
+           TyUnknown,
+           mutabilityNot
+         )
+         ...
+     </k>
+     <types> TYPEMAP </types>
+    requires TY in_keys(TYPEMAP)
+     andBool isTypeInfo(TYPEMAP[TY])
+```
+
 #### Other operations
 
 `binOpOffset`

kmir/src/kmir/kdist/mir-semantics/rt/numbers.md

@@ -150,6 +150,31 @@ This truncation function is instrumental in the implementation of Integer arithm
     [preserves-definedness] // positive shift, divisor non-zero
 ```
 
+## Alignment of Primitives
+
+```k
+// FIXME: Alignment is platform specific
+syntax Int ::= #alignOf( TypeInfo ) [function]
+rule #alignOf( typeInfoPrimitiveType(primTypeBool) )        => 1
+rule #alignOf( typeInfoPrimitiveType(primTypeChar) )        => 4
+rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyIsize)) )  => 8 // FIXME: Hard coded since usize not implemented
+rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI8)) )     => 1
+rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI16)) )    => 2
+rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI32)) )    => 4
+rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI64)) )    => 8
+rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI128)) )   => 16
+rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyUsize)) ) => 8 // FIXME: Hard coded since usize not implemented
+rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU8)) )    => 1
+rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU16)) )   => 2
+rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU32)) )   => 4
+rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU64)) )   => 8
+rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU128)) )  => 16
+rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF16)) )  => 2
+rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF32)) )  => 4
+rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF64)) )  => 8
+rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF128)) ) => 16
+```
+
 ```k
 endmodule
 ```

kmir/uv.lock

@@ -1 +1 @@
-0.3.154
+0.3.155