529 pointer cast corrections (#632)

This became a rather large and pervasive change, adding metadata to the
`Reference` value (not just to pointers).

* `Reference`s now carry metadata which gives the size of the pointee in
case of an array or slice.
* The size of slices (and arrays) is important when dereferencing the
references (or pointers, which is much less common).
* Statically-determined sizes are also carried around to avoid looking
up the size from the `TypeInfo` each time
* when dereferencing arrays, only the expected size is copied. If the
expected size is larger than the actual array, the execution gets stuck.
A new test has been added which is expected to fail on undefined
behaviour (`rustc`-compiled code will instead happily copy random data
into the array, as can be observed by activating the `println`s in the
new test).

Author: jberthold

kmir/src/kmir/kast.py

@@ -5,7 +5,7 @@
 
 from pyk.kast.inner import KApply, KVariable, build_cons
 from pyk.kast.prelude.collections import list_of
-from pyk.kast.prelude.kint import leInt
+from pyk.kast.prelude.kint import eqInt, leInt
 from pyk.kast.prelude.ml import mlEqualsTrue
 from pyk.kast.prelude.utils import token
 
@@ -133,7 +133,7 @@ def run(self, local_types: list[dict]) -> tuple[list[KInner], list[KInner]]:
         return (self.locals + self.pointees, self.constraints)
 
     def _add_local(self, ty: Ty, mutable: bool) -> None:
-        value, constraints = self._symbolic_value(ty, mutable)
+        value, constraints, _ = self._symbolic_value(ty, mutable)
 
         self.locals.append(_typed_value(value, ty, mutable))
         self.constraints += constraints
@@ -143,16 +143,20 @@ def _fresh_var(self, prefix: str) -> KVariable:
         self.counter += 1
         return KVariable(name)
 
-    def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInner]]:
+    def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInner], KInner | None]:
+        # returns: symbolic value of given type, related constraints, related pointer metadata
         match self.smir_info.types.get(ty):
             case Int(info):
-                return int_var(self._fresh_var('ARG_INT'), info.value, True)
+                val, constraints = int_var(self._fresh_var('ARG_INT'), info.value, True)
+                return val, constraints, None
 
             case Uint(info):
-                return int_var(self._fresh_var('ARG_UINT'), info.value, False)
+                val, constraints = int_var(self._fresh_var('ARG_UINT'), info.value, False)
+                return val, constraints, None
 
             case Bool():
-                return bool_var(self._fresh_var('ARG_BOOL'))
+                val, constraints = bool_var(self._fresh_var('ARG_BOOL'))
+                return val, constraints, None
 
             case EnumT(_, _, discriminants):
                 variant_var = self._fresh_var('ARG_VARIDX')
@@ -163,51 +167,62 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                     mlEqualsTrue(leInt(variant_var, token(max_variant))),
                 ]
                 args = self._fresh_var('ENUM_ARGS')
-                return KApply('Value::Aggregate', (KApply('variantIdx', (variant_var,)), args)), idx_range
+                return KApply('Value::Aggregate', (KApply('variantIdx', (variant_var,)), args)), idx_range, None
 
             case StructT(_, _, fields):
                 field_vars: list[KInner] = []
                 field_constraints: list[KInner] = []
                 for _ty in fields:
-                    new_var, new_constraints = self._symbolic_value(_ty, mutable)
+                    new_var, new_constraints, _ = self._symbolic_value(_ty, mutable)
                     field_vars.append(new_var)
                     field_constraints += new_constraints
                 return (
                     KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), list_of(field_vars))),
                     field_constraints,
+                    None,
                 )
 
             case UnionT():
                 args = self._fresh_var('ARG_UNION')
-                return KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), args)), []
+                return KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), args)), [], None
 
             case ArrayT(_, None):
                 elems = self._fresh_var('ARG_ARRAY')
-                return KApply('Value::Range', (elems,)), []
+                len = self._fresh_var('ARG_ARRAY_LEN')
+                return (
+                    KApply('Value::Range', (elems,)),
+                    [mlEqualsTrue(eqInt(KApply('sizeList', (elems,)), len))],
+                    KApply('dynamicSize', (len,)),
+                )
 
             case ArrayT(element_type, size) if size is not None:
                 elem_vars: list[KInner] = []
                 elem_constraints: list[KInner] = []
                 for _ in range(size):
-                    new_var, new_constraints = self._symbolic_value(element_type, mutable)
+                    new_var, new_constraints, _ = self._symbolic_value(element_type, mutable)
                     elem_vars.append(new_var)
                     elem_constraints += new_constraints
-                return KApply('Value::Range', (list_of(elem_vars),)), elem_constraints
+                return (
+                    KApply('Value::Range', (list_of(elem_vars),)),
+                    elem_constraints,
+                    KApply('staticSize', (token(size),)),
+                )
 
             case TupleT(components):
                 elem_vars = []
                 elem_constraints = []
                 for _ty in components:
-                    new_var, new_constraints = self._symbolic_value(_ty, mutable)
+                    new_var, new_constraints, _ = self._symbolic_value(_ty, mutable)
                     elem_vars.append(new_var)
                     elem_constraints += new_constraints
                 return (
                     KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), list_of(elem_vars))),
                     elem_constraints,
+                    None,
                 )
 
             case RefT(pointee_ty):
-                pointee_var, pointee_constraints = self._symbolic_value(pointee_ty, mutable)
+                pointee_var, pointee_constraints, metadata = self._symbolic_value(pointee_ty, mutable)
                 ref = self.ref_offset
                 self.ref_offset += 1
                 self.pointees.append(_typed_value(pointee_var, pointee_ty, mutable))
@@ -218,12 +233,14 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                             token(0),
                             KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))),
                             KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()),
+                            metadata if metadata is not None else KApply('noMetadata', ()),
                         ),
                     ),
                     pointee_constraints,
+                    None,
                 )
             case PtrT(pointee_ty):
-                pointee_var, pointee_constraints = self._symbolic_value(pointee_ty, mutable)
+                pointee_var, pointee_constraints, metadata = self._symbolic_value(pointee_ty, mutable)
                 ref = self.ref_offset
                 self.ref_offset += 1
                 self.pointees.append(_typed_value(pointee_var, pointee_ty, mutable))
@@ -234,12 +251,14 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                             token(0),
                             KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))),
                             KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()),
+                            KApply('PtrEmulation', (metadata if metadata is not None else KApply('noMetadata', ()),)),
                         ),
                     ),
                     pointee_constraints,
+                    None,
                 )
             case other:
                 _LOGGER.warning(f'Missing type information ({other}) for type {ty}')
                 # missing type information, but can assert that this is a value
                 var = self._fresh_var('ARG')
-                return var, [mlEqualsTrue(KApply('isValue', (var,)))]
+                return var, [mlEqualsTrue(KApply('isValue', (var,)))], None

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

@@ -31,6 +31,36 @@ The lists used in the semantics are cons-lists, so only rules with a head elemen
   rule N <Int size(ListItem(_) REST:List) => N -Int 1 <Int size(REST)
     requires 0 <Int N
     [simplification, symbolic(REST)]
+
+  rule 0 <=Int size(_LIST:List) => true [simplification]
+```
+
+The hooked `range` function selects a segment from a list, by removing elements from front and back.
+If nothing is removed, the list remains the same. If all elements are removed, nothing remains.
+
+```k
+  rule range(L:List, 0, 0) => L [simplification]
+
+  rule range(L:List, size(L), 0) => .List [simplification]
+
+  rule range(L:List, 0, size(L)) => .List [simplification]
+
+  rule size(range(L, A, B)) => size(L) -Int A -Int B
+    requires A +Int B <=Int size(L) [simplification, preserves-definedness]
+
+  rule #Ceil(range(L, A, B)) => #Ceil(L) #And #Ceil(A) #And #Ceil(B) #And {true #Equals A +Int B <=Int size(L)} [simplification]
+```
+
+## Simplifications for Int
+
+These are trivial simplifications driven by syntactic equality, which should be present upstream.
+
+```k
+  rule A <=Int A => true [simplification]
+
+  rule A ==Int A => true [simplification]
+
+  rule A -Int A => 0 [simplification]
 ```
 
 ## Simplifications related to the `truncate` function