Skip to content

Instantly share code, notes, and snippets.

@iamchrissmith
Created July 16, 2019 23:56
Show Gist options
  • Save iamchrissmith/7a4635c5dbe21bf40d0c22ebc308159f to your computer and use it in GitHub Desktop.
Save iamchrissmith/7a4635c5dbe21bf40d0c22ebc308159f to your computer and use it in GitHub Desktop.
SPEC ERROR: /Users/chrissmith/Projects/k-ds-guard/out/specs/617021af8de987b5d4f7d2a2afac1a72fd17c33b75cdc5f1440117d544b77a8e.k Location(12,3,180,36)
==================================
Success execution paths: 0
Failed execution paths: 1
Paths in progress: 1
Longest path: 131 steps
Stats for each phase, time, used memory, implicit main GC time percentage:
Total                 :  218.558 s,	  541 MB, gc:  0.649 %
  Parsing             :  206.018 s,	  135 MB, gc:  0.610 %
  Init                :    1.854 s,	  485 MB, gc:  0.917 %
  Execution           :   10.685 s,	  541 MB, gc:  1.357 %

Init+Execution time:      12.539 s
  query build time                 :    0.072 s,      #         67
  Z3 Regular rule implication time :    0.305 s,      #         16
      unsat (proved):       16
    cached queries:       2
  Z3 Function rule implication time:    0.231 s,      #         10
      unknown       :       10
    cached queries:       2
  Z3 Spec rule implication time    :    0.015 s,      #          1
      unsat (proved):       1
  Z3 Regular rule constraint time  :    0.749 s,      #         39
      unknown       :       21
      unsat (proved):       17
  Z3 Spec rule constraint time     :    0.021 s,      #          1
      unknown       :       1

  Time and top-level event counts:
  resolveFunctionAndAnywhere time  :    1.654 s,      #       3610
    evaluateFunction time            :    1.640 s,      #        777
      builtin evaluation               :           ,      #        127
      function rule                    :           ,      #        151
      sort predicate                   :           ,      #         56
      no rule applicable               :           ,      #        443
    applyAnywhereRules time          :    0.001 s,      #       2083
      no anywhere rules                :           ,      #       2083
    remaining time & # cached        :    0.013 s,      #        750
  impliesSMT time                  :    0.592 s,      #         31

  Recursive event counts:
  resolveFunctionAndAnywhere time  :           ,      #      94100
    evaluateFunction time            :           ,      #      42311
      builtin evaluation               :           ,      #      23852
      function rule                    :           ,      #      18278
      sort predicate                   :           ,      #         69
      no rule applicable               :           ,      #        107
    applyAnywhereRules time          :           ,      #       9021
      no anywhere rules                :           ,      #       9021
    # cached                         :           ,      #      42768

Max memory : 10240 MB
==================================

[Error] Critical: Z3 crashed on input query:
(declare-sort WordStack)
(declare-sort KItem)
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun asWord (WordStack) Int)
(declare-fun buf (Int Int) WordStack)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun _dotWS () WordStack)
(declare-fun _plusWS_ (WordStack WordStack) WordStack)
(declare-fun _WS_ (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun smt_keccak (WordStack) Int)
(declare-fun smt_nthbyteof (Int Int Int) Int)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(assert (forall ((|R_I_260| Int)) (= (chop |R_I_260|) (mod |R_I_260| 115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(assert (forall ((|R__0_298| WordStack)(|R__1_299| Int)) (= (>= (sizeWordStackAux |R__0_298| |R__1_299|) 0) true)))
(declare-fun |CD_1572| () WordStack)
(declare-fun |R_CD| () WordStack)
(declare-fun |ACCT_ID_1570| () Int)
(declare-fun |CALLER_ID_1648| () Int)
(declare-fun |ORIGIN_ID_1561| () Int)
(declare-fun |TIME_1638| () Int)
(declare-fun |ACCT_ID_balance_1562| () Int)
(declare-fun |ECREC_BAL_1560| () Int)
(declare-fun |SHA256_BAL_1571| () Int)
(declare-fun |RIP160_BAL_1649| () Int)
(declare-fun |ID_BAL_1559| () Int)
(declare-fun |MODEXP_BAL_1564| () Int)
(declare-fun |ECADD_BAL_1642| () Int)
(declare-fun |ECMUL_BAL_1563| () Int)
(declare-fun |ECPAIRING_BAL_1641| () Int)
(declare-fun |VCallDepth_1643| () Int)
(declare-fun |ABI_src_1569| () Int)
(declare-fun |Can_1583| () Int)
(declare-fun |VGas_1639| () Int)
(declare-fun |_3000| () KItem)
(assert (and
	(= (_plusWS_ _3000 |CD_1572|) |R_CD|)
	(= (<= 0 |ACCT_ID_1570|) true)
	(= (<= |ACCT_ID_1570| 1461501637330902918203684832716283019655932542975) true)
	(= (< 0 |ACCT_ID_1570|) true)
	(= (<= 9 |ACCT_ID_1570|) true)
	(= (<= 0 |CALLER_ID_1648|) true)
	(= (<= |CALLER_ID_1648| 1461501637330902918203684832716283019655932542975) true)
	(= (<= 0 |ORIGIN_ID_1561|) true)
	(= (<= |ORIGIN_ID_1561| 1461501637330902918203684832716283019655932542975) true)
	(= (<= 0 |TIME_1638|) true)
	(= (<= |TIME_1638| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ACCT_ID_balance_1562|) true)
	(= (<= |ACCT_ID_balance_1562| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ECREC_BAL_1560|) true)
	(= (<= |ECREC_BAL_1560| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |SHA256_BAL_1571|) true)
	(= (<= |SHA256_BAL_1571| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |RIP160_BAL_1649|) true)
	(= (<= |RIP160_BAL_1649| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ID_BAL_1559|) true)
	(= (<= |ID_BAL_1559| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |MODEXP_BAL_1564|) true)
	(= (<= |MODEXP_BAL_1564| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ECADD_BAL_1642|) true)
	(= (<= |ECADD_BAL_1642| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ECMUL_BAL_1563|) true)
	(= (<= |ECMUL_BAL_1563| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ECPAIRING_BAL_1641|) true)
	(= (<= |ECPAIRING_BAL_1641| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= |VCallDepth_1643| 1024) true)
	(= (<= 0 |ABI_src_1569|) true)
	(= (<= |ABI_src_1569| 1461501637330902918203684832716283019655932542975) true)
	(= (<= 0 |Can_1583|) true)
	(= (<= |Can_1583| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= (sizeWordStackAux |CD_1572| 0) 1250000000) true)
	(= (>= |VGas_1639| 3000000) true)))
result:
(error "line 114 column 29: Sort mismatch at argument #1 for function (declare-fun _plusWS_ (WordStack WordStack) WordStack) supplied sort is KItem")
unknown

while checking satisfiability for:
ConjunctiveFormula(
  substitutions:
    _==K_(ABI_dst_1567:Int,, ABI_src_1569:Int)
    _==K_(R_DotVar1:K,, #KSequence(#pc[_]_EVM(CALLDATASIZE_EVM(.KList)), #execute_EVM(.KList), CONTINUATION_1647:K))
    _==K_(VCallValue_1645:Int,, Int(#"0"))
  equalities:
    _==K_(_++_WS(#abiCallData(String(#""canCall""),, typedArgs(#address(ABI_src_1569:Int),, typedArgs(#address(ABI_src_1569:Int),, typedArgs(#bytes4(ABI_sig_1568:Int),, .List{"typedArgs"}(.KList))))),, CD_1572:WordStack),, R_CD:WordStack)
    _==K_(_<=Int_(ABI_src_1569:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
    _==K_(_<=Int_(ACCT_ID_1570:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
    _==K_(_<=Int_(ACCT_ID_balance_1562:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(CALLER_ID_1648:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
    _==K_(_<=Int_(Can_1583:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(ECADD_BAL_1642:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(ECMUL_BAL_1563:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(ECPAIRING_BAL_1641:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(ECREC_BAL_1560:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(ID_BAL_1559:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ABI_src_1569:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ACCT_ID_1570:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ACCT_ID_balance_1562:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, CALLER_ID_1648:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, Can_1583:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ECADD_BAL_1642:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ECMUL_BAL_1563:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ECPAIRING_BAL_1641:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ECREC_BAL_1560:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ID_BAL_1559:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, MODEXP_BAL_1564:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, ORIGIN_ID_1561:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, RIP160_BAL_1649:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, SHA256_BAL_1571:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"0"),, TIME_1638:Int),, Bool(#"true"))
    _==K_(_<=Int_(Int(#"9"),, ACCT_ID_1570:Int),, Bool(#"true"))
    _==K_(_<=Int_(MODEXP_BAL_1564:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(ORIGIN_ID_1561:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
    _==K_(_<=Int_(RIP160_BAL_1649:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(SHA256_BAL_1571:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(TIME_1638:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
    _==K_(_<=Int_(VCallDepth_1643:Int,, Int(#"1024")),, Bool(#"true"))
    _==K_(_<=Int_(sizeWordStackAux(CD_1572:WordStack,, Int(#"0")),, Int(#"1250000000")),, Bool(#"true"))
    _==K_(_<Int_(Int(#"0"),, ACCT_ID_1570:Int),, Bool(#"true"))
    _==K_(_>=Int_(VGas_1639:Int,, Int(#"3000000")),, Bool(#"true"))
)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment