Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

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

@@ -2075,12 +2075,18 @@ Since our arithmetic operations signal undefined behaviour on overflow independe
 
 #### "Nullary" operations reifying type information
 
-`nullOpSizeOf`
-`nullOpAlignOf`
-`nullOpOffsetOf(VariantAndFieldIndices)`
+Operation `nullOpSizeOf` returns the size in bytes of a data structure or primitive type, as a `usize`.
+Operation `nullOpAlignOf` returns the required alignment of a data structure or primitive type, as a `usize`.
+This information is read from the layout in the `TypeInfo` if available, or a fixed constant for primitive types.
 
 ```k
 // FIXME: 64 is hardcoded since usize not supported
+rule <k> rvalueNullaryOp(nullOpSizeOf, TY)
+      =>
+           Integer(#sizeOf(lookupTy(TY)), 64, false)
+         ...
+     </k>
+    requires lookupTy(TY) =/=K typeInfoVoidType
 rule <k> rvalueNullaryOp(nullOpAlignOf, TY)
       =>
            Integer(#alignOf(lookupTy(TY)), 64, false)
@@ -2089,6 +2095,8 @@ rule <k> rvalueNullaryOp(nullOpAlignOf, TY)
     requires lookupTy(TY) =/=K typeInfoVoidType
 ```
 
+`nullOpOffsetOf(VariantAndFieldIndices)`
+
 #### Other operations
 
 The unary operation `unOpPtrMetadata`, when given a reference or pointer to a slice, will return the reference or pointer metadata.

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

@@ -147,31 +147,6 @@ This truncation function is instrumental in the implementation of Integer arithm
     [preserves-definedness]
 ```
 
-## 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/src/kmir/kdist/mir-semantics/rt/types.md

@@ -203,6 +203,69 @@ Slices, `str`s  and dynamic types require it, and any `Ty` that `is_sized` does
   rule #zeroSizedType(_) => false [owise]
 ```
 
+## Alignment and Size of Types as per `TypeInfo`
+
+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
+  syntax Int ::= #sizeOf ( TypeInfo )  [function, total]
+               | #alignOf ( TypeInfo ) [function, total]
+
+  // 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]
+  // bool and char
+  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
+  // 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
+  // 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
+  // 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
+  // size of union types: FIXME use layout (currently not in K AST)
+  // rule #sizeOf(typeInfoUnionType(_, _)) => FIXME
+  // rule #alignOf(typeInfoUnionType(_, _)) => FIXME
+  // 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))
+  // 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)))
+  // other types (fun and void types) have size and alignment 0
+  rule #sizeOf(_)  => 0 [owise]
+  rule #alignOf(_) => 0 [owise]
+```
+
 ```k
 endmodule
 ```

kmir/src/kmir/testing/fixtures.py

@@ -13,6 +13,12 @@
 
     from pytest import FixtureRequest, Parser
 
+import sys
+
+
+def pytest_configure(config) -> None:
+    sys.setrecursionlimit(1000000)
+
 
 def assert_or_update_show_output(actual_text: str, expected_file: Path, *, update: bool) -> None:
     if update:

kmir/src/tests/integration/data/prove-rs/align_and_size.rs

@@ -0,0 +1,208 @@
+use std::mem::{size_of, align_of};
+
+
+fn check_size_and_alignment<T>(size: usize, align: usize){
+    let s = size_of::<T>();
+    let a = align_of::<T>();
+
+    assert_eq!(s, size);
+    assert_eq!(a, align);
+}
+
+
+fn main() {
+    // // Basic integer types
+    check_size_and_alignment::<u8>(1, 1);
+    check_size_and_alignment::<u32>(4, 4);
+
+    check_size_and_alignment::<u8>(1, 1);
+    
+    check_size_and_alignment::<i8>(1, 1);
+    
+    check_size_and_alignment::<u16>(2, 2);
+    
+    check_size_and_alignment::<i16>(2, 2);
+    
+    check_size_and_alignment::<u32>(4, 4);
+    
+    check_size_and_alignment::<i32>(4, 4);
+    
+    check_size_and_alignment::<u64>(8, 8);
+    
+    check_size_and_alignment::<i64>(8, 8);
+    
+    check_size_and_alignment::<u128>(16, 16);
+    
+    check_size_and_alignment::<i128>(16, 16);
+    
+    // // Floating point types
+    check_size_and_alignment::<f32>(4, 4);
+    
+    check_size_and_alignment::<f64>(8, 8);
+    
+    // // Other basic types
+    check_size_and_alignment::<bool>(1, 1);
+    
+    check_size_and_alignment::<char>(4, 4);
+    
+    // // Pointer-sized types (64-bit)
+    check_size_and_alignment::<usize>(8, 8);
+    
+    check_size_and_alignment::<isize>(8, 8);
+    
+    check_size_and_alignment::<&u32>(8, 8);
+    
+    check_size_and_alignment::<*const u32>(8, 8);
+    
+    check_size_and_alignment::<*mut u32>(8, 8);
+    
+    // Fat pointers (2x pointer size on 64-bit)
+    check_size_and_alignment::<&[u32]>(16, 8);
+    
+    // check_size_and_alignment::<&str>(16, 8);
+    
+    check_size_and_alignment::<&mut [u32]>(16, 8);
+    
+    // // Arrays
+    check_size_and_alignment::<[u8; 0]>(0, 1);
+    
+    check_size_and_alignment::<[u8; 4]>(4, 1);
+    
+    check_size_and_alignment::<[u8; 16]>(16, 1);
+    
+    check_size_and_alignment::<[u32; 4]>(16, 4);
+    
+    check_size_and_alignment::<[u64; 3]>(24, 8);
+    
+    // // Tuples
+    check_size_and_alignment::<()>(0, 1);
+    
+    check_size_and_alignment::<(u8,)>(1, 1);
+    
+    check_size_and_alignment::<(u8, u8)>(2, 1);
+    
+    check_size_and_alignment::<(u8, u16)>(4, 2);
+    
+    check_size_and_alignment::<(u8, u32)>(8, 4);
+    
+    check_size_and_alignment::<(u8, u64)>(16, 8);
+    
+    check_size_and_alignment::<(u32, u32)>(8, 4);
+    
+    check_size_and_alignment::<(u64, u8, u64)>(24, 8);
+    
+    // rustc will permute fields (less padding)
+    #[allow(dead_code)]
+    struct Padded {
+        a: u8,
+        b: u64,
+        c: u8,
+    }
+    check_size_and_alignment::<Padded>(16, 8);
+    
+    // cannot permute fields
+    #[allow(dead_code)]
+    #[repr(C)]
+    struct ReprC {
+        a: u8,
+        b: u64,
+        c: u8,
+    }
+    check_size_and_alignment::<ReprC>(24, 8);
+    
+    #[allow(dead_code)]
+    #[repr(packed)]
+    struct ReprPacked {
+        a: u8,
+        b: u64,
+        c: u8,
+    }
+    check_size_and_alignment::<ReprPacked>(10, 1);
+    
+    #[allow(dead_code)]
+    struct SmallStruct {
+        a: u8,
+        b: u8,
+        c: u8,
+    }
+    check_size_and_alignment::<SmallStruct>(3, 1);
+    
+    #[allow(dead_code)]
+    struct AlignedStruct {
+        a: u32,
+        b: u32,
+    }
+    check_size_and_alignment::<AlignedStruct>(8, 4);
+    
+    #[allow(dead_code)]
+    #[repr(align(16))]
+    struct Align16 {
+        a: u8,
+    }
+    check_size_and_alignment::<Align16>(16, 16);
+    
+    #[allow(dead_code)]
+    #[repr(align(32))]
+    struct Align32 {
+        a: u32,
+    }
+    check_size_and_alignment::<Align32>(32, 32);
+    
+    // Enums
+    #[allow(dead_code)]
+    enum SimpleEnum {
+        A,
+        B,
+        C,
+    }
+    check_size_and_alignment::<SimpleEnum>(1, 1);
+    
+    #[allow(dead_code)]
+    enum EnumWithData {
+        Variant1(u32),
+        Variant2(u64),
+    }
+    check_size_and_alignment::<EnumWithData>(16, 8);
+    
+    #[allow(dead_code)]
+    enum ComplexEnum {
+        Small(u8),
+        Medium(u32),
+        Large(u64, u64),
+    }
+    check_size_and_alignment::<ComplexEnum>(24, 8);
+    
+    // // Option optimization
+    check_size_and_alignment::<Option<u32>>(8, 4);
+    
+    check_size_and_alignment::<Option<u64>>(16, 8);
+    
+    // Null pointer optimization
+    check_size_and_alignment::<Option<&u32>>(8, 8);
+    
+    check_size_and_alignment::<Option<Box<u32>>>(8, 8);
+    
+    // Result
+    check_size_and_alignment::<Result<u32, u32>>(8, 4);
+    
+    check_size_and_alignment::<Result<u64, u8>>(16, 8);
+    
+    // Zero-sized types
+    struct ZeroSized;
+    check_size_and_alignment::<ZeroSized>(0, 1);
+    
+    struct PhantomStruct<T> {
+        _marker: std::marker::PhantomData<T>,
+    }
+    check_size_and_alignment::<PhantomStruct<u64>>(0, 1);
+    
+    // // String and Vec (heap-allocated)
+    check_size_and_alignment::<String>(24, 8);
+    
+    check_size_and_alignment::<Vec<u32>>(24, 8);
+    
+    check_size_and_alignment::<Box<u32>>(8, 8);
+    
+    check_size_and_alignment::<Box<[u32]>>(16, 8);
+
+}