From 4d6eb7e5d5ce6fdb8c9b35d701e13d6609948c8c Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 25 Apr 2025 18:50:40 -0500 Subject: [PATCH 1/8] Create references for symbolic values --- .../symbolic/kmir-symbolic-locals.md | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md index 1cbbcfccf..05b3df654 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md @@ -86,6 +86,28 @@ module KMIR-SYMBOLIC-LOCALS [symbolic] requires 0 #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT ) + => #reserveSymbolicsFor( localDecl(REFTY, span(-1), MUT) .LocalDecls, 1 ) // Reserve a symbolic value for the type referenced and put it onto the locals + ~> #reserveSymbolicReference(TY, MUT) // Create a stack frame and move the value there. Make the reference for it and + // put it onto the locals. + ~> #reserveSymbolicsFor( LOCALS:LocalDecls, COUNT -Int 1 ) // Reserve the rest of the locals + ... + + ... TY |-> typeInfoRefType ( REFTY ) ... + requires 0 #reserveSymbolicReference(TY, MUT) => .K + ... + + ... ListItem( VAL ) => ListItem( typedValue( Reference( size(STACK) +Int 1, place(local(0), .ProjectionElems), MUT ), TY, MUT ) ) + STACK => STACK ListItem( StackFrame( ty(-1), place(local(-1), .ProjectionElems), noBasicBlockIdx, unwindActionUnreachable, ListItem( VAL ) ) ) +``` + ## Arbitrary Values ```k From 957f9b8be61b7ced7212ff61025fe91d31e28a0b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 28 Apr 2025 11:08:50 +1000 Subject: [PATCH 2/8] Draft code: structs, enums, slices. Arrays TODO --- .../symbolic/kmir-symbolic-locals.md | 63 +++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md index 05b3df654..ad0524342 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md @@ -108,6 +108,69 @@ module KMIR-SYMBOLIC-LOCALS [symbolic] STACK => STACK ListItem( StackFrame( ty(-1), place(local(-1), .ProjectionElems), noBasicBlockIdx, unwindActionUnreachable, ListItem( VAL ) ) ) ``` +## Arrays and Slices + +Slices have an unknown size and need to be abstracted as variables. + +```k + rule #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT ) + => #reserveSymbolicsFor( LOCALS:LocalDecls, COUNT -Int 1 ) + ... + + ... .List => ListItem(typedValue( Range(?_SLICE), TY, MUT)) + ... TY |-> typeInfoArrayType ( _ELEMTY, noTyConst ) ... + requires 0 #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT ) + // => #reserveSymbolicsFor( LOCALS:LocalDecls, COUNT -Int 1 ) + // ... + // + // // FIXME must recursively create each element using reserveSymbolicsFor + // ... .List => ListItem(typedValue( Range(#mkSymbolicList(ELEMTY, MUT, #readTyConstInt(LEN, TYPES))), TY, MUT)) + // (... TY |-> typeInfoArrayType ( ELEMTY, someTyConst(LEN) ) ...) #as TYPES + // requires 0 .List + // requires N <=Int 0 + + // rule #mkSymbolicList(TY, MUT, N) => ListItem(typedValue(?ARRAY_ELEM, TY, MUT)) #mkSymbolicList(TY, MUT, N -Int 1) + // requires 0 #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT ) + => #reserveSymbolicsFor( LOCALS:LocalDecls, COUNT -Int 1 ) + ... + + ... .List => ListItem(typedValue( Aggregate(variantIdx(?_ENUM_IDX), ?_ENUM_ARGS), TY, MUT)) + ... TY |-> typeInfoEnumType ( _, _, _ ) ... + requires 0 #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT ) + => #reserveSymbolicsFor( LOCALS:LocalDecls, COUNT -Int 1 ) + ... + + ... .List => ListItem(typedValue( Aggregate(variantIdx(0), ?_STRUCT_ARGS), TY, MUT)) + ... TY |-> typeInfoStructType ( _, _ ) ... + requires 0 Date: Mon, 28 Apr 2025 12:24:51 +1000 Subject: [PATCH 3/8] WIP new approach to producing lists of symbolic arguments --- .../symbolic/kmir-symbolic-locals.md | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md index ad0524342..d8d95a05b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md @@ -125,6 +125,29 @@ Slices have an unknown size and need to be abstracted as variables. Arrays have statically known size and can be created with full list structure and symbolic array elements: ```k + syntax KItem ::= #symbolicArgsFor ( LocalDecls ) + | #symbolicArgsAux ( List , LocalDecls ) // with accumulator + | #symbolicArgsAux2 ( List , LocalDecls ) // with accumulator + | #symbolicArg ( LocalDecl, Map ) + + rule #symbolicArgsFor(LOCALS) => #symbolicArgsAux(.List, LOCALS) ... + + rule #symbolicArgsAux(ACC, .LocalDecls) => ACC ... + + rule #symbolicArgsAux(ACC, DECL:LocalDecl REST) + => #symbolicArg(DECL, TYPES) + ~> #symbolicArgsAux2(ACC, REST) + ... + + TYPES + + rule TL:TypedLocal ~> #symbolicArgsAux2(ACC, REST) + => #symbolicArgsAux(ACC ListItem(TL), REST) + ... + + + + // rule #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT ) // => #reserveSymbolicsFor( LOCALS:LocalDecls, COUNT -Int 1 ) // ... From 02e69bbdd1f4a2f3dcd05281aa93f729a33763f9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 28 Apr 2025 15:03:35 +1000 Subject: [PATCH 4/8] More draft code for new approach, used in array implementation --- .../symbolic/kmir-symbolic-locals.md | 167 ++++++++++++++++-- 1 file changed, 148 insertions(+), 19 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md index d8d95a05b..dcf19bd06 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md @@ -8,6 +8,8 @@ requires "../kmir.md" module KMIR-SYMBOLIC-LOCALS [symbolic] imports KMIR-CONTROL-FLOW + imports LIST + rule #execFunction( monoItem( SYMNAME, @@ -124,49 +126,177 @@ Slices have an unknown size and need to be abstracted as variables. Arrays have statically known size and can be created with full list structure and symbolic array elements: +```k + rule #reserveSymbolicsFor( localDecl(TY, SPAN, MUT) LOCALS:LocalDecls, COUNT ) + => #mkArrayElems(ELEMTY, SPAN, MUT, LEN) + ~> #mkSymbolicArray(TY, MUT) + ~> #reserveSymbolicsFor( LOCALS, COUNT -Int 1) + ... + + ... TY |-> typeInfoArrayType ( ELEMTY, someTyConst(tyConst(LEN, _)) ) ... + requires 0 #mkArrayElems(TY, SPAN, MUT, LEN) + => #symbolicArgsAux( .List, asLocalDecls(makeList(readTyConstInt(LEN, TYPES), localDecl(TY, SPAN, MUT)))) + ... + + TYPES + requires isInt(readTyConstInt(LEN, TYPES)) + [preserves-definedness] + + syntax LocalDecls ::= asLocalDecls ( List ) [function] + + rule asLocalDecls(.List) => .LocalDecls + + rule asLocalDecls(ListItem(DECL:LocalDecl) REST) => DECL asLocalDecls(REST) + + rule asLocalDecls(ListItem(_OTHER) REST) => asLocalDecls(REST) [owise] + + rule ELEMS:List ~> #mkSymbolicArray(TY, MUT) => .K + ... + + LOCALS => LOCALS ListItem(typedValue(Range(ELEMS), TY, MUT)) +``` + +# New Code to generate symbolic references in a list + +DRAFT CODE. TODO: use wrappers with heating/cooling + ```k syntax KItem ::= #symbolicArgsFor ( LocalDecls ) | #symbolicArgsAux ( List , LocalDecls ) // with accumulator | #symbolicArgsAux2 ( List , LocalDecls ) // with accumulator - | #symbolicArg ( LocalDecl, Map ) + | #symbolicArg ( LocalDecl ) rule #symbolicArgsFor(LOCALS) => #symbolicArgsAux(.List, LOCALS) ... rule #symbolicArgsAux(ACC, .LocalDecls) => ACC ... rule #symbolicArgsAux(ACC, DECL:LocalDecl REST) - => #symbolicArg(DECL, TYPES) + => #symbolicArg(DECL) ~> #symbolicArgsAux2(ACC, REST) ... - TYPES rule TL:TypedLocal ~> #symbolicArgsAux2(ACC, REST) => #symbolicArgsAux(ACC ListItem(TL), REST) ... +``` + +## Integers + +```k + // Unsigned + rule #symbolicArg(localDecl(TY, _, MUT)) + => typedValue( Integer(?INT:Int, #bitWidth(PRIMTY), false), TY, MUT ) + ... + + ... TY |-> typeInfoPrimitiveType ( primTypeUint( PRIMTY ) ) ... + ensures #intConstraints( ?INT, PRIMTY ) + + // Signed + rule #symbolicArg(localDecl(TY, _, MUT)) + => typedValue( Integer(?INT:Int, #bitWidth(PRIMTY), true), TY, MUT ) + ... + + ... TY |-> typeInfoPrimitiveType ( primTypeInt( PRIMTY ) ) ... + ensures #intConstraints( ?INT, PRIMTY ) + + syntax Bool ::= #intConstraints( Int, InTy ) [function, total] + + rule #intConstraints( X, TY:IntTy ) => 0 -Int (2 ^Int (#bitWidth(TY) -Int 1)) <=Int X andBool X 0 <=Int X andBool X #symbolicArg( localDecl(TY, _, MUT) ) + => typedValue( BoolVal( ?_BOOL:Bool ), TY, MUT ) + ... + + ... TY |-> typeInfoPrimitiveType ( primTypeBool ) ... +``` + +## References + +```k + rule #symbolicArg( localDecl(TY, SPAN, MUT) ) + => #symbolicArg( localDecl(REFTY, SPAN, MUT) ) // Create a symbolic value for the type + ~> #symbolicRef(TY, MUT) // Move created value to stack frame and create reference + ... + + ... TY |-> typeInfoRefType ( REFTY ) ... + + syntax KItem ::= #symbolicRef(Ty, Mutability) + + rule VAL:TypedValue ~> #symbolicRef(TY, MUT) + => typedValue( Reference( 1, place(local(size(LOCALS)), .ProjectionElems), MUT ), TY, MUT ) + ... + + ListItem( StackFrame( _, _, _, _, LOCALS => LOCALS ListItem( VAL ) ) ) ... + // FIXME assumes a stack frame exists on the stack +``` + +## Arrays and Slices + +Slices have an unknown length, so the list of elements is necessarily symbolic. + +```k + rule #symbolicArg( localDecl(TY, _, MUT) ) + => typedValue( Range(?_SLICE), TY, MUT) + ... + + ... TY |-> typeInfoArrayType ( _ELEMTY, noTyConst ) ... +``` + + Arrays have statically known size and can be created with full list structure and symbolic array elements: + +```k + rule #symbolicArg( localDecl(TY, SPAN, MUT) ) + => #mkArrayElems(ELEMTY, SPAN, MUT, LEN) + ~> #symbolicArray(TY, MUT) + ... + + ... TY |-> typeInfoArrayType ( ELEMTY, someTyConst(tyConst(LEN, _)) ) ... + + syntax KItem ::= #symbolicArray ( Ty , Mutability ) + rule ELEMS:List ~> #symbolicArray(TY, MUT) + => typedValue( Range(ELEMS), TY, MUT) + ... + +``` + +## Enums and Structs +For `enum` types, it cannot be determined which variant is used, therefore the argument list is a variable. - // rule #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT ) - // => #reserveSymbolicsFor( LOCALS:LocalDecls, COUNT -Int 1 ) - // ... - // - // // FIXME must recursively create each element using reserveSymbolicsFor - // ... .List => ListItem(typedValue( Range(#mkSymbolicList(ELEMTY, MUT, #readTyConstInt(LEN, TYPES))), TY, MUT)) - // (... TY |-> typeInfoArrayType ( ELEMTY, someTyConst(LEN) ) ...) #as TYPES - // requires 0 #symbolicArg( localDecl(TY, _, MUT) ) + => typedValue( Aggregate(variantIdx(?_ENUM_IDX), ?_ENUM_ARGS), TY, MUT) + ... + + ... TY |-> typeInfoEnumType ( _, _, _ ) ... +``` - // syntax List ::= #mkSymbolicList ( Ty , Mutability, Int ) [function, total] +For structs, we could generate suitable arguments with more type information about the fields. At the time of writing this information is not available, though. - // rule #mkSymbolicList(_, _, N) => .List - // requires N <=Int 0 - - // rule #mkSymbolicList(TY, MUT, N) => ListItem(typedValue(?ARRAY_ELEM, TY, MUT)) #mkSymbolicList(TY, MUT, N -Int 1) - // requires 0 #symbolicArg( localDecl(TY, _, MUT) ) + => typedValue( Aggregate(variantIdx(0), ?_STRUCT_ARGS), TY, MUT) + ... + + ... TY |-> typeInfoStructType ( _, _ ) ... ``` + +# End of new code, old code follows + ## Enums and Structs For `enum` types, it cannot be determined which variant is used, therefore the argument list is a variable. @@ -193,7 +323,6 @@ For structs, we could generate suitable arguments with more type information abo requires 0 Date: Tue, 29 Apr 2025 00:43:01 +0000 Subject: [PATCH 5/8] Set Version: 0.3.124 --- 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 db2d8a209..c232be20e 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.123" +version = "0.3.124" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 617d50163..10e10a41f 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.123' +VERSION: Final = '0.3.124' diff --git a/package/version b/package/version index 07e28cb52..6c93e0fd9 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.123 +0.3.124 From 18a24ed0f0ae3e030ec39ade39a83635fbda5b58 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 30 Apr 2025 12:07:22 +1000 Subject: [PATCH 6/8] remove ambiguity of reserveSymbolicFor rules --- .../kdist/mir-semantics/symbolic/kmir-symbolic-locals.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md index dcf19bd06..cc40c1605 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md @@ -40,11 +40,11 @@ module KMIR-SYMBOLIC-LOCALS [symbolic] ```k syntax KItem ::= #reserveSymbolicsFor( LocalDecls, Int ) - rule #reserveSymbolicsFor( .LocalDecls, _ ) => .K ... + rule #reserveSymbolicsFor( .LocalDecls, _ ) => .K ... [priority(40)] - rule #reserveSymbolicsFor( LOCALS:LocalDecls, 0 ) => .K ... + rule #reserveSymbolicsFor( LOCALS:LocalDecls, N ) => .K ... ... .List => #reserveFor(LOCALS) // No more arguments, treat the rest of the Decls normally - + requires N ==Int 0 ``` ## Integers From 636d434a23da0e69111316aa3936993f40e7ad3d Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 30 Apr 2025 02:07:39 +0000 Subject: [PATCH 7/8] Set Version: 0.3.128 --- 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 d9bc010a6..523f185ac 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.126" +version = "0.3.128" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 468fb9c0c..12b20c923 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.126' +VERSION: Final = '0.3.128' diff --git a/package/version b/package/version index 65010dbc1..dbce0d89d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.126 +0.3.128 From 66058ee431a3f31842f253254274f422239cd88f Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 1 May 2025 04:53:10 +1000 Subject: [PATCH 8/8] add preserves-definedness to symbolic int / uint value generation rules --- .../kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md | 4 ++++ kmir/uv.lock | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md index cc40c1605..2b7b853cc 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md @@ -59,6 +59,7 @@ module KMIR-SYMBOLIC-LOCALS [symbolic] ... TY |-> typeInfoPrimitiveType ( primTypeUint( PRIMTY ) ) ... requires 0 #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT ) @@ -69,6 +70,7 @@ module KMIR-SYMBOLIC-LOCALS [symbolic] ... TY |-> typeInfoPrimitiveType ( primTypeInt( PRIMTY ) ) ... requires 0 ... TY |-> typeInfoPrimitiveType ( primTypeUint( PRIMTY ) ) ... ensures #intConstraints( ?INT, PRIMTY ) + [preserves-definedness] // uint-type // Signed rule #symbolicArg(localDecl(TY, _, MUT)) @@ -205,6 +208,7 @@ DRAFT CODE. TODO: use wrappers with heating/cooling ... TY |-> typeInfoPrimitiveType ( primTypeInt( PRIMTY ) ) ... ensures #intConstraints( ?INT, PRIMTY ) + [preserves-definedness] // int-type syntax Bool ::= #intConstraints( Int, InTy ) [function, total] diff --git a/kmir/uv.lock b/kmir/uv.lock index 2e1d3a991..c650d2022 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -520,7 +520,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.125" +version = "0.3.127" source = { editable = "." } dependencies = [ { name = "kframework" },