Remove unused code (#752)

Fixes #748

Author: tothtamas28

kmir/src/kmir/__main__.py

@@ -9,9 +9,8 @@
 
 from pyk.cli.args import KCLIArgs
 from pyk.cterm.show import CTermShow
-from pyk.kast.outer import KFlatModule, KImport
 from pyk.kast.pretty import PrettyPrinter
-from pyk.proof.reachability import APRProof, APRProver
+from pyk.proof.reachability import APRProof
 from pyk.proof.show import APRProofShow
 from pyk.proof.tui import APRProofViewer
 
@@ -20,17 +19,14 @@
 from .kmir import KMIR, KMIRAPRNodePrinter
 from .linker import link
 from .options import (
-    GenSpecOpts,
     InfoOpts,
     LinkOpts,
-    ProveRawOpts,
     ProveRSOpts,
     PruneOpts,
     RunOpts,
     ShowOpts,
     ViewOpts,
 )
-from .parse.parser import parse_json
 from .smir import SMIRInfo, Ty
 from .utils import render_leaf_k_cells, render_rules, render_statistics
 
@@ -71,55 +67,6 @@ def _kmir_prove_rs(opts: ProveRSOpts) -> None:
         sys.exit(1)
 
 
-def _kmir_gen_spec(opts: GenSpecOpts) -> None:
-    kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR)
-
-    parse_result = parse_json(kmir.definition, opts.input_file, 'Pgm')
-    if parse_result is None:
-        print('Parse error!', file=sys.stderr)
-        sys.exit(1)
-
-    smir_info = SMIRInfo.from_file(opts.input_file).reduce_to(opts.start_symbol)
-    apr_proof = kmir.apr_proof_from_smir(
-        str(opts.input_file.stem.replace('_', '-')),
-        smir_info,
-        start_symbol=opts.start_symbol,
-        sort='KmirCell',
-    )
-    claim = apr_proof.as_claim()
-
-    output_file = opts.output_file
-    if output_file is None:
-        suffixes = ''.join(opts.input_file.suffixes)
-        base = opts.input_file.name.removesuffix(suffixes).replace('_', '-')
-        output_file = Path(f'{base}-spec.k')
-
-    module_name = output_file.stem.upper().replace('_', '-')
-    spec_module = KFlatModule(module_name, (claim,), (KImport('KMIR'),))
-
-    output_file.write_text(kmir.pretty_print(spec_module))
-
-
-def _kmir_prove_raw(opts: ProveRawOpts) -> None:
-    kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report)
-    claim_index = kmir.get_claim_index(opts.spec_file)
-    labels = claim_index.labels(include=opts.include_labels, exclude=opts.exclude_labels)
-    for label in labels:
-        print(f'Proving {label}')
-        claim = claim_index[label]
-        if not opts.reload and opts.proof_dir is not None and APRProof.proof_data_exists(label, opts.proof_dir):
-            _LOGGER.info(f'Reading proof from disc: {opts.proof_dir}, {label}')
-            proof = APRProof.read_proof_data(opts.proof_dir, label)
-        else:
-            _LOGGER.info(f'Constructing initial proof: {label}')
-            proof = APRProof.from_claim(kmir.definition, claim, {}, proof_dir=opts.proof_dir)
-        with kmir.kcfg_explore(label) as kcfg_explore:
-            prover = APRProver(kcfg_explore, execute_depth=opts.max_depth)
-            prover.advance_proof(proof, max_iterations=opts.max_iterations)
-        summary = proof.summary
-        print(f'{summary}')
-
-
 def _kmir_view(opts: ViewOpts) -> None:
     kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR)
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
@@ -212,12 +159,8 @@ def kmir(args: Sequence[str]) -> None:
     match opts:
         case RunOpts():
             _kmir_run(opts)
-        case GenSpecOpts():
-            _kmir_gen_spec(opts)
         case InfoOpts():
             _kmir_info(opts)
-        case ProveRawOpts():
-            _kmir_prove_raw(opts)
         case ViewOpts():
             _kmir_view(opts)
         case ShowOpts():
@@ -248,15 +191,6 @@ def _arg_parser() -> ArgumentParser:
     )
     run_parser.add_argument('--haskell-backend', action='store_true', help='Run with the haskell backend')
 
-    gen_spec_parser = command_parser.add_parser(
-        'gen-spec', help='Generate a k spec from a SMIR json', parents=[kcli_args.logging_args]
-    )
-    gen_spec_parser.add_argument('input_file', metavar='FILE', help='MIR program to generate a spec for')
-    gen_spec_parser.add_argument('--output-file', metavar='FILE', help='Output file')
-    gen_spec_parser.add_argument(
-        '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
-    )
-
     info_parser = command_parser.add_parser(
         'info', help='Show information about a SMIR JSON file', parents=[kcli_args.logging_args]
     )
@@ -276,17 +210,6 @@ def _arg_parser() -> ArgumentParser:
     proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view')
     proof_args.add_argument('--proof-dir', metavar='DIR', help='Proof directory')
 
-    prove_raw_parser = command_parser.add_parser(
-        'prove', help='Utilities for working with proofs over SMIR', parents=[kcli_args.logging_args, prove_args]
-    )
-    prove_raw_parser.add_argument('input_file', metavar='FILE', help='K File with the spec module')
-    prove_raw_parser.add_argument(
-        '--include-labels', metavar='LABELS', help='Comma separated list of claim labels to include'
-    )
-    prove_raw_parser.add_argument(
-        '--exclude-labels', metavar='LABELS', help='Comma separated list of claim labels to exclude'
-    )
-
     display_args = ArgumentParser(add_help=False)
     display_args.add_argument(
         '--full-printer',
@@ -394,22 +317,8 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 start_symbol=ns.start_symbol,
                 haskell_backend=ns.haskell_backend,
             )
-        case 'gen-spec':
-            return GenSpecOpts(input_file=Path(ns.input_file), output_file=ns.output_file, start_symbol=ns.start_symbol)
         case 'info':
             return InfoOpts(smir_file=Path(ns.smir_file), types=ns.types)
-        case 'prove':
-            proof_dir = Path(ns.proof_dir)
-            return ProveRawOpts(
-                spec_file=Path(ns.input_file),
-                proof_dir=ns.proof_dir,
-                include_labels=ns.include_labels,
-                exclude_labels=ns.exclude_labels,
-                bug_report=ns.bug_report,
-                max_depth=ns.max_depth,
-                reload=ns.reload,
-                max_iterations=ns.max_iterations,
-            )
         case 'show':
             return ShowOpts(
                 proof_dir=Path(ns.proof_dir),

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

@@ -33,7 +33,5 @@ module KMIR-AST
 
   syntax TypeMappings ::= List{TypeMapping, ""} [group(mir-list), symbol(TypeMappings::append), terminator-symbol(TypeMappings::empty)]
 
-  syntax KItem ::= #init( Pgm )
-
 endmodule
-```
+```

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

@@ -2,7 +2,6 @@
 
 ```k
 requires "kmir-ast.md"
-requires "symbolic/kmir-symbolic-locals.md"
 requires "rt/data.md"
 requires "rt/configuration.md"
 requires "lemmas/kmir-lemmas.md"
@@ -31,7 +30,6 @@ module KMIR-CONTROL-FLOW
   imports MAP
   imports K-EQUAL
 
-  imports KMIR-AST
   imports MONO
   imports TYPES
 
@@ -45,146 +43,7 @@ function map and the initial memory have to be set up.
 
 All of this is done in the client code so we omit the initialisation code which was historically placed here.
 
-```
-  // #init step, assuming a singleton in the K cell
-  rule <k> #init(_NAME:Symbol _ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames _ITEMS:MonoItems _TYPES:TypeMappings _MACHINE:MachineInfo)
-         =>
-           #execFunction(#findItem(ITEMS, FUNCNAME), FUNCTIONS)
-       </k>
-```
-
-The `Map` of types is static information used for decoding constants and allocated data into `Value`s.
-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).
-
-```
-  syntax Map ::= #mkTypeMap ( Map, TypeMappings ) [function, total, symbol("mkTypeMap")]
-
-  rule #mkTypeMap(ACC, .TypeMappings) => ACC
-
-  // build map of Ty -> RigidTy from suitable pairs
-  rule #mkTypeMap(ACC, TypeMapping(TY, TYPEINFO) MORE:TypeMappings)
-      =>
-       #mkTypeMap(ACC[TY <- TYPEINFO], MORE)
-    requires notBool TY in_keys(ACC)
-    [preserves-definedness] // key collision checked
-
-  // skip anything that causes a key collision
-  rule #mkTypeMap(ACC, _OTHERTYKIND:TypeMapping MORE:TypeMappings)
-      =>
-       #mkTypeMap(ACC, MORE)
-    [owise]
-```
-
-The `Map` of `functions` is constructed from the lookup table of `FunctionNames`,
-composed with a secondary lookup of `Item`s via `symbolName`. This composed map will
-only be populated for `MonoItemFn` items that are indeed _called_ in the code (i.e.,
-they are callee in a `Call` terminator within an `Item`).
-
-The function _names_ and _ids_ are not relevant for calls and therefore dropped.
-
-```
-  syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total, symbol("mkFunctionMap") ]
-               | #accumFunctions ( Map, Map, FunctionNames ) [ function, total ]
-               | #accumItems ( Map, MonoItems )              [ function, total ]
-
-  rule #mkFunctionMap(Functions, Items)
-    =>
-       #accumFunctions(#mainIsMinusOne(Items), #accumItems(.Map, Items), Functions)
-  //////////////////// ^^^^^^^^^^^^^^^^^^^^^^ HACK Adds "main" as function with ty(-1)
-  syntax Map ::= #mainIsMinusOne(MonoItems) [function]
-  rule #mainIsMinusOne(ITEMS) => ty(-1) |-> monoItemKind(#findItem(ITEMS, symbol("main")))
-  ////////////////////////////////////////////////////////////////
-
-  // accumulate map of symbol_name -> function (MonoItemFn), discarding duplicate IDs
-  rule #accumItems(Acc, .MonoItems) => Acc
-
-  rule #accumItems(Acc, monoItem(SymName, monoItemFn(_, _, _) #as Function) Rest:MonoItems)
-     =>
-       #accumItems(Acc (SymName |-> Function), Rest)
-    requires notBool (SymName in_keys(Acc))
-    [ preserves-definedness ] // key collisions checked
-
-  // discard other items and duplicate symbolNames
-  rule #accumItems(Acc, _:MonoItem Rest:MonoItems)
-     =>
-       #accumItems(Acc, Rest)
-    [ owise ]
-
-  // accumulate composed map of Ty -> MonoItemFn, using item map from before and function names
-  rule #accumFunctions(Acc, _, .List) => Acc
-
-  rule #accumFunctions(Acc, ItemMap, ListItem(functionName(TyIdx, functionNormalSym(SymName))) Rest )
-    =>
-      #accumFunctions(Acc (TyIdx |-> ItemMap[SymName]), ItemMap, Rest)
-    requires SymName in_keys(ItemMap)
-     andBool notBool (TyIdx in_keys(Acc))
-    [preserves-definedness]
 
-  // TODO handle NoOpSym and IntrinsicSym cases here
-
-  // discard anything else:
-  // - duplicate Ty mappings (impossible by construction in stable-mir-json)
-  // - unknown symbol_name (impossible by construction in stable-mir-json)
-  rule #accumFunctions(Acc, ItemMap, ListItem(_) Rest)
-    =>
-       #accumFunctions(Acc, ItemMap, Rest)
-    [ owise ]
-
-```
-
-Executing a given named function means to create the `currentFrame` data
-structure from its function body and then execute the first basic
-block of the body. The function's `Ty` index in the `functions` map must
-be known to populate the `currentFunc` field.
-
-```
-  // find function through its MonoItemFn.name
-  syntax MonoItem ::= #findItem ( MonoItems, Symbol ) [ function ]
-
-  rule #findItem( (monoItem(_, monoItemFn(N, _, _)) #as ITEM) _REST, NAME )
-     =>
-       ITEM
-    requires N ==K NAME
-  rule #findItem( _:MonoItem REST:MonoItems, NAME )
-     =>
-       #findItem(REST, NAME)
-    [owise]
-  // rule #findItem( .MonoItems, _NAME) => error!
-
-  syntax KItem ::= #execFunction ( MonoItem, FunctionNames )
-
-  rule <k> #execFunction(
-              monoItem(
-                SYMNAME,
-                monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS,LOCALS, _, _, _, _)))
-              ),
-              FUNCTIONNAMES
-            )
-         =>
-           #execBlock(FIRST)
-         ...
-       </k>
-       <currentFunc> _ => #tyFromName(SYMNAME, FUNCTIONNAMES) </currentFunc>
-       <currentFrame>
-         <currentBody> _ => toKList(BLOCKS) </currentBody>
-         <caller> _ => ty(-1) </caller> // no caller
-         <dest> _ => place(local(-1), .ProjectionElems)</dest>
-         <target> _ => noBasicBlockIdx </target>
-         <unwind> _ => unwindActionUnreachable </unwind>
-         <locals> _ => #reserveFor(LOCALS)  </locals>
-       </currentFrame>
-
-  // This function performs a reverse lookup in the functions table (looks up a `Ty` by name)
-  // It defaults to `Ty(-1)` which is currently what `main` gets (`main` is not in the functions table)
-  syntax Ty ::= #tyFromName( Symbol, FunctionNames ) [function, total]
-
-  rule #tyFromName(NAME, ListItem(functionName(TY, functionNormalSym(FNAME))) _) => TY
-    requires NAME ==K FNAME
-  rule #tyFromName(NAME, ListItem(_) REST:List) => #tyFromName(NAME, REST)
-    [owise]
-
-  rule #tyFromName(_, .List) => ty(-1) // HACK see #mainIsMinusOne above
-```
 #### Function Execution
 
 
@@ -677,8 +536,7 @@ The top-level module `KMIR` includes both the control flow constructs (and trans
 
 ```k
 module KMIR
+  imports KMIR-AST // Necessary for the external Python parser
   imports KMIR-CONTROL-FLOW
   imports KMIR-LEMMAS
-//  imports KMIR-SYMBOLIC-LOCALS
-
 endmodule

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

@@ -17,7 +17,6 @@ Besides the `caller` (to return to) and `dest` and `target` to specify where the
 requires "./value.md"
 
 module KMIR-CONFIGURATION
-  imports KMIR-AST
   imports INT-SYNTAX
   imports BOOL-SYNTAX
   imports RT-VALUE-SYNTAX
@@ -32,7 +31,7 @@ module KMIR-CONFIGURATION
                                    locals:List)               // return val, args, local variables
 
   configuration <kmir>
-                  <k> #init($PGM:Pgm) </k>
+                  <k> $PGM:KItem </k>
                   <retVal> noReturn </retVal>
                   <currentFunc> ty(-1) </currentFunc> // to retrieve caller
                   // unpacking the top frame to avoid frequent stack read/write operations