Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

kmir/src/kmir/kmir.py

@@ -87,45 +87,61 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:
         ) as cts:
             yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
 
-    def make_call_config(
+    def _make_concrete_call_config(self, smir_info: SMIRInfo, *, start_symbol: str = 'main') -> KInner:
+        def init_subst() -> dict[str, KInner]:
+            init_config = self.definition.init_config(KSort('GeneratedTopCell'))
+            _, res = split_config_from(init_config)
+            return res
+
+        if not start_symbol in smir_info.function_tys:
+            raise KeyError(f'{start_symbol} not found in program')
+
+        args_info = smir_info.function_arguments[start_symbol]
+        if args_info:
+            raise ValueError(
+                f'Cannot create concrete call configuration for {start_symbol}: function has parameters: {args_info}'
+            )
+
+        # The configuration is the default initial configuration, with the K cell updated with the call terminator
+        # TODO: see if this can be expressed in more simple terms
+        subst = Subst(
+            {
+                **init_subst(),
+                **{
+                    'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
+                },
+            }
+        )
+        empty_config = self.definition.empty_config(KSort('GeneratedTopCell'))
+        config = subst(empty_config)
+        assert not free_vars(config), f'Config by construction should not have any free variables: {config}'
+        return config
+
+    def _make_symbolic_call_config(
         self,
         smir_info: SMIRInfo,
         *,
         start_symbol: str = 'main',
-        sort: str = 'GeneratedTopCell',
-        init: bool = False,
     ) -> tuple[KInner, list[KInner]]:
         if not start_symbol in smir_info.function_tys:
             raise KeyError(f'{start_symbol} not found in program')
 
         args_info = smir_info.function_arguments[start_symbol]
         locals, constraints = symbolic_locals(smir_info, args_info)
-
-        _subst = {
-            'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
-            'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
-            'LOCALS_CELL': list_of(locals),
-        }
-
-        _init_subst: dict[str, KInner] = {}
-        if init:
-            _subst['LOCALS_CELL'] = list_empty()
-            init_config = self.definition.init_config(KSort(sort))
-            _, _init_subst = split_config_from(init_config)
-
-        for key in _init_subst:
-            if key not in _subst:
-                _subst[key] = _init_subst[key]
-
-        subst = Subst(_subst)
-        config = self.definition.empty_config(KSort(sort))
-        return (subst.apply(config), constraints)
+        subst = Subst(
+            {
+                'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
+                'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
+                'LOCALS_CELL': list_of(locals),
+            },
+        )
+        empty_config = self.definition.empty_config(KSort('GeneratedTopCell'))
+        config = subst(empty_config)
+        return config, constraints
 
     def run_smir(self, smir_info: SMIRInfo, start_symbol: str = 'main', depth: int | None = None) -> Pattern:
         smir_info = smir_info.reduce_to(start_symbol)
-        init_config, init_constraints = self.make_call_config(smir_info, start_symbol=start_symbol, init=True)
-        if len(free_vars(init_config)) > 0 or len(init_constraints) > 0:
-            raise ValueError(f'Cannot run function with variables: {start_symbol} - {free_vars(init_config)}')
+        init_config = self._make_concrete_call_config(smir_info, start_symbol=start_symbol)
         init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell'))
         result = self.run_pattern(init_kore, depth=depth)
         return result
@@ -135,10 +151,9 @@ def apr_proof_from_smir(
         id: str,
         smir_info: SMIRInfo,
         start_symbol: str = 'main',
-        sort: str = 'GeneratedTopCell',
         proof_dir: Path | None = None,
     ) -> APRProof:
-        lhs_config, constraints = self.make_call_config(smir_info, start_symbol=start_symbol, sort=sort)
+        lhs_config, constraints = self._make_symbolic_call_config(smir_info, start_symbol=start_symbol)
         lhs = CTerm(lhs_config, constraints)
 
         var_config, var_subst = split_config_from(lhs_config)