Merge remote-tracking branch 'upstream/master' into foundry-fixes

ehildenb · ehildenb · commit f81aca1e74b5 · 2022-12-14T05:21:05.000Z
diff --git a/include/kframework/abi.md b/include/kframework/abi.md
@@ -325,7 +325,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
     rule #enc( #int256( DATA )) => #bufStrict(32, #getValue( #int256( DATA )))
     rule #enc( #int128( DATA )) => #bufStrict(32, #getValue( #int128( DATA )))
 
-    rule #enc( #bytes4( DATA )) => #bufStrict(32, #getValue( #bytes4( DATA )))
+    rule #enc( #bytes4( DATA )) => #padRightToWidth(32, #bufStrict(4, #getValue(#bytes4( DATA ))))
     rule #enc(#bytes32( DATA )) => #bufStrict(32, #getValue(#bytes32( DATA )))
 
     rule #enc(   #bool( DATA )) => #bufStrict(32, #getValue(   #bool( DATA )))
diff --git a/include/kframework/evm-types.md b/include/kframework/evm-types.md
@@ -435,10 +435,10 @@ The local memory of execution is a byte-array (instead of a word-array).
     syntax ByteArray ::= #padToWidth      ( Int , ByteArray ) [function, total]
                        | #padRightToWidth ( Int , ByteArray ) [function, total]
  // ---------------------------------------------------------------------------
-    rule                        #padToWidth(N, BS)      =>               BS        requires notBool (N >=Int 0)
-    rule [padToWidthNonEmpty] : #padToWidth(N, BS)      =>  padLeftBytes(BS, N, 0) requires          N >=Int 0
-    rule                        #padRightToWidth(N, BS) =>               BS        requires notBool (N >=Int 0)
-    rule                        #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires          N >=Int 0
+    rule                            #padToWidth(N, BS)      =>               BS        requires notBool (N >=Int 0)
+    rule [padToWidthNonEmpty]:      #padToWidth(N, BS)      =>  padLeftBytes(BS, N, 0) requires          N >=Int 0
+    rule                            #padRightToWidth(N, BS) =>               BS        requires notBool (N >=Int 0)
+    rule [padRightToWidthNonEmpty]: #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires          N >=Int 0
 ```
 
 ```{.k .nobytes}
diff --git a/include/kframework/lemmas/lemmas.k b/include/kframework/lemmas/lemmas.k
@@ -136,10 +136,11 @@ module LEMMAS [symbolic]
 
     // sizeByteArray
 
-    rule #sizeByteArray(BUF1 ++ BUF2)            => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2)      [simplification]
-    rule #sizeByteArray(#buf(SIZE, _))           => SIZE                                                [simplification]
-    rule #sizeByteArray(_MEM [ START .. WIDTH ]) => WIDTH  requires 0 <=Int START andBool 0 <=Int WIDTH [simplification]
-    rule #sizeByteArray(#range(_, START, WIDTH)) => WIDTH  requires 0 <=Int START andBool 0 <=Int WIDTH [simplification]
+    rule #sizeByteArray(BUF1 ++ BUF2)                 => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2)      [simplification]
+    rule #sizeByteArray(#buf(SIZE, _))                => SIZE                                                [simplification]
+    rule #sizeByteArray(_MEM [ START .. WIDTH ])      => WIDTH  requires 0 <=Int START andBool 0 <=Int WIDTH [simplification]
+    rule #sizeByteArray(#range(_, START, WIDTH))      => WIDTH  requires 0 <=Int START andBool 0 <=Int WIDTH [simplification]
+    rule #sizeByteArray(#padRightToWidth(WIDTH, BUF)) => WIDTH  requires #sizeByteArray(BUF) <=Int WIDTH     [simplification]
 
     // TODO: custom ==K unification doesn't work in Haskell yet
     // ++ unification
@@ -149,6 +150,12 @@ module LEMMAS [symbolic]
 
     rule #asWord(WS) >>Int M => #asWord(WS [ 0 .. #sizeByteArray(WS) -Int (M /Int 8) ])  requires 0 <=Int M andBool M modInt 8 ==Int 0 [simplification]
 
+    rule #asWord(#padRightToWidth(32, BUF)) &Int notMaxUInt224 =>
+         #asWord(#padRightToWidth(32, BUF))
+      requires #sizeByteArray(BUF) <=Int 4 [simplification]
+
+    rule #padRightToWidth(_, BUF)[ 0 .. WIDTH ] => BUF requires #sizeByteArray(BUF) ==Int WIDTH [simplification]
+
 endmodule
 
 module LEMMAS-JAVA [symbolic, kast]
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -14,19 +14,32 @@
 from pyk.kcfg import KCFG
 from pyk.ktool.kit import KIT
 from pyk.ktool.krun import KRunOutput, _krun
+from pyk.prelude.k import GENERATED_TOP_CELL
 from pyk.prelude.ml import is_top, mlTop
 
 from .gst_to_kore import gst_to_kore
 from .kevm import KEVM, Foundry
 from .solc_to_k import Contract, contract_to_main_module, method_to_cfg, solc_compile
-from .utils import KCFG__replace_node, KPrint_make_unparsing, KProve_prove_claim, add_include_arg, sanitize_config
+from .utils import (
+    KCFG__replace_node,
+    KDefinition__expand_macros,
+    KPrint_make_unparsing,
+    KProve_prove_claim,
+    add_include_arg,
+    sanitize_config,
+)
 
 T = TypeVar('T')
 
 _LOGGER: Final = logging.getLogger(__name__)
 _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
 
 
+def write_cfg(_cfg: KCFG, _cfgpath: Path) -> None:
+    _cfgpath.write_text(_cfg.to_json())
+    _LOGGER.info(f'Updated CFG file: {_cfgpath}')
+
+
 def _ignore_arg(args: Dict[str, Any], arg: str, cli_option: str) -> None:
     if arg in args:
         if args[arg] is not None:
@@ -327,25 +340,21 @@ def exec_foundry_prove(
             contract_name, method_name = test.split('.')
             contract = [c for c in contracts if c.name == contract_name][0]
             method = [m for m in contract.methods if m.name == method_name][0]
-            empty_config = foundry.definition.empty_config(Foundry.Sorts.FOUNDRY_CELL)
+            empty_config = foundry.definition.empty_config(GENERATED_TOP_CELL)
             cfg = method_to_cfg(empty_config, contract, method)
+            init_term = cfg.get_unique_init().cterm.kast
+            target_term = cfg.get_unique_target().cterm.kast
+            _LOGGER.info(f'Expanding macros in initial state for test: {test}')
+            init_term = KDefinition__expand_macros(foundry.definition, init_term)
+            _LOGGER.info(f'Expanding macros in target state for test: {test}')
+            target_term = KDefinition__expand_macros(foundry.definition, target_term)
             if simplify_init:
                 _LOGGER.info(f'Simplifying initial state for test: {test}')
-                edge = KCFG.Edge(cfg.get_unique_init(), cfg.get_unique_target(), mlTop(), -1)
-                claim = edge.to_claim()
-                init_simplified = foundry.prove_claim(
-                    claim, f'simplify-init-{cfg.get_unique_init().id}', args=['--depth', '0']
-                )
-                init_simplified = sanitize_config(foundry.definition, init_simplified)
-                cfg = KCFG__replace_node(cfg, cfg.get_unique_init().id, CTerm(init_simplified))
+                init_term = foundry.simplify(CTerm(init_term))
                 _LOGGER.info(f'Simplifying target state for test: {test}')
-                edge = KCFG.Edge(cfg.get_unique_target(), cfg.get_unique_init(), mlTop(), -1)
-                claim = edge.to_claim()
-                target_simplified = foundry.prove_claim(
-                    claim, f'simplify-target-{cfg.get_unique_target().id}', args=['--depth', '0']
-                )
-                target_simplified = sanitize_config(foundry.definition, target_simplified)
-                cfg = KCFG__replace_node(cfg, cfg.get_unique_target().id, CTerm(target_simplified))
+                target_term = foundry.simplify(CTerm(target_term))
+            cfg = KCFG__replace_node(cfg, cfg.get_unique_init().id, CTerm(init_term))
+            cfg = KCFG__replace_node(cfg, cfg.get_unique_target().id, CTerm(target_term))
             kcfgs[test] = (cfg, kcfg_file)
             with open(kcfg_file, 'w') as kf:
                 kf.write(json.dumps(cfg.to_dict()))
@@ -357,11 +366,6 @@ def exec_foundry_prove(
 
     lemma_rules = [KRule(KToken(lr, 'K'), att=KAtt({'simplification': ''})) for lr in lemmas]
 
-    def _write_cfg(_cfg: KCFG, _cfgpath: Path) -> None:
-        with open(_cfgpath, 'w') as cfgfile:
-            cfgfile.write(json.dumps(_cfg.to_dict()))
-            _LOGGER.info(f'Updated CFG file: {_cfgpath}')
-
     def prove_it(_id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
         _cfg_id, (_cfg, _cfg_path) = _id_and_cfg
         if len(_cfg.frontier) == 0:
@@ -387,11 +391,12 @@ def prove_it(_id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
                 if minimize:
                     result_state = minimize_term(result_state)
                 _LOGGER.error(f'Proof failed: {_cfg_id}\n{foundry.pretty_print(result_state)}')
-        _write_cfg(_cfg, _cfg_path)
+        write_cfg(_cfg, _cfg_path)
         failure_nodes = _cfg.frontier + _cfg.stuck
         return len(failure_nodes) == 0
 
     with ProcessPool(ncpus=workers) as process_pool:
+        foundry.close_kore_rpc()
         results = process_pool.map(prove_it, kcfgs.items())
         process_pool.close()
 
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -161,6 +161,7 @@ def concrete_rules() -> List[str]:
             'EVM-TYPES.bytesRange',
             'EVM-TYPES.mapWriteBytes.recursive',
             'EVM-TYPES.#padRightToWidth',
+            'EVM-TYPES.padRightToWidthNonEmpty',
             'EVM-TYPES.#padToWidth',
             'EVM-TYPES.padToWidthNonEmpty',
             'EVM-TYPES.powmod.nonzero',
@@ -191,7 +192,7 @@ def add_invariant(cterm: CTerm) -> CTerm:
         constraints.append(mlEqualsTrue(KEVM.range_address(get_cell(config, 'ID_CELL'))))
         constraints.append(mlEqualsTrue(KEVM.range_address(get_cell(config, 'CALLER_CELL'))))
         constraints.append(mlEqualsTrue(KEVM.range_address(get_cell(config, 'ORIGIN_CELL'))))
-        constraints.append(mlEqualsTrue(ltInt(KEVM.size_bytearray(get_cell(config, 'CALLDATA_CELL')), KEVM.pow256())))
+        constraints.append(mlEqualsTrue(ltInt(KEVM.size_bytearray(get_cell(config, 'CALLDATA_CELL')), KEVM.pow128())))
 
         return CTerm(mlAnd([config] + list(unique(constraints))))
 
@@ -219,6 +220,10 @@ def jumpi_applied(pc: KInner, cond: KInner) -> KApply:
     def jump_applied(pc: KInner) -> KApply:
         return KApply('___EVM_InternalOp_UnStackOp_Int', [KEVM.jump(), pc])
 
+    @staticmethod
+    def pow128() -> KApply:
+        return KApply('pow128_WORD_Int', [])
+
     @staticmethod
     def pow256() -> KApply:
         return KApply('pow256_WORD_Int', [])
diff --git a/kevm-pyk/src/kevm_pyk/solc_to_k.py b/kevm-pyk/src/kevm_pyk/solc_to_k.py
@@ -545,7 +545,9 @@ def _range_predicate(term: KInner, type_label: str) -> Optional[KInner]:
         return KEVM.range_uint(256, term)
     if type_label == 'int256':
         return KEVM.range_sint(256, term)
-    if type_label in {'bytes', 'string'}:
+    if type_label == 'bytes':
+        return KEVM.range_uint(128, KEVM.size_bytearray(term))
+    if type_label == 'string':
         return TRUE
 
     _LOGGER.warning(f'Unknown range predicate for type: {type_label}')
diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -2,7 +2,7 @@
 from typing import Collection, Iterable, List, Optional, Tuple
 
 from pyk.cterm import CTerm
-from pyk.kast.inner import KApply, KInner, KVariable, Subst
+from pyk.kast.inner import KApply, KInner, KRewrite, KVariable, Subst
 from pyk.kast.manip import (
     abstract_term_safely,
     bool_to_ml_pred,
@@ -23,6 +23,27 @@
 from pyk.prelude.ml import mlAnd
 
 
+def KDefinition__expand_macros(defn: KDefinition, term: KInner) -> KInner:  # noqa: N802
+    def _expand_macros(_term: KInner) -> KInner:
+        if type(_term) is KApply:
+            prod = defn.production_for_klabel(_term.label)
+            if 'macro' in prod.att or 'alias' in prod.att or 'macro-rec' in prod.att or 'alias-rec' in prod.att:
+                for r in defn.macro_rules:
+                    assert type(r.body) is KRewrite
+                    _new_term = r.body.apply_top(_term)
+                    if _new_term != _term:
+                        _term = _new_term
+                        break
+        return _term
+
+    old_term = None
+    while term != old_term:
+        old_term = term
+        term = bottom_up(_expand_macros, term)
+
+    return term
+
+
 def KCFG__replace_node(cfg: KCFG, node_id: str, new_cterm: CTerm) -> KCFG:  # noqa: N802
 
     # Remove old node, record data
diff --git a/tests/foundry/exclude b/tests/foundry/exclude
@@ -14,6 +14,10 @@ AssumeTest.test_assume_false
 AssumeTest.testFail_assume_false
 AssumeTest.testFail_assume_true
 BroadcastTest.testDeploy
+BytesTypeTest.test_bytes32_fail
+BytesTypeTest.test_bytes4_fail
+BytesTypeTest.testFail_bytes32
+BytesTypeTest.testFail_bytes4
 ContractBTest.testCannotSubtract43
 ContractBTest.testFailSubtract43
 ContractBTest.testNumberIs42
diff --git a/tests/foundry/foundry.k.check.expected b/tests/foundry/foundry.k.check.expected
diff --git a/tests/foundry/test/DynamicTypes.t.sol b/tests/foundry/test/DynamicTypes.t.sol
diff --git a/tests/foundry/test/TypeTest.t.sol b/tests/foundry/test/TypeTest.t.sol
diff --git a/tests/specs/concrete-rules.txt b/tests/specs/concrete-rules.txt
