Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Contradictory formula in SSTORE (CONSTANTINOPLE) #287

Closed
nrryuya opened this issue Dec 17, 2018 · 5 comments
Closed

Contradictory formula in SSTORE (CONSTANTINOPLE) #287

nrryuya opened this issue Dec 17, 2018 · 5 comments

Comments

@nrryuya
Copy link

nrryuya commented Dec 17, 2018 •
edited
Loading

TL;DR

KEVM fails while symbolic execution of SSTORE and outputs java.lang.AssertionError at org.kframework.backend.java.symbolic.ConjunctiveFormula.implies(ConjunctiveFormula.java:848)
in CONSTANTINOPLE mode.

Targets

  • target contract in Vyper(v0.1.0b4)
data: uint256

@public
def setOne():
    self.data = 1

Error

STEP 549 v1 : 39.774 s, 		406 MB
===================
<k>(#KSequence(____EVM(SSTORE_EVM(.KList),, Int(#"0"),, Int(#"1")), #pc[_]_EVM(SSTORE_EVM(.KList)), #execute_EVM(.KList)))
<output>(_1201_1369:WordStack)
<statusCode>(_1203_1371:StatusCode)
<localMem>
...
</localMem>
<pc>(Int(#"177"))
<gas>(#if_#then_#else_#fi_K-EQUAL(_==K_(DATA_1368:Int,, Int(#"1")),, Int(#"99672"),, #if_#then_#else_#fi_K-EQUAL(_==K_(DATA_1368:Int,, Int(#"0")),, Int(#"79872"),, Int(#"94872"))))
<wordStack>(.WordStack_EVM-DATA(.KList))
accounts: 1
<acctID>(ACCT_ID_1367:Int)
<storage>(Int(#"0") |-> DATA_1368:Int   _1238_1406:Map)
/\
ConjunctiveFormula(
  equalities:
    _==K_(_<=Int__INT(Int(#"0"),, ACCT_ID_1367:Int),, Bool(#"true"))
    _==K_(_<=Int__INT(Int(#"0"),, CALLER_ID_1412:Int),, Bool(#"true"))
    _==K_(_<=Int__INT(Int(#"0"),, CALL_DEPTH_1366:Int),, Bool(#"true"))
    _==K_(_<=Int__INT(Int(#"0"),, DATA_1368:Int),, Bool(#"true"))
    _==K_(_<=Int__INT(Int(#"0"),, ORIGIN_ID_1365:Int),, Bool(#"true"))
    _==K_(_<Int__INT(ACCT_ID_1367:Int,, Int(#"1461501637330902918203684832716283019655932542976")),, Bool(#"true"))
    _==K_(_<Int__INT(CALLER_ID_1412:Int,, Int(#"1461501637330902918203684832716283019655932542976")),, Bool(#"true"))
    _==K_(_<Int__INT(CALL_DEPTH_1366:Int,, Int(#"1024")),, Bool(#"true"))
    _==K_(_<Int__INT(DATA_1368:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639936")),, Bool(#"true"))
    _==K_(_<Int__INT(ORIGIN_ID_1365:Int,, Int(#"1461501637330902918203684832716283019655932542976")),, Bool(#"true"))
)

Exception while evaluating functional term:
	#if_#then_#else_#fi_K-EQUAL(_andBool_(notBool_(_==K_(DATA_1368:Int,, Int(#"1"))),, _==K_(DATA_1368:Int,, Int(#"1"))),, #if_#then_#else_#fi_K-EQUAL(_==K_(DATA_1368:Int,, Int(#"0")),, Int(#"19800"),, Int(#"4800")),, Int(#"0"))
and applying the rule
	rule #if_#then_#else_#fi_K-EQUAL(R_C_595:Bool,, R_B1_596:K,, R__10_597:K) => R_B1_596:K requires [R_C_595:Bool] ensures [Bool(#"true")] [Location: Optional[Location(751,8,751,56)], Optional[Source(/Users/ryuya.nakamura/work/experiments/verified-vyper-contracts/k/.build/k/k-distribution/target/release/k/include/builtin/domains.k)]]

Exception message: java.lang.AssertionError


Exception while evaluating functional term:
	Rsstore(CONSTANTINOPLE_EVM(.KList),, Int(#"1"),, DATA_1368:Int,, DATA_1368:Int)
and applying the rule
	rule Rsstore(R_SCHED_1149:Schedule,, R_NEW_1150:Int,, R_CURR_1147:Int,, R_ORIG_1148:Int) => #if_#then_#else_#fi_K-EQUAL(_andBool_(_andBool_(_=/=Int__INT(R_CURR_1147:Int,, R_NEW_1150:Int),, _==Int_(R_ORIG_1148:Int,, R_CURR_1147:Int)),, _==Int_(R_NEW_1150:Int,, Int(#"0"))),, _<_>_EVM(Rsstoreclear_EVM(.KList),, R_SCHED_1149:Schedule),, _+Int_(#if_#then_#else_#fi_K-EQUAL(_andBool_(_andBool_(_=/=Int__INT(R_CURR_1147:Int,, R_NEW_1150:Int),, _=/=Int__INT(R_ORIG_1148:Int,, R_CURR_1147:Int)),, _=/=Int__INT(R_ORIG_1148:Int,, Int(#"0"))),, #if_#then_#else_#fi_K-EQUAL(_==Int_(R_CURR_1147:Int,, Int(#"0")),, _-Int__INT(Int(#"0"),, _<_>_EVM(Rsstoreclear_EVM(.KList),, R_SCHED_1149:Schedule)),, #if_#then_#else_#fi_K-EQUAL(_==Int_(R_NEW_1150:Int,, Int(#"0")),, _<_>_EVM(Rsstoreclear_EVM(.KList),, R_SCHED_1149:Schedule),, Int(#"0"))),, Int(#"0")),, #if_#then_#else_#fi_K-EQUAL(_andBool_(_=/=Int__INT(R_CURR_1147:Int,, R_NEW_1150:Int),, _==Int_(R_ORIG_1148:Int,, R_NEW_1150:Int)),, _-Int__INT(#if_#then_#else_#fi_K-EQUAL(_==Int_(R_ORIG_1148:Int,, Int(#"0")),, _<_>_EVM(Gsstoreset_EVM(.KList),, R_SCHED_1149:Schedule),, _<_>_EVM(Gsstorereset_EVM(.KList),, R_SCHED_1149:Schedule)),, _<_>_EVM(Gsload_EVM(.KList),, R_SCHED_1149:Schedule)),, Int(#"0")))) requires [_<<_>>_EVM(Ghasdirtysstore_EVM(.KList),, R_SCHED_1149:Schedule)] ensures [Bool(#"true")] [Location: Optional[Location(2200,10,2215,43)], Optional[Source(/Users/ryuya.nakamura/work/experiments/verified-vyper-contracts/k/.build/evm-semantics/.build/java/evm.k)]]

Exception message: java.lang.AssertionError

Term throwing exception
============================


<generatedTop>(<k>(#KSequence(____EVM(SSTORE_EVM(.KList),, Int(#"0"),, Int(#"1")), #pc[_]_EVM(SSTORE_EVM(.KList)), #execute_EVM(.KList))),, <exit-code>(Int(#"1")),, <mode>(NORMAL(.KList)),, <schedule>(CONSTANTINOPLE_EVM(.KList)),, <analysis>(.Map),, <ethereum>(<evm>(<output>(_1201_1369:WordStack),, <statusCode>(_1203_1371:StatusCode),, <callStack>(_1204_1372:List),, <interimStates>(_1205_1373:List),, <touchedAccounts>(_1206_1374:Set),, <callState>(<program>(CodeMap(42)),, <programBytes>(1),, <id>(ACCT_ID_1367:Int),, <caller>(CALLER_ID_1412:Int),, <callData>(_:__EVM-DATA(Int(#"78"),, _:__EVM-DATA(Int(#"233"),, _:__EVM-DATA(Int(#"252"),, _:__EVM-DATA(Int(#"217"),, .WordStack_EVM-DATA(.KList)))))),, <callValue>(Int(#"0")),, <wordStack>(.WordStack_EVM-DATA(.KList)),, <localMem>(Int(#"28") |-> Int(#"78") Int(#"29") |-> Int(#"233") Int(#"30") |-> Int(#"252") Int(#"31") |-> Int(#"217") Int(#"32") |-> Int(#"0") Int(#"33") |-> Int(#"0") Int(#"34") |-> Int(#"0") Int(#"35") |-> Int(#"0") Int(#"36") |-> Int(#"0") Int(#"37") |-> Int(#"0") Int(#"38") |-> Int(#"0") Int(#"39") |-> Int(#"0") Int(#"40") |-> Int(#"0") Int(#"41") |-> Int(#"0") Int(#"42") |-> Int(#"0") Int(#"43") |-> Int(#"1") Int(#"44") |-> Int(#"0") Int(#"45") |-> Int(#"0") Int(#"46") |-> Int(#"0") Int(#"47") |-> Int(#"0") Int(#"48") |-> Int(#"0") Int(#"49") |-> Int(#"0") Int(#"50") |-> Int(#"0") Int(#"51") |-> Int(#"0") Int(#"52") |-> Int(#"0") Int(#"53") |-> Int(#"0") Int(#"54") |-> Int(#"0") Int(#"55") |-> Int(#"0") Int(#"56") |-> Int(#"0") Int(#"57") |-> Int(#"0") Int(#"58") |-> Int(#"0") Int(#"59") |-> Int(#"0") Int(#"60") |-> Int(#"0") Int(#"61") |-> Int(#"0") Int(#"62") |-> Int(#"0") Int(#"63") |-> Int(#"0") Int(#"64") |-> Int(#"0") Int(#"65") |-> Int(#"0") Int(#"66") |-> Int(#"0") Int(#"67") |-> Int(#"0") Int(#"68") |-> Int(#"0") Int(#"69") |-> Int(#"0") Int(#"70") |-> Int(#"0") Int(#"71") |-> Int(#"0") Int(#"72") |-> Int(#"0") Int(#"73") |-> Int(#"0") Int(#"74") |-> Int(#"0") Int(#"75") |-> Int(#"0") Int(#"76") |-> Int(#"0") Int(#"77") |-> Int(#"0") Int(#"78") |-> Int(#"0") Int(#"79") |-> Int(#"0") Int(#"80") |-> Int(#"127") Int(#"81") |-> Int(#"255") Int(#"82") |-> Int(#"255") Int(#"83") |-> Int(#"255") Int(#"84") |-> Int(#"255") Int(#"85") |-> Int(#"255") Int(#"86") |-> Int(#"255") Int(#"87") |-> Int(#"255") Int(#"88") |-> Int(#"255") Int(#"89") |-> Int(#"255") Int(#"90") |-> Int(#"255") Int(#"91") |-> Int(#"255") Int(#"92") |-> Int(#"255") Int(#"93") |-> Int(#"255") Int(#"94") |-> Int(#"255") Int(#"95") |-> Int(#"255") Int(#"96") |-> Int(#"255") Int(#"97") |-> Int(#"255") Int(#"98") |-> Int(#"255") Int(#"99") |-> Int(#"255") Int(#"100") |-> Int(#"255") Int(#"101") |-> Int(#"255") Int(#"102") |-> Int(#"255") Int(#"103") |-> Int(#"255") Int(#"104") |-> Int(#"255") Int(#"105") |-> Int(#"255") Int(#"106") |-> Int(#"255") Int(#"107") |-> Int(#"255") Int(#"108") |-> Int(#"255") Int(#"109") |-> Int(#"255") Int(#"110") |-> Int(#"255") Int(#"111") |-> Int(#"255") Int(#"112") |-> Int(#"128") Int(#"113") |-> Int(#"0") Int(#"114") |-> Int(#"0") Int(#"115") |-> Int(#"0") Int(#"116") |-> Int(#"0") Int(#"117") |-> Int(#"0") Int(#"118") |-> Int(#"0") Int(#"119") |-> Int(#"0") Int(#"120") |-> Int(#"0") Int(#"121") |-> Int(#"0") Int(#"122") |-> Int(#"0") Int(#"123") |-> Int(#"0") Int(#"124") |-> Int(#"0") Int(#"125") |-> Int(#"0") Int(#"126") |-> Int(#"0") Int(#"127") |-> Int(#"0") Int(#"128") |-> Int(#"0") Int(#"129") |-> Int(#"0") Int(#"130") |-> Int(#"0") Int(#"131") |-> Int(#"0") Int(#"132") |-> Int(#"0") Int(#"133") |-> Int(#"0") Int(#"134") |-> Int(#"0") Int(#"135") |-> Int(#"0") Int(#"136") |-> Int(#"0") Int(#"137") |-> Int(#"0") Int(#"138") |-> Int(#"0") Int(#"139") |-> Int(#"1") Int(#"140") |-> Int(#"42") Int(#"141") |-> Int(#"5") Int(#"142") |-> Int(#"241") Int(#"143") |-> Int(#"255") Int(#"144") |-> Int(#"255") Int(#"145") |-> Int(#"255") Int(#"146") |-> Int(#"255") Int(#"147") |-> Int(#"255") Int(#"148") |-> Int(#"255") Int(#"149") |-> Int(#"255") Int(#"150") |-> Int(#"255") Int(#"151") |-> Int(#"255") Int(#"152") |-> Int(#"255") Int(#"153") |-> Int(#"255") Int(#"154") |-> Int(#"255") Int(#"155") |-> Int(#"253") Int(#"156") |-> Int(#"171") Int(#"157") |-> Int(#"244") Int(#"158") |-> Int(#"28") Int(#"159") |-> Int(#"0") Int(#"160") |-> Int(#"255") Int(#"161") |-> Int(#"255") Int(#"162") |-> Int(#"255") Int(#"163") |-> Int(#"255") Int(#"164") |-> Int(#"255") Int(#"165") |-> Int(#"255") Int(#"166") |-> Int(#"255") Int(#"167") |-> Int(#"255") Int(#"168") |-> Int(#"255") Int(#"169") |-> Int(#"255") Int(#"170") |-> Int(#"255") Int(#"171") |-> Int(#"254") Int(#"172") |-> Int(#"213") Int(#"173") |-> Int(#"250") Int(#"174") |-> Int(#"14") Int(#"175") |-> Int(#"0") Int(#"176") |-> Int(#"0") Int(#"177") |-> Int(#"0") Int(#"178") |-> Int(#"0") Int(#"179") |-> Int(#"0") Int(#"180") |-> Int(#"0") Int(#"181") |-> Int(#"0") Int(#"182") |-> Int(#"0") Int(#"183") |-> Int(#"0") Int(#"184") |-> Int(#"0") Int(#"185") |-> Int(#"0") Int(#"186") |-> Int(#"0") Int(#"187") |-> Int(#"0") Int(#"188") |-> Int(#"0") Int(#"189") |-> Int(#"0") Int(#"190") |-> Int(#"0") Int(#"191") |-> Int(#"0")   ),, <pc>(Int(#"177")),, <gas>(#if_#then_#else_#fi_K-EQUAL(_==K_(DATA_1368:Int,, Int(#"1")),, Int(#"99672"),, #if_#then_#else_#fi_K-EQUAL(_==K_(DATA_1368:Int,, Int(#"0")),, Int(#"79872"),, Int(#"94872")))),, <memoryUsed>(Int(#"6")),, <previousGas>(Int(#"99872")),, <static>(Bool(#"false")),, <callDepth>(CALL_DEPTH_1366:Int)),, <substate>(<selfDestruct>(_1215_1383:Set),, <log>(_1216_1384:List),, <refund>(_1217_1385:Int)),, <gasPrice>(_1218_1386:Int),, <origin>(ORIGIN_ID_1365:Int),, <previousHash>(_1219_1387:Int),, <ommersHash>(_1220_1388:Int),, <coinbase>(_1221_1389:Int),, <stateRoot>(_1222_1390:Int),, <transactionsRoot>(_1223_1391:Int),, <receiptsRoot>(_1224_1392:Int),, <logsBloom>(_1225_1393:WordStack),, <difficulty>(_1226_1394:Int),, <number>(_1227_1395:Int),, <gasLimit>(_1228_1396:Int),, <gasUsed>(_1229_1397:Int),, <timestamp>(_1230_1398:Int),, <extraData>(_1231_1399:WordStack),, <mixHash>(_1232_1400:Int),, <blockNonce>(_1233_1401:Int),, <ommerBlockHeaders>(_1234_1402:JSON),, <blockhash>(_1235_1403:List)),, <network>(<activeAccounts>(ACCT_ID_1367:Int_1236_1404:Set),, <accounts>(<acctID>(ACCT_ID_1367:Int) |-> <account>(<acctID>(ACCT_ID_1367:Int),, <balance>(_1237_1405:Int),, <code>(1),, <storage>(Int(#"0") |-> DATA_1368:Int   _1238_1406:Map),, <origStorage>(Int(#"0") |-> DATA_1368:Int   _1239_1407:Map),, <nonce>(_1240_1408:Int))   ),, <txOrder>(_1241_1409:List),, <txPending>(_1242_1410:List),, <messages>(_1243_1411:Map))))
/\
#And(_==K_(_<=Int__INT(Int(#"0"),, ACCT_ID_1367:Int),, Bool(#"true")),, 
#And(_==K_(_<Int__INT(ACCT_ID_1367:Int,, Int(#"1461501637330902918203684832716283019655932542976")),, Bool(#"true")),, 
#And(_==K_(_<=Int__INT(Int(#"0"),, CALLER_ID_1412:Int),, Bool(#"true")),, 
#And(_==K_(_<Int__INT(CALLER_ID_1412:Int,, Int(#"1461501637330902918203684832716283019655932542976")),, Bool(#"true")),, 
#And(_==K_(_<=Int__INT(Int(#"0"),, ORIGIN_ID_1365:Int),, Bool(#"true")),, 
#And(_==K_(_<Int__INT(ORIGIN_ID_1365:Int,, Int(#"1461501637330902918203684832716283019655932542976")),, Bool(#"true")),, 
#And(_==K_(_<=Int__INT(Int(#"0"),, CALL_DEPTH_1366:Int),, Bool(#"true")),, 
#And(_==K_(_<Int__INT(CALL_DEPTH_1366:Int,, Int(#"1024")),, Bool(#"true")),, 
#And(_==K_(_<=Int__INT(Int(#"0"),, DATA_1368:Int),, Bool(#"true")),, _==K_(_<Int__INT(DATA_1368:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639936")),, Bool(#"true")))))))))))
java.lang.AssertionError
	at org.kframework.backend.java.symbolic.ConjunctiveFormula.implies(ConjunctiveFormula.java:848)
	at org.kframework.backend.java.util.RewriteEngineUtils.evaluateConditions(RewriteEngineUtils.java:147)
	at org.kframework.backend.java.util.RewriteEngineUtils.lambda$evaluateConditions$0(RewriteEngineUtils.java:186)
	at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:195)
	at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1492)
	at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:484)
	at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:474)
	at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:913)
	at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
	at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:578)
	at org.kframework.backend.java.util.RewriteEngineUtils.evaluateConditions(RewriteEngineUtils.java:188)
	at org.kframework.backend.java.symbolic.PatternMatcher.match(PatternMatcher.java:118)
	at org.kframework.backend.java.kil.KItem$KItemOperations.evaluateFunction(KItem.java:544)
	at org.kframework.backend.java.kil.KItem$KItemOperations.resolveFunctionAndAnywhere(KItem.java:409)
	at org.kframework.backend.java.kil.KItem.resolveFunctionAndAnywhere(KItem.java:337)
	at org.kframework.backend.java.util.RewriteEngineUtils.construct(RewriteEngineUtils.java:292)
	at org.kframework.backend.java.kil.KItem$KItemOperations.evaluateFunction(KItem.java:565)
	at org.kframework.backend.java.kil.KItem$KItemOperations.resolveFunctionAndAnywhere(KItem.java:409)
	at org.kframework.backend.java.kil.KItem.resolveFunctionAndAnywhere(KItem.java:337)
	at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:103)
	at org.kframework.backend.java.kil.KItem.accept(KItem.java:853)
	at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:246)
	at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:111)
	at org.kframework.backend.java.kil.KList.accept(KList.java:150)
	at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:153)
	at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:102)
	at org.kframework.backend.java.kil.KItem.accept(KItem.java:853)
	at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:246)
	at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:111)
	at org.kframework.backend.java.kil.KList.accept(KList.java:150)
	at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:153)
	at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:102)
	at org.kframework.backend.java.kil.KItem.accept(KItem.java:853)
	at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:246)
	at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:111)
	at org.kframework.backend.java.kil.KList.accept(KList.java:150)
	at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:153)
	at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:102)
	at org.kframework.backend.java.kil.KItem.accept(KItem.java:853)
	at org.kframework.backend.java.kil.Term.substituteAndEvaluate(Term.java:80)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.buildRHS(SymbolicRewriter.java:342)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.buildRHS(SymbolicRewriter.java:362)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.buildRHS(SymbolicRewriter.java:362)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.buildRHS(SymbolicRewriter.java:362)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:199)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.proveRule(SymbolicRewriter.java:737)
	at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.lambda$prove$2(InitializeRewriter.java:237)
	at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:195)
	at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:177)
	at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1492)
	at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:484)
	at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:474)
	at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:913)
	at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
	at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:578)
	at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.prove(InitializeRewriter.java:240)
	at org.kframework.kprove.KProve.run(KProve.java:68)
	at org.kframework.kprove.KProveFrontEnd.run(KProveFrontEnd.java:96)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
	at org.kframework.main.Main.runApplication(Main.java:118)
	at org.kframework.main.Main.runApplication(Main.java:107)
	at org.kframework.main.Main.main(Main.java:53)

gist

Issue

In this part of the above,

Exception while evaluating functional term:
	#if_#then_#else_#fi_K-EQUAL(_andBool_(notBool_(_==K_(DATA_1368:Int,, Int(#"1"))),, _==K_(DATA_1368:Int,, Int(#"1"))),, #if_#then_#else_#fi_K-EQUAL(_==K_(DATA_1368:Int,, Int(#"0")),, Int(#"19800"),, Int(#"4800")),, Int(#"0"))

_andBool_(notBool_(_==K_(DATA_1368:Int,, Int(#"1"))),, _==K_(DATA_1368:Int,, Int(#"1"))) is apparently contradictory.

Therefore I guess the AssertionError condition isFalseFromContradictions() is the case.

Notes

  • This issue doesn't appeared in BYZANTIUM. The BYZANTIUM version of the spec above passed.
  • I found the same error in Solidity code as the below.
pragma solidity ^0.5.0;


contract Test {
    uint256 data;
    function setZero() public {
        data = 0;
    }
}
@nrryuya nrryuya mentioned this issue Dec 18, 2018
Merged
@daejunpark
Copy link
Contributor

@denis-bogdanas Do you have an idea with this? Is it something to do with the contradictory terms you fixed before?

@denis-bogdanas
Copy link
Contributor

The isFalseExtended() probably shouldn't be used on assert. I replaced it with simple isFalse(). The fix with isFalseExtended() shouldn't be needed now that we have better translation to Z3, but doesn't hurt either.

@nrryuya Can you confirm if this fixed your issue? Also, can you attach a spec for your solidity example above. We want to add it to our test suite.

@nrryuya
Copy link
Author

nrryuya commented Dec 20, 2018

@denis-bogdanas

Thank you. I replaced like assert !constraint.isFalse(); and the spec passed.

This gist is the spec of simple setZero() function in Solidity.

@nrryuya nrryuya mentioned this issue Dec 26, 2018
Open
@nrryuya nrryuya mentioned this issue Jan 24, 2019
Closed
@ehildenb
Copy link
Member

This should be fixed in both K master and here (because we now use Byzantium).

@denis-bogdanas
Copy link
Contributor

Yes it was upstreamed to master.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@denis-bogdanas @daejunpark @ehildenb @nrryuya