Generate symbolic arguments based on function signature (#525)

fixes: #495 

- Creates a symbolic `KMIR-SYMBOLIC-LOCALS` module with symbolic
counterparts to the `#init` and `#execFunction` symbols in `KMIR`.
- Modifies `kmir gen-spec` to use `#initSymbolic` in the generated
claim.

---------

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

Author: gtrepta

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.116"
+version = "0.3.117"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.116'
+VERSION: Final = '0.3.117'

kmir/src/kmir/__main__.py

@@ -105,8 +105,9 @@ def _kmir_gen_spec(opts: GenSpecOpts) -> None:
     config_with_cell_vars, _ = split_config_from(config)
 
     lhs = CTerm(config)
-    new_k_cell = KMIR.Symbols.END_PROGRAM
-    rhs = CTerm(Subst({'K_CELL': new_k_cell})(config_with_cell_vars))
+
+    rhs_subst = Subst({'K_CELL': KMIR.Symbols.END_PROGRAM})
+    rhs = CTerm(rhs_subst(config_with_cell_vars))
     claim, _ = cterm_build_claim(opts.input_file.stem.replace('_', '-'), lhs, rhs)
 
     output_file = opts.output_file

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

@@ -2,6 +2,7 @@
 
 ```k
 requires "kmir-ast.md"
+requires "symbolic/kmir-symbolic-locals.md"
 requires "rt/data.md"
 requires "rt/configuration.md"
 requires "lemmas/kmir-lemmas.md"
@@ -615,5 +616,6 @@ The top-level module `KMIR` includes both the control flow constructs (and trans
 module KMIR
   imports KMIR-CONTROL-FLOW
   imports KMIR-LEMMAS
+  imports KMIR-SYMBOLIC-LOCALS
 
 endmodule

kmir/src/kmir/kdist/mir-semantics/symbolic/kmir-symbolic-locals.md

@@ -0,0 +1,102 @@
+# Symbolic locals for functions
+
+This module contains rules that follow the same structure as `#init` in the KMIR module, however it reads the arguments for the signature of the start symbol and generates symbolic values for them.
+
+```k
+requires "../kmir.md"
+
+module KMIR-SYMBOLIC-LOCALS [symbolic]
+  imports KMIR-CONTROL-FLOW
+
+  rule <k> #execFunction(
+              monoItem(
+                SYMNAME,
+                monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS,RETURNLOCAL:LocalDecl LOCALS:LocalDecls, ARGCOUNT, _, _, _)))
+              ),
+              FUNCTIONNAMES
+            )
+        =>
+           #reserveSymbolicsFor(LOCALS, ARGCOUNT)
+        ~> #execBlock(FIRST)
+         ...
+       </k>
+       <currentFunc> _ => #tyFromName(SYMNAME, FUNCTIONNAMES) </currentFunc>
+       <currentFrame>
+         <currentBody> _ => toKList(BLOCKS) </currentBody>
+         <caller> _ => ty(-1) </caller> // no caller
+         <dest> _ => place(local(-1), .ProjectionElems)</dest>
+         <target> _ => noBasicBlockIdx </target>
+         <unwind> _ => unwindActionUnreachable </unwind>
+         <locals> _ => #reserveFor(RETURNLOCAL) </locals>
+       </currentFrame>
+    requires ARGCOUNT >Int 0
+    [priority(25)]
+```
+
+## Declare symbolic arguments based on their types
+
+```k
+  syntax KItem ::= #reserveSymbolicsFor( LocalDecls, Int )
+
+  rule <k> #reserveSymbolicsFor( .LocalDecls, _ ) => .K ... </k>
+
+  rule <k> #reserveSymbolicsFor( LOCALS:LocalDecls, 0 ) => .K ... </k>
+       <locals> ... .List => #reserveFor(LOCALS) </locals> // No more arguments, treat the rest of the Decls normally
+
+```
+
+## Integers
+
+```k
+  // Unsigned
+  rule <k> #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT        )
+        => #reserveSymbolicsFor(                       LOCALS:LocalDecls, COUNT -Int 1 )
+           ...
+       </k>
+       <locals> ... .List => ListItem(typedValue( Integer(?INT:Int, #bitWidth(PRIMTY), false), TY, MUT )) </locals>
+       <types> ... TY |-> typeInfoPrimitiveType ( primTypeUint( PRIMTY ) ) ... </types>
+    requires 0 <Int COUNT
+    ensures #intConstraints( ?INT, PRIMTY )
+
+  // Signed
+  rule <k> #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT        )
+        => #reserveSymbolicsFor(                       LOCALS:LocalDecls, COUNT -Int 1 )
+           ...
+       </k>
+       <locals> ... .List => ListItem(typedValue( Integer(?INT:Int, #bitWidth(PRIMTY), true), TY, MUT )) </locals>
+       <types> ... TY |-> typeInfoPrimitiveType ( primTypeInt( PRIMTY ) ) ... </types>
+    requires 0 <Int COUNT
+    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 <Int 2 ^Int (#bitWidth(TY) -Int 1)
+  rule #intConstraints( X, TY:UintTy ) => 0                                      <=Int X andBool X <Int 2 ^Int  #bitWidth(TY)
+```
+
+## Boolean Values
+
+```k
+  rule <k> #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT        )
+        => #reserveSymbolicsFor(                       LOCALS:LocalDecls, COUNT -Int 1 )
+           ...
+       </k>
+       <locals> ... .List => ListItem(typedValue( BoolVal( ?_BOOL:Bool ), TY, MUT )) </locals>
+       <types> ... TY |-> typeInfoPrimitiveType ( primTypeBool ) ... </types>
+    requires 0 <Int COUNT
+```
+
+## Arbitrary Values
+
+```k
+  rule <k> #reserveSymbolicsFor( localDecl(TY, _, MUT) LOCALS:LocalDecls, COUNT        )
+        => #reserveSymbolicsFor(                       LOCALS:LocalDecls, COUNT -Int 1 )
+           ...
+       </k>
+       <locals> ... .List => ListItem(typedValue( ?_VAL:Value, TY, MUT )) </locals>
+       <types> ... TY |-> _:TypeInfo ... </types>
+    requires 0 <Int COUNT
+    [owise]
+
+endmodule
+```

package/version

@@ -1 +1 @@
-0.3.116
+0.3.117