feat: support terminator call from a function pointer (#894)

- Solve #488

---------

Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

Author: Stevengre

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

@@ -305,21 +305,33 @@ The call stack is not necessarily empty at this point so it is left untouched.
 `Call` is calling another function, setting up its stack frame and
 where the returned result should go.
 
-
 ```k
-  // Intrinsic function call - execute directly without state switching
-  rule [termCallIntrinsic]: <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _
-         =>
-           #execIntrinsic(lookupFunction(#tyOfCall(FUNC)), ARGS, DEST) ~> #continueAt(TARGET)
+  syntax KItem ::= #execTerminatorCall(fty: Ty, func: MonoItemKind, args: Operands, destination: Place, target: MaybeBasicBlockIdx, unwind: UnwindAction)
+
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), _SPAN))
+        => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND)
+        ...
        </k>
-    requires isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
+
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), .ProjectionElems)), ARGS, DEST, TARGET, UNWIND), _SPAN))
+        => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND)
+        ...
+       </k>
+      <locals> LOCALS </locals>
+
+  // Intrinsic function call - execute directly without state switching
+  rule [termCallIntrinsic]:
+        <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND) ~> _
+         => #execIntrinsic(FUNC, ARGS, DEST) ~> #continueAt(TARGET)
+        </k>
+    requires isIntrinsicFunction(FUNC)
 
   // Regular function call - full state switching and stack setup
-  rule [termCallFunction]: <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _
-         =>
-           #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS)
+  rule [termCallFunction]:
+       <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND) ~> _
+        => #setUpCalleeData(FUNC, ARGS)
        </k>
-       <currentFunc> CALLER => #tyOfCall(FUNC) </currentFunc>
+       <currentFunc> CALLER => FTY </currentFunc>
        <currentFrame>
          <currentBody> _ </currentBody>
          <caller> OLDCALLER => CALLER </caller>
@@ -329,7 +341,7 @@ where the returned result should go.
          <locals> LOCALS </locals>
        </currentFrame>
        <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
-    requires notBool isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
+    requires notBool isIntrinsicFunction(FUNC)
 
   syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function]
   rule isIntrinsicFunction(IntrinsicFunction(_)) => true
@@ -338,11 +350,6 @@ where the returned result should go.
   syntax KItem ::= #continueAt(MaybeBasicBlockIdx)
   rule <k> #continueAt(someBasicBlockIdx(TARGET)) => #execBlockIdx(TARGET) ... </k>
   rule <k> #continueAt(noBasicBlockIdx) => .K ... </k>
-
-  syntax Ty ::= #tyOfCall( Operand ) [function, total]
-
-  rule #tyOfCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _)))) => Ty
-  rule #tyOfCall(_) => ty(-1) [owise] // copy, move, non-zero size: not supported
 ```
 
 The local data has to be set up for the call, which requires information about the local variables of a call. This step is separate from the above call stack setup because it needs to retrieve the locals declaration from the body. Arguments to the call are `Operands` which refer to the old locals (`OLDLOCALS` below), and the data is either _copied_ into the new locals using `#setArgs`, or it needs to be _shared_ via references.
@@ -412,7 +419,8 @@ An operand may be a `Reference` (the only way a function could access another fu
      andBool isTypedValue(CALLERLOCALS[I])
     [preserves-definedness] // valid list indexing checked
 
-  rule <k> #setArgFromStack(IDX, operandMove(place(local(I), .ProjectionElems)))
+  // TODO: This is not safe, need to add more checks to this.
+  rule <k> #setArgFromStack(IDX, operandMove(place(local(I), _)))
         =>
            #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
         ...

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

@@ -130,6 +130,17 @@ Constant operands are simply decoded according to their type.
     requires typeInfoVoidType =/=K lookupTy(TY)
 ```
 
+Function pointers are zero-sized constants whose `Ty` is a key in the function table instaed of the type table.
+
+```k
+  rule <k> operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, ty(ID) #as TY, _)))
+        => FunPtr(TY)
+       ...
+       </k>
+    requires typeInfoVoidType ==K lookupTy(TY) // not a valid type info
+     andBool lookupFunction(TY) =/=K monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(ID), noBody ) // valid function Ty
+```
+
 ### Copying and Moving
 
 When an operand is `Copied` by a read, the original remains valid (see `false` passed to `#readProjection`).

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

@@ -51,6 +51,8 @@ The special `Moved` value represents values that have been used and should not b
                                                           [symbol(Value::PtrLocal)]
                    // pointer to a local TypedValue (on the stack)
                    // fields are the same as in Reference
+                 | FunPtr ( Ty )
+                   // function pointer, created by operandConstant only. Ty is a key in the function table
                  | AllocRef ( AllocId , ProjectionElems , Metadata )
                                                           [symbol(Value::AllocRef)]
                    // reference to static allocation, by AllocId, possibly projected, carrying metadata if applicable

kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (42 steps)
+│  (44 steps)
 ├─ 3 (split)
 │   #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 18446744073709
 ┃

kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (225 steps)
+│  (228 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (34 steps)
+│  (35 steps)
 ├─ 3 (split)
 │   #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709
 ┃

kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (112 steps)
+│  (114 steps)
 ├─ 3 (split)
 │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
 ┃
@@ -14,7 +14,7 @@
 ┃  ├─ 4
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
 ┃  │
-┃  │  (5 steps)
+┃  │  (6 steps)
 ┃  └─ 6 (stuck, leaf)
 ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
 ┃
@@ -25,7 +25,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
    │
-   │  (181 steps)
+   │  (182 steps)
    ├─ 7 (terminal)
    │   #EndProgram ~> .K
    │

kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (727 steps)
+│  (736 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (212 steps)
+│  (216 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/prove-rs/488-support-function-pointer-calls.rs

@@ -0,0 +1,27 @@
+use std::convert::TryFrom;
+use std::array;
+
+// inspired by solana-pubkey but very simple code
+#[allow(dead_code)]
+struct EightBytes([u8;8]);
+
+impl From<[u8;8]> for EightBytes {
+    fn from(bytes: [u8;8]) -> Self { Self(bytes) } 
+}
+
+// causing problems with the extraction
+// the `try_from` and `from` from stdlib are not available in the SMIR
+impl TryFrom<&[u8]> for EightBytes {
+    type Error = array::TryFromSliceError;
+    fn try_from(bytes: &[u8]) -> Result<EightBytes, Self::Error> {
+        <[u8;8]>::try_from(bytes).map(Self::from) 
+    }
+}
+
+fn main() {
+    let bytes: [u8;8] = [1,2,3,4,5,6,7,8];
+    let _unused = EightBytes::from(bytes);
+    let slice: &[u8] = &bytes;
+    let thing: Result<EightBytes, _> = EightBytes::try_from(slice);
+    assert!(thing.is_ok());
+}