Fix offset deref for single elements (#798)

Faulty behaviour when dereferencing pointers after offset was observed
in the P-token proofs, returning an array instead of a single element.
The quick-fix is to project to a single element during `#derefTruncate`
when metadata indicates that a single value is required.

Also adds offset tests to `exec_smir` suite. Closes #764

Author: jberthold

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

@@ -165,16 +165,29 @@ will be `129`.
 
   rule <k> #selectBlock(switchTargets(.Branches, BBIDX), _) => #execBlockIdx(BBIDX) ... </k>
 
-  rule <k> #selectBlock(switchTargets(branch(MI, BBIDX) _, _), V) => #execBlockIdx(BBIDX) ... </k> requires #switchMatch(MI, V) [preserves-definedness]
+  rule <k> #selectBlock(switchTargets(branch(MI, BBIDX) _, _), V) => #execBlockIdx(BBIDX) ... </k>
+    requires #switchMatch(MI, V)
+     andBool #switchCanUse(V)
+    [preserves-definedness]
 
-  rule <k> #selectBlock(switchTargets(branch(MI, _) BRANCHES => BRANCHES, _), V) ... </k> requires notBool #switchMatch(MI, V) [preserves-definedness]
+  rule <k> #selectBlock(switchTargets(branch(MI, _) BRANCHES => BRANCHES, _), V) ... </k>
+    requires notBool #switchMatch(MI, V)
+     andBool #switchCanUse(V)
+    [preserves-definedness]
 
   syntax Bool ::= #switchMatch   ( MIRInt , Value ) [function]
 
   rule #switchMatch(0, BoolVal(B)           ) => notBool B
   rule #switchMatch(1, BoolVal(B)           ) => B
   rule #switchMatch(I, Integer(I2, WIDTH, _)) => I ==Int truncate(I2, WIDTH, Unsigned) requires 0 <Int WIDTH
   rule #switchMatch(I, Integer(I2,   0  , _)) => I ==Int I2
+
+  syntax Bool ::= #switchCanUse ( Value ) [function, total]
+  // ------------------------------------------------------
+  rule #switchCanUse(Integer(_, _, _)) => true
+  rule #switchCanUse(  BoolVal( _ )  ) => true
+  rule #switchCanUse(   thunk( _ )   ) => true
+  rule #switchCanUse(   _OTHER       ) => false [owise]
 ```
 
 `Return` simply returns from a function call, using the information

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

@@ -613,11 +613,19 @@ An attempt to read more elements than the length of the accessed array is undefi
   // helper rewrite to implement truncating slices to required size
   syntax KItem ::= #derefTruncate ( MetadataSize , ProjectionElems )
   // ----------------------------------------------------------------------------------------
-  // no metadata, no change to the value
-  rule <k> #traverseProjection( DEST,         VAL, .ProjectionElems, CTXTS) ~> #derefTruncate(noMetadataSize, PROJS)
+  // values other than `Range` do not have metadata anyway, they are passed along unchanged
+  rule <k> #traverseProjection( DEST,         VAL                , .ProjectionElems, CTXTS) ~> #derefTruncate(noMetadataSize, PROJS)
         => #traverseProjection(DEST, VAL, PROJS, CTXTS)
         ...
        </k>
+    requires notBool isRange(VAL)
+
+  // TODO move these to value.md
+  syntax Bool ::= isRange ( Value ) [function, total]
+  // ------------------------------------------------
+  rule isRange(Range(_)) => true
+  rule isRange( _OTHER ) => false [owise]
+
   // staticSize metadata requires an array of suitable length and truncates it
   rule <k> #traverseProjection( DEST, Range(ELEMS), .ProjectionElems, CTXTS) ~> #derefTruncate(staticSize(SIZE), PROJS)
         => #traverseProjection(DEST, Range(range(ELEMS, 0, size(ELEMS) -Int SIZE)), PROJS, CTXTS)
@@ -630,6 +638,12 @@ An attempt to read more elements than the length of the accessed array is undefi
         ...
        </k>
     requires 0 <=Int SIZE andBool SIZE <=Int size(ELEMS) [preserves-definedness] // range parameters checked
+  // If an array was projected to but no metadata is available, use the head element
+  rule <k> #traverseProjection( DEST, Range(ListItem(VAL) _:List), .ProjectionElems, CTXTS) ~> #derefTruncate(noMetadataSize, PROJS)
+        => #traverseProjection(DEST, VAL, PROJS, CTXTS)
+        ...
+       </k>
+    [preserves-definedness]
 
   // Ref, 0 < OFFSET, 0 < PTR_OFFSET, ToStack
   rule <k> #traverseProjection(

kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.rs

@@ -0,0 +1,8 @@
+fn main() {
+    let arr = [11, 22, 33];
+    let mid_ref = unsafe { arr.get_unchecked(1) };
+    let mid = *mid_ref;
+    assert!(mid == 22);
+    let last = unsafe { arr.get_unchecked(2) };
+    assert!(*last == 33);
+}