From bca046ae8d9b690490cff9a31a38b4be01f0d320 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 23 Apr 2025 11:19:02 +0900 Subject: [PATCH 1/6] Added local raw pointer test --- .../data/exec-smir/memory/local-raw.rs | 5 + .../data/exec-smir/memory/local-raw.smir.json | 1953 +++++++++++++++++ 2 files changed, 1958 insertions(+) create mode 100644 kmir/src/tests/integration/data/exec-smir/memory/local-raw.rs create mode 100644 kmir/src/tests/integration/data/exec-smir/memory/local-raw.smir.json diff --git a/kmir/src/tests/integration/data/exec-smir/memory/local-raw.rs b/kmir/src/tests/integration/data/exec-smir/memory/local-raw.rs new file mode 100644 index 000000000..d369e7fe3 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/memory/local-raw.rs @@ -0,0 +1,5 @@ +fn main() { + let mut x: u32 = 3; + let y: *mut u32 = &mut x; + unsafe { *y = 0; } +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/memory/local-raw.smir.json b/kmir/src/tests/integration/data/exec-smir/memory/local-raw.smir.json new file mode 100644 index 000000000..458ef6dfc --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/memory/local-raw.smir.json @@ -0,0 +1,1953 @@ +{ + "name": "local_raw", + "crate_id": 12612019338599006157, + "allocs": [], + "functions": [ + [ + 0, + { + "NormalSym": "_ZN3std2rt19lang_start_internal17h018b8394ba015d86E" + } + ], + [ + 13, + { + "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17hca3e1575e34769d2E" + } + ], + [ + 14, + { + "NormalSym": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h45ef82b44d0382bcE" + } + ], + [ + 19, + { + "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17hf631e6f7e51a8568E" + } + ], + [ + 20, + { + "IntrinsicSym": "black_box" + } + ], + [ + 21, + { + "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h4d3f6389d02c5922E" + } + ], + [ + 23, + { + "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h3f6feba5a40ef10bE" + } + ], + [ + 34, + { + "NoOpSym": "" + } + ] + ], + "uneval_consts": [], + "items": [ + { + "symbol_name": "_ZN3std2rt10lang_start17hc674cf1fa4a61e44E", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::rt::lang_start::<()>", + "id": 0, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "StorageLive": 5 + }, + "span": 1 + }, + { + "kind": { + "StorageLive": 6 + }, + "span": 2 + }, + { + "kind": { + "StorageLive": 8 + }, + "span": 3 + }, + { + "kind": { + "Assign": [ + { + "local": 8, + "projection": [] + }, + { + "Aggregate": [ + { + "Closure": [ + 1, + [ + { + "Type": 1 + }, + { + "Type": 2 + }, + { + "Type": 3 + }, + { + "Type": 4 + } + ] + ] + }, + [ + { + "Copy": { + "local": 1, + "projection": [] + } + } + ] + ] + } + ] + }, + "span": 3 + }, + { + "kind": { + "Assign": [ + { + "local": 7, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + "Shared", + { + "local": 8, + "projection": [] + } + ] + } + ] + }, + "span": 2 + }, + { + "kind": { + "Assign": [ + { + "local": 6, + "projection": [] + }, + { + "Cast": [ + { + "PointerCoercion": "Unsize" + }, + { + "Copy": { + "local": 7, + "projection": [] + } + }, + 5 + ] + } + ] + }, + "span": 2 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 0, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 0, + "id": 0 + } + } + }, + "args": [ + { + "Move": { + "local": 6, + "projection": [] + } + }, + { + "Move": { + "local": 2, + "projection": [] + } + }, + { + "Move": { + "local": 3, + "projection": [] + } + }, + { + "Move": { + "local": 4, + "projection": [] + } + } + ], + "destination": { + "local": 5, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 1 + } + }, + { + "statements": [ + { + "kind": { + "StorageDead": 6 + }, + "span": 5 + }, + { + "kind": { + "Assign": [ + { + "local": 0, + "projection": [] + }, + { + "Use": { + "Copy": { + "local": 5, + "projection": [ + { + "Downcast": 0 + }, + { + "Field": [ + 0, + 6 + ] + } + ] + } + } + } + ] + }, + "span": 6 + }, + { + "kind": { + "StorageDead": 8 + }, + "span": 7 + }, + { + "kind": { + "StorageDead": 5 + }, + "span": 7 + } + ], + "terminator": { + "kind": "Return", + "span": 4 + } + } + ], + "locals": [ + { + "ty": 6, + "span": 8, + "mutability": "Mut" + }, + { + "ty": 7, + "span": 9, + "mutability": "Not" + }, + { + "ty": 6, + "span": 10, + "mutability": "Not" + }, + { + "ty": 8, + "span": 11, + "mutability": "Not" + }, + { + "ty": 9, + "span": 12, + "mutability": "Not" + }, + { + "ty": 10, + "span": 1, + "mutability": "Mut" + }, + { + "ty": 5, + "span": 2, + "mutability": "Mut" + }, + { + "ty": 11, + "span": 2, + "mutability": "Not" + }, + { + "ty": 12, + "span": 3, + "mutability": "Not" + } + ], + "arg_count": 4, + "var_debug_info": [ + { + "name": "main", + "source_info": { + "span": 9, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": 1 + }, + { + "name": "argc", + "source_info": { + "span": 10, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 2, + "projection": [] + } + }, + "argument_index": 2 + }, + { + "name": "argv", + "source_info": { + "span": 11, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 3, + "projection": [] + } + }, + "argument_index": 3 + }, + { + "name": "sigpipe", + "source_info": { + "span": 12, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 4, + "projection": [] + } + }, + "argument_index": 4 + }, + { + "name": "v", + "source_info": { + "span": 6, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 0, + "projection": [] + } + }, + "argument_index": null + } + ], + "spread_arg": null, + "span": 13 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h3f6feba5a40ef10bE", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::rt::lang_start::<()>::{closure#0}", + "id": 1, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "StorageLive": 2 + }, + "span": 16 + }, + { + "kind": { + "StorageLive": 3 + }, + "span": 15 + }, + { + "kind": { + "StorageLive": 4 + }, + "span": 17 + }, + { + "kind": { + "Assign": [ + { + "local": 4, + "projection": [] + }, + { + "Use": { + "Copy": { + "local": 1, + "projection": [ + "Deref", + { + "Field": [ + 0, + 7 + ] + } + ] + } + } + } + ] + }, + "span": 17 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 14, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 13, + "id": 1 + } + } + }, + "args": [ + { + "Move": { + "local": 4, + "projection": [] + } + } + ], + "destination": { + "local": 3, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 15 + } + }, + { + "statements": [ + { + "kind": { + "StorageDead": 4 + }, + "span": 19 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 18, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 14, + "id": 2 + } + } + }, + "args": [ + { + "Move": { + "local": 3, + "projection": [] + } + } + ], + "destination": { + "local": 2, + "projection": [] + }, + "target": 2, + "unwind": "Continue" + } + }, + "span": 16 + } + }, + { + "statements": [ + { + "kind": { + "StorageDead": 3 + }, + "span": 21 + }, + { + "kind": { + "StorageLive": 5 + }, + "span": 22 + }, + { + "kind": { + "Assign": [ + { + "local": 5, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + "Shared", + { + "local": 2, + "projection": [ + { + "Field": [ + 0, + 15 + ] + } + ] + } + ] + } + ] + }, + "span": 22 + }, + { + "kind": { + "StorageLive": 6 + }, + "span": 23 + }, + { + "kind": { + "Assign": [ + { + "local": 6, + "projection": [] + }, + { + "Use": { + "Copy": { + "local": 2, + "projection": [ + { + "Field": [ + 0, + 15 + ] + }, + { + "Field": [ + 0, + 9 + ] + } + ] + } + } + } + ] + }, + "span": 23 + }, + { + "kind": { + "Assign": [ + { + "local": 0, + "projection": [] + }, + { + "Cast": [ + "IntToInt", + { + "Move": { + "local": 6, + "projection": [] + } + }, + 16 + ] + } + ] + }, + "span": 24 + }, + { + "kind": { + "StorageDead": 6 + }, + "span": 25 + }, + { + "kind": { + "StorageDead": 5 + }, + "span": 26 + }, + { + "kind": { + "StorageDead": 2 + }, + "span": 27 + } + ], + "terminator": { + "kind": "Return", + "span": 20 + } + } + ], + "locals": [ + { + "ty": 16, + "span": 28, + "mutability": "Mut" + }, + { + "ty": 11, + "span": 3, + "mutability": "Mut" + }, + { + "ty": 17, + "span": 16, + "mutability": "Mut" + }, + { + "ty": 1, + "span": 15, + "mutability": "Mut" + }, + { + "ty": 7, + "span": 17, + "mutability": "Mut" + }, + { + "ty": 18, + "span": 22, + "mutability": "Mut" + }, + { + "ty": 9, + "span": 23, + "mutability": "Mut" + } + ], + "arg_count": 1, + "var_debug_info": [ + { + "name": "main", + "source_info": { + "span": 9, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [ + "Deref", + { + "Field": [ + 0, + 7 + ] + } + ] + } + }, + "argument_index": null + }, + { + "name": "self", + "source_info": { + "span": 29, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 2, + "projection": [] + } + }, + "argument_index": 1 + }, + { + "name": "self", + "source_info": { + "span": 30, + "scope": 2 + }, + "composite": null, + "value": { + "Place": { + "local": 5, + "projection": [] + } + }, + "argument_index": 1 + } + ], + "spread_arg": null, + "span": 3 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17hca3e1575e34769d2E", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::sys::backtrace::__rust_begin_short_backtrace::", + "id": 2, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 31, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 19, + "id": 3 + } + } + }, + "args": [ + { + "Move": { + "local": 1, + "projection": [] + } + }, + { + "Constant": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 1, + "id": 4 + } + } + } + ], + "destination": { + "local": 0, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 33 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 34, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 20, + "id": 5 + } + } + }, + "args": [ + { + "Constant": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 1, + "id": 4 + } + } + } + ], + "destination": { + "local": 2, + "projection": [] + }, + "target": 2, + "unwind": "Unreachable" + } + }, + "span": 35 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 36 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 37, + "mutability": "Mut" + }, + { + "ty": 7, + "span": 38, + "mutability": "Not" + }, + { + "ty": 1, + "span": 39, + "mutability": "Not" + } + ], + "arg_count": 1, + "var_debug_info": [ + { + "name": "f", + "source_info": { + "span": 38, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": 1 + }, + { + "name": "result", + "source_info": { + "span": 40, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 0, + "projection": [] + } + }, + "argument_index": null + }, + { + "name": "dummy", + "source_info": { + "span": 41, + "scope": 2 + }, + "composite": null, + "value": { + "Const": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 1, + "id": 4 + } + } + }, + "argument_index": 1 + } + ], + "spread_arg": null, + "span": 42 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h2930c7ff67af9629E", + "mono_item_kind": { + "MonoItemFn": { + "name": "<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once", + "id": 3, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 43, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 21, + "id": 6 + } + } + }, + "args": [ + { + "Move": { + "local": 1, + "projection": [ + "Deref" + ] + } + }, + { + "Move": { + "local": 2, + "projection": [] + } + } + ], + "destination": { + "local": 0, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 43 + } + } + ], + "locals": [ + { + "ty": 16, + "span": 43, + "mutability": "Mut" + }, + { + "ty": 22, + "span": 43, + "mutability": "Not" + }, + { + "ty": 1, + "span": 43, + "mutability": "Not" + } + ], + "arg_count": 2, + "var_debug_info": [], + "spread_arg": 2, + "span": 43 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ops8function6FnOnce9call_once17h4d3f6389d02c5922E", + "mono_item_kind": { + "MonoItemFn": { + "name": "<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once", + "id": 3, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 3, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + { + "Mut": { + "kind": "Default" + } + }, + { + "local": 1, + "projection": [] + } + ] + } + ] + }, + "span": 43 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 43, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 23, + "id": 7 + } + } + }, + "args": [ + { + "Move": { + "local": 3, + "projection": [] + } + }, + { + "Move": { + "local": 2, + "projection": [] + } + } + ], + "destination": { + "local": 0, + "projection": [] + }, + "target": 1, + "unwind": { + "Cleanup": 3 + } + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 1, + "projection": [] + }, + "target": 2, + "unwind": "Continue" + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 1, + "projection": [] + }, + "target": 4, + "unwind": "Terminate" + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": "Resume", + "span": 43 + } + } + ], + "locals": [ + { + "ty": 16, + "span": 43, + "mutability": "Mut" + }, + { + "ty": 12, + "span": 43, + "mutability": "Not" + }, + { + "ty": 1, + "span": 43, + "mutability": "Not" + }, + { + "ty": 24, + "span": 43, + "mutability": "Not" + } + ], + "arg_count": 2, + "var_debug_info": [], + "spread_arg": 2, + "span": 43 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ops8function6FnOnce9call_once17hf631e6f7e51a8568E", + "mono_item_kind": { + "MonoItemFn": { + "name": ">::call_once", + "id": 3, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Move": { + "local": 1, + "projection": [] + } + }, + "args": [], + "destination": { + "local": 0, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 43 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 43, + "mutability": "Mut" + }, + { + "ty": 7, + "span": 43, + "mutability": "Not" + }, + { + "ty": 1, + "span": 43, + "mutability": "Not" + } + ], + "arg_count": 2, + "var_debug_info": [], + "spread_arg": 2, + "span": 43 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17h060755156e7a57d6E", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::ptr::drop_in_place::<{closure@std::rt::lang_start<()>::{closure#0}}>", + "id": 4, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 44 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 22, + "span": 44, + "mutability": "Not" + } + ], + "arg_count": 1, + "var_debug_info": [], + "spread_arg": null, + "span": 44 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h45ef82b44d0382bcE", + "mono_item_kind": { + "MonoItemFn": { + "name": "<() as std::process::Termination>::report", + "id": 5, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 0, + "projection": [] + }, + { + "Use": { + "Constant": { + "span": 46, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 1, + "mutability": "Mut" + } + }, + "ty": 17, + "id": 8 + } + } + } + } + ] + }, + "span": 46 + } + ], + "terminator": { + "kind": "Return", + "span": 45 + } + } + ], + "locals": [ + { + "ty": 17, + "span": 47, + "mutability": "Mut" + }, + { + "ty": 1, + "span": 48, + "mutability": "Not" + } + ], + "arg_count": 1, + "var_debug_info": [ + { + "name": "self", + "source_info": { + "span": 48, + "scope": 0 + }, + "composite": null, + "value": { + "Const": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 1, + "id": 4 + } + } + }, + "argument_index": 1 + } + ], + "spread_arg": null, + "span": 49 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN9local_raw4main17he7e120dae1291682E", + "mono_item_kind": { + "MonoItemFn": { + "name": "main", + "id": 6, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 1, + "projection": [] + }, + { + "Use": { + "Constant": { + "span": 51, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 3, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 4, + "mutability": "Mut" + } + }, + "ty": 25, + "id": 9 + } + } + } + } + ] + }, + "span": 51 + }, + { + "kind": { + "Assign": [ + { + "local": 3, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + { + "Mut": { + "kind": "Default" + } + }, + { + "local": 1, + "projection": [] + } + ] + } + ] + }, + "span": 52 + }, + { + "kind": { + "Assign": [ + { + "local": 2, + "projection": [] + }, + { + "AddressOf": [ + "Mut", + { + "local": 3, + "projection": [ + "Deref" + ] + } + ] + } + ] + }, + "span": 52 + }, + { + "kind": { + "Assign": [ + { + "local": 4, + "projection": [] + }, + { + "Cast": [ + "PtrToPtr", + { + "Copy": { + "local": 2, + "projection": [] + } + }, + 26 + ] + } + ] + }, + "span": 50 + }, + { + "kind": { + "Assign": [ + { + "local": 5, + "projection": [] + }, + { + "Cast": [ + "Transmute", + { + "Copy": { + "local": 4, + "projection": [] + } + }, + 27 + ] + } + ] + }, + "span": 50 + }, + { + "kind": { + "Assign": [ + { + "local": 6, + "projection": [] + }, + { + "NullaryOp": [ + "AlignOf", + 25 + ] + } + ] + }, + "span": 50 + }, + { + "kind": { + "Assign": [ + { + "local": 7, + "projection": [] + }, + { + "BinaryOp": [ + "Sub", + { + "Copy": { + "local": 6, + "projection": [] + } + }, + { + "Constant": { + "span": 50, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 8, + "mutability": "Mut" + } + }, + "ty": 27, + "id": 10 + } + } + } + ] + } + ] + }, + "span": 50 + }, + { + "kind": { + "Assign": [ + { + "local": 8, + "projection": [] + }, + { + "BinaryOp": [ + "BitAnd", + { + "Copy": { + "local": 5, + "projection": [] + } + }, + { + "Copy": { + "local": 7, + "projection": [] + } + } + ] + } + ] + }, + "span": 50 + }, + { + "kind": { + "Assign": [ + { + "local": 9, + "projection": [] + }, + { + "BinaryOp": [ + "Eq", + { + "Copy": { + "local": 8, + "projection": [] + } + }, + { + "Constant": { + "span": 50, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 8, + "mutability": "Mut" + } + }, + "ty": 27, + "id": 11 + } + } + } + ] + } + ] + }, + "span": 50 + } + ], + "terminator": { + "kind": { + "Assert": { + "cond": { + "Copy": { + "local": 9, + "projection": [] + } + }, + "expected": true, + "msg": { + "MisalignedPointerDereference": { + "required": { + "Copy": { + "local": 6, + "projection": [] + } + }, + "found": { + "Copy": { + "local": 5, + "projection": [] + } + } + } + }, + "target": 1, + "unwind": "Unreachable" + } + }, + "span": 50 + } + }, + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 2, + "projection": [ + "Deref" + ] + }, + { + "Use": { + "Constant": { + "span": 54, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 4, + "mutability": "Mut" + } + }, + "ty": 25, + "id": 12 + } + } + } + } + ] + }, + "span": 50 + } + ], + "terminator": { + "kind": "Return", + "span": 53 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 55, + "mutability": "Mut" + }, + { + "ty": 25, + "span": 56, + "mutability": "Mut" + }, + { + "ty": 28, + "span": 57, + "mutability": "Not" + }, + { + "ty": 29, + "span": 52, + "mutability": "Mut" + }, + { + "ty": 26, + "span": 50, + "mutability": "Mut" + }, + { + "ty": 27, + "span": 50, + "mutability": "Mut" + }, + { + "ty": 27, + "span": 50, + "mutability": "Mut" + }, + { + "ty": 27, + "span": 50, + "mutability": "Mut" + }, + { + "ty": 27, + "span": 50, + "mutability": "Mut" + }, + { + "ty": 30, + "span": 50, + "mutability": "Mut" + } + ], + "arg_count": 0, + "var_debug_info": [ + { + "name": "x", + "source_info": { + "span": 56, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": null + }, + { + "name": "y", + "source_info": { + "span": 57, + "scope": 2 + }, + "composite": null, + "value": { + "Place": { + "local": 2, + "projection": [] + } + }, + "argument_index": null + } + ], + "spread_arg": null, + "span": 58 + } + } + }, + "details": null + } + ], + "types": [ + [ + 2, + { + "PrimitiveType": { + "Int": "I8" + } + } + ], + [ + 6, + { + "PrimitiveType": { + "Int": "Isize" + } + } + ], + [ + 9, + { + "PrimitiveType": { + "Uint": "U8" + } + } + ], + [ + 10, + { + "EnumType": { + "name": "std::result::Result", + "adt_def": 8, + "discriminants": [ + [ + 0, + 0 + ], + [ + 1, + 1 + ] + ] + } + } + ], + [ + 15, + { + "StructType": { + "name": "std::sys::pal::unix::process::process_common::ExitCode", + "adt_def": 15 + } + } + ], + [ + 16, + { + "PrimitiveType": { + "Int": "I32" + } + } + ], + [ + 17, + { + "StructType": { + "name": "std::process::ExitCode", + "adt_def": 13 + } + } + ], + [ + 25, + { + "PrimitiveType": { + "Uint": "U32" + } + } + ], + [ + 27, + { + "PrimitiveType": { + "Uint": "Usize" + } + } + ], + [ + 30, + { + "PrimitiveType": "Bool" + } + ] + ], + "debug": null +} From 3093afc1839175db11c51f00baba40bd5d209527 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 23 Apr 2025 13:29:28 +0900 Subject: [PATCH 2/6] Basic `Ptr` type added for locals with naieve casts --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 27 ++++++++++++++++++- kmir/src/kmir/kdist/mir-semantics/rt/value.md | 2 +- 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a4fd43085..efe68c2c1 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -831,7 +831,18 @@ A `CopyForDeref` `RValue` has the semantics of a simple `Use(operandCopy(...))`, ```k rule rvalueCopyForDeref(PLACE) => rvalueUse(operandCopy(PLACE)) ... -// AddressOf: not implemented yet +``` + +### Raw Pointers +TODO + +```k +rule rvalueAddressOf( MUTABILITY, PLACE) + => + typedValue( Ptr( 0, PLACE, MUTABILITY), TyUnknown, MUTABILITY ) // TyUnknown and MUTABILITY will be overwritten to the Local's type + ... + + ``` ## Type casts @@ -890,6 +901,20 @@ Error cases for `castKindIntToInt` [owise] ``` +### Pointer Casts + +Casting between two raw pointers. FIXME: No validity checks are currently performed + +```k + rule #cast( typedValue(Ptr(DEPTH, PLACE, PTR_MUT), _TY_FROM, LOCAL_MUT), castKindPtrToPtr, TY_TO) => typedValue(Ptr(DEPTH, PLACE, PTR_MUT), TY_TO, LOCAL_MUT) ... + // TYPEMAP + // requires TY_TO #in TYPEMAP + // requires #is_valid_cast(TY_FROM.layout(), TY_TO.layout()) + + rule #cast( typedValue(VALUE, _TY_FROM, LOCAL_MUT), castKindTransmute, TY_TO) => typedValue(VALUE, TY_TO, LOCAL_MUT) ... + +``` + ### Other type casts Other type casts are not implemented yet. diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index f5a1969b3..b60a1fe94 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -34,7 +34,7 @@ High-level values can be // stack depth (initially 0), place, borrow kind | Range( List ) // homogenous values for array/slice - // | Ptr( Address, MaybeValue ) // FIXME why maybe? why value? + | Ptr( Int, Place, Mutability ) // Same as ref for now until I understand how to handle better // address, metadata for ref/ptr | "Any" // arbitrary value for transmute/invalid ptr lookup From 0bc45b228a33efdb1a683ce17f60e84f5034a21a Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 23 Apr 2025 14:35:08 +0900 Subject: [PATCH 3/6] Added `NullaryOp` `AlignOf` evaluation --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 34 ++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index efe68c2c1..4562dd23f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1357,6 +1357,40 @@ One important use case of `UbChecks` is to determine overflows in unchecked arit `nullOpAlignOf` `nullOpOffsetOf(VariantAndFieldIndices)` +```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 + +rule rvalueNullaryOp(nullOpAlignOf, TY) => typedValue( Integer(#alignOf({TYPEMAP[TY]}:>TypeInfo), 64, false), TyUnknown, mutabilityNot ) ... // FIXME: 64 is hardcoded since usize not supported + TYPEMAP + requires TY in_keys(TYPEMAP) + andBool isTypeInfo(TYPEMAP[TY]) + +``` + #### Other operations `binOpOffset` From aab0f9514d2b12c11d0d7e512fe35cf62fb09f0c Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 23 Apr 2025 05:38:42 +0000 Subject: [PATCH 4/6] Set Version: 0.3.122 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index bf71df0eb..d43c4bc8e 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmir" -version = "0.3.121" +version = "0.3.122" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 171936af8..1345b2f7a 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.121' +VERSION: Final = '0.3.122' diff --git a/package/version b/package/version index b96616520..165ea630e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.121 +0.3.122 From 8c41f44e6c67790ea5e2e90ffef74dca943e6b91 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 23 Apr 2025 16:32:38 +0900 Subject: [PATCH 5/6] Added bitwise operations `^`, `&`, `|` --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 82 +++++++++++++------ .../kmir/kdist/mir-semantics/rt/numbers.md | 29 +++++++ 2 files changed, 85 insertions(+), 26 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 4562dd23f..759856055 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1340,6 +1340,62 @@ The `unOpNot` operation works on boolean and integral values, with the usual sem `binOpShr` `binOpShrUnchecked` +```k + syntax Bool ::= isBitwise ( BinOp ) [function, total] + // -------------------------------------------------- + rule isBitwise(binOpBitXor) => true + rule isBitwise(binOpBitAnd) => true + rule isBitwise(binOpBitOr) => true + rule isBitwise(_) => false [owise] + + syntax Bool ::= isShift ( BinOp ) [function, total] + // ------------------------------------------------ + rule isShift(binOpShl) => true + rule isShift(binOpShlUnchecked) => true + rule isShift(binOpShr) => true + rule isShift(binOpShrUnchecked) => true + rule isShift(_) => false [owise] + + rule onInt(binOpBitXor, X, Y) => X xorInt Y + rule onInt(binOpBitAnd, X, Y) => X &Int Y + rule onInt(binOpBitOr, X, Y) => X |Int Y + + // Only permitting non-shift bitwise operations on same width integers, overflow check not required + rule #compute( + BOP, + typedValue(Integer(ARG1, WIDTH, _), _, _), + typedValue(Integer(ARG2, WIDTH, _), _, _), + false) // unchecked + => + typedValue( + Integer(onInt(BOP, ARG1, ARG2), WIDTH, false), + TyUnknown, + mutabilityNot + ) + requires isBitwise(BOP) + [preserves-definedness] + + rule #compute( + BOP, + typedValue(Ptr(_ARG1, _, _), _, _), + typedValue(Integer(_ARG2, WIDTH, _), _, _), + false) // unchecked + => + typedValue( + Integer(4242, WIDTH, false), + TyUnknown, + mutabilityNot + ) + // typedValue( + // Integer(onInt(BOP, ARG1, ARG2), WIDTH, false), + // TyUnknown, + // mutabilityNot + // ) + requires isBitwise(BOP) + [preserves-definedness] + +``` + #### Nullary operations for activating certain checks @@ -1358,32 +1414,6 @@ One important use case of `UbChecks` is to determine overflows in unchecked arit `nullOpOffsetOf(VariantAndFieldIndices)` ```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 - rule rvalueNullaryOp(nullOpAlignOf, TY) => typedValue( Integer(#alignOf({TYPEMAP[TY]}:>TypeInfo), 64, false), TyUnknown, mutabilityNot ) ... // FIXME: 64 is hardcoded since usize not supported TYPEMAP requires TY in_keys(TYPEMAP) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md index 46cc8f2a5..c434d31c5 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md @@ -153,6 +153,35 @@ 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 1ee2475e10c728326275dce14748562eaee81d7f Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 24 Apr 2025 13:25:47 +0900 Subject: [PATCH 6/6] Updated Ptr with Address and Offset. Added projection update rules --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 73 ++++++++++++++++--- kmir/src/kmir/kdist/mir-semantics/rt/value.md | 4 +- 2 files changed, 65 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 759856055..9231a2adc 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -581,6 +581,58 @@ The solution is to use rewrite operations in a downward pass through the project andBool (FORCE orBool MUT ==K mutabilityMut) [preserves-definedness] + rule #projectedUpdate( + _DEST, + typedValue(Ptr(OFFSET, place(LOCAL, PLACEPROJ), MUT, _ADDRESS, _OFFSET2), _, _), + projectionElemDeref PROJS, + UPDATE, + _CTXTS, + FORCE + ) + => + #projectedUpdate( + toStack(OFFSET, LOCAL), + #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), + appendP(PLACEPROJ, PROJS), // apply ptr (reference) projections first, then rest + UPDATE, + .Contexts, // previous contexts obsolete + FORCE + ) + ... + + STACK + requires 0 #projectedUpdate( + _DEST, + typedValue(Ptr(OFFSET, place(local(I), PLACEPROJ), MUT, _ADDRESS, _OFFSET2), _, _), + projectionElemDeref PROJS, + UPDATE, + _CTXTS, + FORCE + ) + => + #projectedUpdate( + toLocal(I), + {LOCALS[I]}:>TypedLocal, + appendP(PLACEPROJ, PROJS), // apply ptr (reference) projections first, then rest + UPDATE, + .Contexts, // previous contexts obsolete + FORCE + ) + ... + + LOCALS + requires OFFSET ==Int 0 + andBool 0 <=Int I + andBool I #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false) => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) @@ -837,9 +889,10 @@ A `CopyForDeref` `RValue` has the semantics of a simple `Use(operandCopy(...))`, TODO ```k +// FIXME: Address is currently hardcoded to 0 so that the alignment check passes everytime rule rvalueAddressOf( MUTABILITY, PLACE) => - typedValue( Ptr( 0, PLACE, MUTABILITY), TyUnknown, MUTABILITY ) // TyUnknown and MUTABILITY will be overwritten to the Local's type + typedValue( Ptr( 0, PLACE, MUTABILITY, 0, 0), TyUnknown, MUTABILITY ) // TyUnknown and MUTABILITY will be overwritten to the Local's type ... @@ -906,7 +959,12 @@ Error cases for `castKindIntToInt` Casting between two raw pointers. FIXME: No validity checks are currently performed ```k - rule #cast( typedValue(Ptr(DEPTH, PLACE, PTR_MUT), _TY_FROM, LOCAL_MUT), castKindPtrToPtr, TY_TO) => typedValue(Ptr(DEPTH, PLACE, PTR_MUT), TY_TO, LOCAL_MUT) ... + // FIXME: Address and Offset are blindly transferred through + rule #cast( typedValue(Ptr(DEPTH, PLACE, PTR_MUT, ADDRESS, OFFSET), _TY_FROM, LOCAL_MUT), castKindPtrToPtr, TY_TO) + => + typedValue(Ptr(DEPTH, PLACE, PTR_MUT, ADDRESS, OFFSET), TY_TO, LOCAL_MUT) + ... + // TYPEMAP // requires TY_TO #in TYPEMAP // requires #is_valid_cast(TY_FROM.layout(), TY_TO.layout()) @@ -1377,20 +1435,15 @@ The `unOpNot` operation works on boolean and integral values, with the usual sem rule #compute( BOP, - typedValue(Ptr(_ARG1, _, _), _, _), - typedValue(Integer(_ARG2, WIDTH, _), _, _), + typedValue(Ptr(_, _, _, ADDRESS, _), _, _), + typedValue(Integer(VAL, WIDTH, _), _, _), false) // unchecked => typedValue( - Integer(4242, WIDTH, false), + Integer(onInt(BOP, VAL, ADDRESS), WIDTH, false), TyUnknown, mutabilityNot ) - // typedValue( - // Integer(onInt(BOP, ARG1, ARG2), WIDTH, false), - // TyUnknown, - // mutabilityNot - // ) requires isBitwise(BOP) [preserves-definedness] diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index b60a1fe94..1a29f56b2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -34,8 +34,8 @@ High-level values can be // stack depth (initially 0), place, borrow kind | Range( List ) // homogenous values for array/slice - | Ptr( Int, Place, Mutability ) // Same as ref for now until I understand how to handle better - // address, metadata for ref/ptr + | Ptr( Int, Place, Mutability, Int, Int) + // stack depth (initially zero), place, mutablility, address, offset NOTE: First 3 fields are the same as Reference, last are needed for low level instructions | "Any" // arbitrary value for transmute/invalid ptr lookup ```