From 2c9c6e1b4938795fbf4ca9a2f305dd9180346108 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 9 May 2025 14:42:38 -0400 Subject: [PATCH 1/2] Added nullaryOpAlignOf for primitives --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 16 ++++++++++++ .../kmir/kdist/mir-semantics/rt/numbers.md | 25 +++++++++++++++++++ 2 files changed, 41 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index fac0115fc..e65426e32 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/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 rvalueNullaryOp(nullOpAlignOf, TY) + => + typedValue( + Integer(#alignOf({TYPEMAP[TY]}:>TypeInfo), 64, false), + TyUnknown, + mutabilityNot + ) + ... + + TYPEMAP + requires TY in_keys(TYPEMAP) + andBool isTypeInfo(TYPEMAP[TY]) +``` + #### Other operations `binOpOffset` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md index 7b54e54d0..7d16c36ef 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md +++ b/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 ``` \ No newline at end of file From f938f4acfa96641bd1f07ccafe4ec4caf6afbe34 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 9 May 2025 18:52:41 +0000 Subject: [PATCH 2/2] Set Version: 0.3.155 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 040fd58f2..de1b2f598 100644 --- a/kmir/pyproject.toml +++ b/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 = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index b3414ef65..3bd862c04 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.154' +VERSION: Final = '0.3.155' diff --git a/kmir/uv.lock b/kmir/uv.lock index 6f0c754dd..efb21301a 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.154" +version = "0.3.155" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index 589f2dfa3..9ad723c36 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.154 +0.3.155