Updates from master (#781)

* Caching for the LLVM compilation
* more random-running functionality
* `assume` cheatcode
* Discriminant bit width fix
* Optimisations to eliminate `transmute` thunks

Author: jberthold

kmir/src/kmir/__main__.py

@@ -14,7 +14,7 @@
 from pyk.proof.show import APRProofShow
 from pyk.proof.tui import APRProofViewer
 
-from .build import HASKELL_DEF_DIR, LLVM_DEF_DIR, LLVM_LIB_DIR
+from .build import HASKELL_DEF_DIR, LLVM_LIB_DIR
 from .cargo import CargoProject
 from .kmir import KMIR, KMIRAPRNodePrinter
 from .linker import link
@@ -42,8 +42,6 @@
 
 
 def _kmir_run(opts: RunOpts) -> None:
-    kmir = KMIR(HASKELL_DEF_DIR) if opts.haskell_backend else KMIR(LLVM_DEF_DIR)
-
     if opts.file:
         smir_info = SMIRInfo.from_file(Path(opts.file))
     else:
@@ -54,11 +52,17 @@ def _kmir_run(opts: RunOpts) -> None:
         # target = opts.bin if opts.bin else cargo.default_target
         smir_info = cargo.smir_for_project(clean=False)
 
-    with tempfile.TemporaryDirectory() as work_dir:
-        kmir = KMIR.from_kompiled_kore(smir_info, symbolic=opts.haskell_backend, target_dir=work_dir)
+    def run(target_dir: Path):
+        kmir = KMIR.from_kompiled_kore(smir_info, symbolic=opts.haskell_backend, target_dir=target_dir)
         result = kmir.run_smir(smir_info, start_symbol=opts.start_symbol, depth=opts.depth)
         print(kmir.kore_to_pretty(result))
 
+    if opts.target_dir:
+        run(target_dir=opts.target_dir)
+    else:
+        with tempfile.TemporaryDirectory() as target_dir:
+            run(target_dir=Path(target_dir))
+
 
 def _kmir_prove_rs(opts: ProveRSOpts) -> None:
     proof = KMIR.prove_rs(opts)
@@ -185,6 +189,7 @@ def _arg_parser() -> ArgumentParser:
     run_target_selection = run_parser.add_mutually_exclusive_group()
     run_target_selection.add_argument('--bin', metavar='TARGET', help='Target to run')
     run_target_selection.add_argument('--file', metavar='SMIR', help='SMIR json file to execute')
+    run_parser.add_argument('--target-dir', type=Path, metavar='TARGET_DIR', help='SMIR kompilation target directory')
     run_parser.add_argument('--depth', type=int, metavar='DEPTH', help='Depth to execute')
     run_parser.add_argument(
         '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
@@ -313,6 +318,7 @@ def _parse_args(ns: Namespace) -> KMirOpts:
             return RunOpts(
                 bin=ns.bin,
                 file=ns.file,
+                target_dir=ns.target_dir,
                 depth=ns.depth,
                 start_symbol=ns.start_symbol,
                 haskell_backend=ns.haskell_backend,

kmir/src/kmir/decoding.py

@@ -25,12 +25,13 @@
     UintT,
 )
 from .value import (
-    NO_METADATA,
+    NO_SIZE,
     AggregateValue,
     AllocRefValue,
     BoolValue,
     DynamicSize,
     IntValue,
+    Metadata,
     RangeValue,
     StaticSize,
     StrValue,
@@ -120,18 +121,30 @@ def _decode_memory_alloc_or_unable(
                 except KeyError:
                     return UnableToDecodeValue(f'Unknown pointee type: {pointee_ty}')
 
-                metadata = _metadata(pointee_type_info)
+                metadata_size = _metadata_size(pointee_type_info)
 
                 if len(data) == 8:
                     # single slim pointer (assumes usize == u64)
-                    return AllocRefValue(alloc_id=alloc_id, metadata=metadata)
+                    return AllocRefValue(
+                        alloc_id=alloc_id,
+                        metadata=Metadata(
+                            size=metadata_size,
+                            pointer_offset=0,
+                            origin_size=metadata_size,
+                        ),
+                    )
 
-                if len(data) == 16 and metadata == DynamicSize(1):
+                if len(data) == 16 and metadata_size == DynamicSize(1):
                     # sufficient data to decode dynamic size (assumes usize == u64)
                     # expect fat pointer
+                    actual_size = DynamicSize(int.from_bytes(data[8:16], byteorder='little', signed=False))
                     return AllocRefValue(
                         alloc_id=alloc_id,
-                        metadata=DynamicSize(int.from_bytes(data[8:16], byteorder='little', signed=False)),
+                        metadata=Metadata(
+                            size=actual_size,
+                            pointer_offset=0,
+                            origin_size=actual_size,
+                        ),
                     )
 
     return UnableToDecodeValue(f'Unable to decode alloc: {data!r}, of type: {type_info}')
@@ -145,14 +158,14 @@ def _pointee_ty(type_info: TypeMetadata) -> Ty | None:
             return None
 
 
-def _metadata(type_info: TypeMetadata) -> MetadataSize:
+def _metadata_size(type_info: TypeMetadata) -> MetadataSize:
     match type_info:
         case ArrayT(length=None):
             return DynamicSize(1)  # 1 is a placeholder, the actual size is inferred from the slice data
         case ArrayT(length=int() as length):
             return StaticSize(length)
         case _:
-            return NO_METADATA
+            return NO_SIZE
 
 
 def decode_value_or_unable(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMetadata]) -> Value:

kmir/src/kmir/kast.py

@@ -1,6 +1,7 @@
 from __future__ import annotations
 
 import logging
+from itertools import count
 from typing import TYPE_CHECKING, NamedTuple
 
 from pyk.kast.inner import KApply, KSort, KVariable, Subst, build_cons
@@ -11,10 +12,23 @@
 from pyk.kast.prelude.utils import token
 
 from .ty import ArrayT, BoolT, EnumT, IntT, PtrT, RefT, StructT, TupleT, Ty, UintT, UnionT
-from .value import BoolValue, IntValue
+from .value import (
+    NO_SIZE,
+    AggregateValue,
+    BoolValue,
+    DynamicSize,
+    IntValue,
+    Local,
+    Metadata,
+    Place,
+    PtrLocalValue,
+    RangeValue,
+    RefValue,
+    StaticSize,
+)
 
 if TYPE_CHECKING:
-    from collections.abc import Iterable, Mapping, Sequence
+    from collections.abc import Iterable, Iterator, Mapping, Sequence
     from random import Random
     from typing import Any, Final
 
@@ -29,6 +43,9 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
+RANDOM_MAX_ARRAY_LEN: Final = 32
+
+
 LOCAL_0: Final = KApply('newLocal', KApply('ty', token(0)), KApply('Mutability::Not'))
 
 
@@ -474,25 +491,7 @@ def to_kast(self) -> KInner:
 
 
 def _random_locals(random: Random, args: Sequence[_Local], types: Mapping[Ty, TypeMetadata]) -> list[KInner]:
-    res: list[KInner] = [LOCAL_0]
-    pointees: list[KInner] = []
-
-    next_ref = len(args) + 1
-    for arg in args:
-        rvres = _random_value(
-            random=random,
-            local=arg,
-            types=types,
-            next_ref=next_ref,
-        )
-        res.append(rvres.value.to_kast())
-        match rvres:
-            case PointerRes(pointee=pointee):
-                pointees.append(pointee.to_kast())
-                next_ref += 1
-
-    res += pointees
-    return res
+    return _RandomArgGen(random=random, args=args, types=types).run()
 
 
 class SimpleRes(NamedTuple):
@@ -501,55 +500,155 @@ class SimpleRes(NamedTuple):
 
 class ArrayRes(NamedTuple):
     value: TypedValue
-    metadata: MetadataSize
+    metadata_size: MetadataSize
 
 
-class PointerRes(NamedTuple):
-    value: TypedValue
-    pointee: TypedValue
+RandomValueRes = SimpleRes | ArrayRes
 
 
-RandomValueRes = SimpleRes | ArrayRes | PointerRes
+class _RandomArgGen:
+    _random: Random
+    _args: Sequence[_Local]
+    _types: Mapping[Ty, TypeMetadata]
+    _pointees: list[TypedValue]
+    _ref: Iterator[int]
 
+    def __init__(self, *, random: Random, args: Sequence[_Local], types: Mapping[Ty, TypeMetadata]):
+        self._random = random
+        self._args = args
+        self._types = types
+        self._pointees = []
+        self._ref = count(len(args) + 1)
 
-def _random_value(
-    *,
-    random: Random,
-    local: _Local,
-    types: Mapping[Ty, TypeMetadata],
-    next_ref: int,
-) -> RandomValueRes:
-    try:
-        type_info = types[local.ty]
-    except KeyError as err:
-        raise ValueError(f'Unknown type: {local.ty}') from err
-
-    match type_info:
-        case BoolT():
-            return SimpleRes(
-                TypedValue.from_local(
-                    value=_random_bool_value(random),
-                    local=local,
+    def run(self) -> list[KInner]:
+        res: list[KInner] = [LOCAL_0]
+        res.extend(self._random_value(arg).value.to_kast() for arg in self._args)
+        res.extend(pointee.to_kast() for pointee in self._pointees)
+        return res
+
+    def _random_value(self, local: _Local) -> RandomValueRes:
+        try:
+            type_info = self._types[local.ty]
+        except KeyError as err:
+            raise ValueError(f'Unknown type: {local.ty}') from err
+
+        match type_info:
+            case BoolT():
+                return SimpleRes(
+                    TypedValue.from_local(
+                        value=self._random_bool_value(),
+                        local=local,
+                    )
                 )
-            )
-        case IntT() | UintT():
-            return SimpleRes(
-                TypedValue.from_local(
-                    value=_random_int_value(random, type_info),
-                    local=local,
-                ),
-            )
-        case _:
-            raise ValueError(f'Type unsupported for random value generator: {type_info}')
+            case IntT() | UintT():
+                return SimpleRes(
+                    TypedValue.from_local(
+                        value=self._random_int_value(type_info),
+                        local=local,
+                    ),
+                )
+            case EnumT(discriminants=discriminants, fields=fields):
+                return SimpleRes(
+                    TypedValue.from_local(
+                        value=self._random_enum_value(mut=local.mut, discriminants=discriminants, fields=fields),
+                        local=local,
+                    ),
+                )
+            case StructT(fields=tys) | TupleT(components=tys):
+                return SimpleRes(
+                    TypedValue.from_local(
+                        value=self._random_struct_or_tuple_value(mut=local.mut, tys=tys),
+                        local=local,
+                    ),
+                )
+            case ArrayT(element_type=elem_ty, length=length):
+                value, metadata_size = self._random_array_value(mut=local.mut, elem_ty=elem_ty, length=length)
+                return ArrayRes(
+                    value=TypedValue.from_local(
+                        value=value,
+                        local=local,
+                    ),
+                    metadata_size=metadata_size,
+                )
+            case PtrT() | RefT():
+                return SimpleRes(
+                    value=TypedValue.from_local(
+                        value=self._random_ptr_value(mut=local.mut, type_info=type_info),
+                        local=local,
+                    ),
+                )
+            case _:
+                raise ValueError(f'Type unsupported for random value generator: {type_info}')
 
+    def _random_bool_value(self) -> BoolValue:
+        return BoolValue(bool(self._random.getrandbits(1)))
 
-def _random_bool_value(random: Random) -> BoolValue:
-    return BoolValue(bool(random.getrandbits(1)))
+    def _random_int_value(self, type_info: IntT | UintT) -> IntValue:
+        return IntValue(
+            value=self._random.randint(type_info.min, type_info.max),
+            nbits=type_info.nbits,
+            signed=isinstance(type_info, IntT),
+        )
 
+    def _random_enum_value(
+        self,
+        *,
+        mut: bool,
+        discriminants: list[int],
+        fields: list[list[Ty]],
+    ) -> AggregateValue:
+        variant_idx = self._random.randrange(len(discriminants))
+        values = self._random_fields(tys=fields[variant_idx], mut=mut)
+        return AggregateValue(variant_idx, values)
+
+    def _random_struct_or_tuple_value(self, *, mut: bool, tys: list[Ty]) -> AggregateValue:
+        return AggregateValue(0, fields=self._random_fields(tys=tys, mut=mut))
+
+    def _random_fields(self, *, tys: list[Ty], mut: bool) -> tuple[Value, ...]:
+        return tuple(self._random_value(local=_Local(ty=ty, mut=mut)).value.value for ty in tys)
+
+    def _random_array_value(self, *, mut: bool, elem_ty: Ty, length: int | None) -> tuple[RangeValue, MetadataSize]:
+        metadata_size: MetadataSize
+        if length is None:
+            length = self._random.randint(0, RANDOM_MAX_ARRAY_LEN)
+            metadata_size = DynamicSize(length)
+        else:
+            metadata_size = StaticSize(length)
+
+        elems = tuple(self._random_value(local=_Local(ty=elem_ty, mut=mut)).value.value for _ in range(length))
+        value = RangeValue(elems)
+        return value, metadata_size
+
+    def _random_ptr_value(self, mut: bool, type_info: PtrT | RefT) -> PtrLocalValue | RefValue:
+        pointee_local = _Local(ty=type_info.pointee_type, mut=mut)
+        pointee_res = self._random_value(pointee_local)
+        self._pointees.append(pointee_res.value)
+
+        metadata_size: MetadataSize
+        match pointee_res:
+            case ArrayRes(metadata_size=metadata_size):
+                pass
+            case _:
+                metadata_size = NO_SIZE
 
-def _random_int_value(random: Random, type_info: IntT | UintT) -> IntValue:
-    return IntValue(
-        value=random.randint(type_info.min, type_info.max),
-        nbits=type_info.nbits,
-        signed=isinstance(type_info, IntT),
-    )
+        metadata = Metadata(size=metadata_size, pointer_offset=0, origin_size=metadata_size)
+
+        ref = next(self._ref)
+
+        match type_info:
+            case PtrT():
+                return PtrLocalValue(
+                    stack_depth=0,
+                    place=Place(local=Local(ref)),
+                    mut=mut,
+                    metadata=metadata,
+                )
+            case RefT():
+                return RefValue(
+                    stack_depth=0,
+                    place=Place(local=Local(ref)),
+                    mut=mut,
+                    metadata=metadata,
+                )
+            case _:
+                raise AssertionError()