Initialise a call config in python (with symbolic arguments)

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.163"
+version = "0.3.164"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.163'
+VERSION: Final = '0.3.164'

kmir/src/kmir/__main__.py

@@ -69,7 +69,11 @@ def _kmir_gen_spec(opts: GenSpecOpts) -> None:
 
     kmir_kast, _ = parse_result
     apr_proof = kmir.apr_proof_from_kast(
-        str(opts.input_file.stem.replace('_', '-')), kmir_kast, start_symbol=opts.start_symbol, sort='KmirCell'
+        str(opts.input_file.stem.replace('_', '-')),
+        kmir_kast,
+        SMIRInfo.from_file(opts.input_file),
+        start_symbol=opts.start_symbol,
+        sort='KmirCell',
     )
     claim = apr_proof.as_claim()
 
@@ -110,7 +114,7 @@ def _kmir_view(opts: ViewOpts) -> None:
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
     smir_info = None
     if opts.smir_info is not None:
-        smir_info = SMIRInfo(opts.smir_info)
+        smir_info = SMIRInfo.from_file(opts.smir_info)
     node_printer = KMIRAPRNodePrinter(kmir, proof, smir_info=smir_info, full_printer=False)
     viewer = APRProofViewer(proof, kmir, node_printer=node_printer)
     viewer.run()
@@ -121,7 +125,7 @@ def _kmir_show(opts: ShowOpts) -> None:
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
     smir_info = None
     if opts.smir_info is not None:
-        smir_info = SMIRInfo(opts.smir_info)
+        smir_info = SMIRInfo.from_file(opts.smir_info)
     node_printer = KMIRAPRNodePrinter(kmir, proof, smir_info=smir_info, full_printer=opts.full_printer)
     shower = APRProofShow(kmir, node_printer=node_printer)
     lines = shower.show(proof)

kmir/src/kmir/kast.py

@@ -0,0 +1,215 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+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.ml import mlEqualsTrue
+from pyk.kast.prelude.utils import token
+
+from .smir import ArrayT, Bool, EnumT, Int, RefT, StructT, TupleT, Uint, UnionT
+
+if TYPE_CHECKING:
+    from collections.abc import Iterable
+
+    from pyk.kast.inner import KInner
+
+    from .smir import SMIRInfo
+
+
+def int_var(var: KVariable, num_bytes: int, signed: bool) -> tuple[KInner, Iterable[KInner]]:
+    bit_width = num_bytes * 8
+    var_max = ((1 << (bit_width - 1)) if signed else (1 << bit_width)) - 1
+    var_min = -(1 << (bit_width - 1)) if signed else 0
+    constraints = (mlEqualsTrue(leInt(var, token(var_max))), mlEqualsTrue(leInt(token(var_min), var)))
+    term = KApply('Value::Integer', (var, token(bit_width), token(signed)))
+    return term, constraints
+
+
+def bool_var(var: KVariable) -> tuple[KInner, Iterable[KInner]]:
+    term = KApply('Value::BoolVal', (var,))
+    return term, ()
+
+
+def mk_call_terminator(target: int, arg_count: int) -> KInner:
+    operands = [
+        KApply(
+            'Operand::Copy',
+            (KApply('place', (KApply('local', (token(i + 1),)), KApply('ProjectionElems::empty', ()))),),
+        )
+        for i in range(arg_count)
+    ]
+
+    args = build_cons(KApply('Operands::empty', ()), 'Operands::append', operands)
+
+    return KApply(
+        '#execTerminator(_)_KMIR-CONTROL-FLOW_KItem_Terminator',
+        (
+            KApply(
+                'terminator(_,_)_BODY_Terminator_TerminatorKind_Span',
+                (
+                    KApply(
+                        'TerminatorKind::Call',
+                        (
+                            KApply(
+                                'Operand::Constant',
+                                (
+                                    KApply(
+                                        'constOperand(_,_,_)_BODY_ConstOperand_Span_MaybeUserTypeAnnotationIndex_MirConst',
+                                        (
+                                            KApply('span', token(0)),
+                                            KApply('noUserTypeAnnotationIndex_BODY_MaybeUserTypeAnnotationIndex', ()),
+                                            KApply(
+                                                'mirConst(_,_,_)_TYPES_MirConst_ConstantKind_Ty_MirConstId',
+                                                (
+                                                    KApply('ConstantKind::ZeroSized', ()),
+                                                    KApply('ty', (token(target),)),
+                                                    KApply('mirConstId(_)_TYPES_MirConstId_Int', (token(0),)),
+                                                ),
+                                            ),
+                                        ),
+                                    ),
+                                ),
+                            ),
+                            args,
+                            KApply(
+                                'place',
+                                (
+                                    KApply('local', (token(0),)),
+                                    KApply('ProjectionElems::empty', ()),
+                                ),
+                            ),
+                            KApply('noBasicBlockIdx_BODY_MaybeBasicBlockIdx', ()),
+                            KApply('UnwindAction::Continue', ()),
+                        ),
+                    ),
+                    KApply('span', token(0)),
+                ),
+            ),
+        ),
+    )
+
+
+def symbolic_locals(smir_info: SMIRInfo, local_types: list[dict]) -> tuple[list[KInner], list[KInner]]:
+    locals, constraints = ArgGenerator(smir_info).run(local_types)
+    local0 = KApply('newLocal', (KApply('ty', (token(0),)), KApply('Mutability::Not', ())))
+    return ([local0] + locals, constraints)
+
+
+def _typed_value(value: KInner, ty: int, mutable: bool) -> KInner:
+    return KApply(
+        'typedValue',
+        (value, KApply('ty', (token(ty),)), KApply('Mutability::Mut' if mutable else 'Mutability::Not', ())),
+    )
+
+
+class ArgGenerator:
+    smir_info: SMIRInfo
+    locals: list[KInner]
+    pointees: list[KInner]
+    constraints: list[KInner]
+    counter: int
+    ref_offset: int
+
+    if TYPE_CHECKING:
+        from .smir import Ty
+
+    def __init__(self, smir_info: SMIRInfo) -> None:
+        self.smir_info = smir_info
+        self.locals = []
+        self.pointees = []
+        self.constraints = []
+        self.counter = 1
+        self.ref_offset = 0
+
+    def run(self, local_types: list[dict]) -> tuple[list[KInner], list[KInner]]:
+        self.ref_offset = len(local_types) + 1
+        for ty, mut in [(t['ty'], t['mutability']) for t in local_types]:
+            self._add_local(ty, mut == 'Mut')
+        return (self.locals + self.pointees, self.constraints)
+
+    def _add_local(self, ty: Ty, mutable: bool) -> None:
+        value, constraints = self._symbolic_value(ty, mutable)
+
+        self.locals.append(_typed_value(value, ty, mutable))
+        self.constraints += constraints
+
+    def _fresh_var(self, prefix: str) -> KVariable:
+        name = prefix + str(self.counter)
+        self.counter += 1
+        return KVariable(name)
+
+    def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInner]]:
+        match self.smir_info.types.get(ty):
+            case Int(info):
+                return int_var(self._fresh_var('ARG_INT'), info.value, True)
+
+            case Uint(info):
+                return int_var(self._fresh_var('ARG_UINT'), info.value, False)
+
+            case Bool():
+                return bool_var(self._fresh_var('ARG_BOOL'))
+
+            case EnumT(_, _, discriminants):
+                variantVar = self._fresh_var('ARG_VARIDX')
+                # constraints for variant index being in range
+                max_variant = max(discriminants.keys())
+                idx_range = [
+                    mlEqualsTrue(leInt(token(0), variantVar)),
+                    mlEqualsTrue(leInt(variantVar, token(max_variant))),
+                ]
+                args = self._fresh_var('ENUM_ARGS')
+                return KApply('Value::Aggregate', (KApply('variantIdx', (variantVar,)), args)), idx_range
+
+            case StructT():
+                args = self._fresh_var('STRUCT_ARGS')
+                return KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), args)), []
+
+            case UnionT():
+                args = self._fresh_var('ARG_UNION')
+                return KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), args)), []
+
+            case ArrayT(_, None):
+                elems = self._fresh_var('ARG_ARRAY')
+                return KApply('Value::Range', (elems,)), []
+
+            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)
+                    elem_vars.append(_typed_value(new_var, element_type, mutable))
+                    elem_constraints += new_constraints
+                return KApply('Value::Range', (list_of(elem_vars),)), elem_constraints
+
+            case TupleT(components):
+                elem_vars = []
+                elem_constraints = []
+                for _ty in components:
+                    new_var, new_constraints = self._symbolic_value(_ty, mutable)
+                    elem_vars.append(_typed_value(new_var, _ty, mutable))
+                    elem_constraints += new_constraints
+                return (
+                    KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), list_of(elem_vars))),
+                    elem_constraints,
+                )
+
+            case RefT(pointee_ty):
+                pointee_var, pointee_constraints = self._symbolic_value(pointee_ty, mutable)
+                ref = self.ref_offset
+                self.ref_offset += 1
+                self.pointees.append(_typed_value(pointee_var, pointee_ty, mutable))
+                return (
+                    KApply(
+                        'Value::Reference',
+                        (
+                            token(0),
+                            KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))),
+                            KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()),
+                        ),
+                    ),
+                    pointee_constraints,
+                )
+            case _:
+                return self._fresh_var('ARG'), []

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

@@ -46,9 +46,9 @@ syntax MaybeOperand ::= someOperand(Operand) [group(mir-option)]
 
 syntax Operands ::= List {Operand, ""} [group(mir-list), symbol(Operands::append), terminator-symbol(Operands::empty)]
 
-syntax Local ::= local(Int)            [group(mir-int)]
-syntax MaybeLocal ::= someLocal(Local) [group(mir-option)]
-                    | "noLocal"        [group(mir-option)]
+syntax Local ::= local(Int)            [group(mir-int)   , symbol(local)]
+syntax MaybeLocal ::= someLocal(Local) [group(mir-option), symbol(someLocal)]
+                    | "noLocal"        [group(mir-option), symbol(noLocal)]
 
 syntax ProjectionElem ::=  "projectionElemDeref"                                                            [group(mir-enum),                                symbol(ProjectionElem::Deref)]
                         |  projectionElemField(FieldIdx, Ty)                                                [group(mir-enum),                                symbol(ProjectionElem::Field)]
@@ -60,9 +60,9 @@ syntax ProjectionElem ::=  "projectionElemDeref"
                         |  projectionElemSubtype(Ty)                                                        [group(mir-enum),                                symbol(ProjectionElem::Subtype)]
 
 syntax ProjectionElems ::= List {ProjectionElem, ""} [group(mir-list), symbol(ProjectionElems::append), terminator-symbol(ProjectionElems::empty)]
-syntax Place ::= place(local: Local, projection: ProjectionElems) [group(mir---local--projection)]
-syntax MaybePlace ::= somePlace(Place)                            [group(mir-option)]
-                    | "noPlace"                                   [group(mir-option)]
+syntax Place ::= place(local: Local, projection: ProjectionElems) [group(mir---local--projection), symbol(place)]
+syntax MaybePlace ::= somePlace(Place)                            [group(mir-option), symbol(somePlace)]
+                    | "noPlace"                                   [group(mir-option), symbol(noPlace)]
 
 syntax Branch ::= branch(MIRInt, BasicBlockIdx) [group(mir)]
 syntax Branches ::= List {Branch, ""} [group(mir-list), symbol(Branches::append), terminator-symbol(Branches::empty)]

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

@@ -59,7 +59,7 @@ The `Map` of types is static information used for decoding constants and allocat
 It maps `Ty` IDs to `TypeInfo` that can be supplied to decoding and casting functions as well as operations involving `Aggregate` values (related to `struct`s and `enum`s).
 
 ```k
-  syntax Map ::= #mkTypeMap ( Map, TypeMappings ) [function, total]
+  syntax Map ::= #mkTypeMap ( Map, TypeMappings ) [function, total, symbol("mkTypeMap")]
 
   rule #mkTypeMap(ACC, .TypeMappings) => ACC
 
@@ -80,7 +80,7 @@ It maps `Ty` IDs to `TypeInfo` that can be supplied to decoding and casting func
 Another type-related `Map` is required to associate an `AdtDef` ID with its corresponding `Ty` ID for `struct`s and `enum`s when creating or using `Aggregate` values.
 
 ```k
-  syntax Map ::= #mkAdtMap ( Map , TypeMappings ) [function, total]
+  syntax Map ::= #mkAdtMap ( Map , TypeMappings ) [function, total, symbol("mkAdtMap")]
   // --------------------------------------------------------------
   rule #mkAdtMap(ACC, .TypeMappings) => ACC
 
@@ -108,7 +108,7 @@ they are callee in a `Call` terminator within an `Item`).
 The function _names_ and _ids_ are not relevant for calls and therefore dropped.
 
 ```k
-  syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total ]
+  syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total, symbol("mkFunctionMap") ]
                | #accumFunctions ( Map, Map, FunctionNames ) [ function, total ]
                | #accumItems ( Map, MonoItems )              [ function, total ]
 

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

@@ -22,17 +22,17 @@ High-level values can be
 - arrays and slices (with homogenous element types)
 
 ```k
-  syntax Value ::= Integer( Int, Int, Bool )
+  syntax Value ::= Integer( Int, Int, Bool )              [symbol(Value::Integer)]
                    // value, bit-width, signedness   for un/signed int
-                 | BoolVal( Bool )
+                 | BoolVal( Bool )                        [symbol(Value::BoolVal)]
                    // boolean
-                 | Aggregate( VariantIdx , List )
+                 | Aggregate( VariantIdx , List )         [symbol(Value::Aggregate)]
                    // heterogenous value list        for tuples and structs (standard, tuple, or anonymous)
-                 | Float( Float, Int )
+                 | Float( Float, Int )                    [symbol(Value::Float)]
                    // value, bit-width               for f16-f128
-                 | Reference( Int , Place , Mutability )
+                 | Reference( Int , Place , Mutability )  [symbol(Value::Reference)]
                    // stack depth (initially 0), place, borrow kind
-                 | Range( List )
+                 | Range( List )                          [symbol(Value::Range)]
                    // homogenous values              for array/slice
                 //  | Ptr( Address, MaybeValue )
                    // address, metadata              for ref/ptr
@@ -52,11 +52,11 @@ The local variables may be actual values (`typedValue`), uninitialised (`NewLoca
   // local storage of the stack frame
   syntax TypedLocal ::= TypedValue | MovedLocal | NewLocal
 
-  syntax TypedValue ::= typedValue ( Value , MaybeTy , Mutability )
+  syntax TypedValue ::= typedValue ( Value , MaybeTy , Mutability ) [symbol(typedValue)]
 
   syntax MovedLocal ::= "Moved"
 
-  syntax NewLocal ::= newLocal ( Ty , Mutability )
+  syntax NewLocal ::= newLocal ( Ty , Mutability )                  [symbol(newLocal)]
 
   // the type of aggregates cannot be determined from the data provided when they
   // occur as `RValue`, therefore we have to make the `Ty` field optional here.

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

@@ -71,7 +71,7 @@ syntax ParamDef ::= paramDef(Int)                       [group(mir-int)] // impo
 syntax RegionDef ::= regionDef(Int)                     [group(mir-int)] // imported from crate
 syntax TraitDef ::= traitDef(Int)                       [group(mir-int)] // imported from crate
 
-syntax VariantIdx ::= variantIdx(Int) [group(mir-int)]
+syntax VariantIdx ::= variantIdx(Int) [group(mir-int), symbol(variantIdx)]
 
 syntax DynKind ::= "dynKindDyn"      [group(mir-enum), symbol(DynKind::Dyn)]
                  | "dynKindDynStar"  [group(mir-enum), symbol(DynKind::DynStar)]