search

marcoeilers / nagini

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
Mozilla Public License 2.0
233 stars 8 forks source link

Disjunction in Requires / Ensures crashes Nagini #186

Closed omkar-ethz closed 7 months ago

omkar-ethz commented 7 months ago

Minimal example:

from nagini_contracts.contracts import *

@Predicate
def pred1() -> bool:
    return True

@Predicate
def pred2() -> bool:
    return True

def crash() -> None:
    Requires(pred1() or pred2())

May replace Requires with Ensures to trigger the same error.

Expected output: Maybe Translation failed? Disjunction not supported in Assertions

Actual Output:

Translation successful.
java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: scala.MatchError: acc(pred1(), write) (of class viper.silver.ast.PredicateAccessPredicate)
    at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
    at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
    at viper.silicon.Silicon.verify(Silicon.scala:200)
    at viper.silicon.Silicon.verify(Silicon.scala:158)
Caused by: java.util.concurrent.ExecutionException: scala.MatchError: acc(pred1(), write) (of class viper.silver.ast.PredicateAccessPredicate)
    at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
    at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
    at viper.silicon.verifier.DefaultMasterVerifier.$anonfun$verify$9(DefaultMasterVerifier.scala:238)
    at scala.collection.TraversableLike.$anonfun$flatMap$1(TraversableLike.scala:240)
    at scala.collection.immutable.List.foreach(List.scala:388)
    at scala.collection.TraversableLike.flatMap(TraversableLike.scala:240)
    at scala.collection.TraversableLike.flatMap$(TraversableLike.scala:237)
    at scala.collection.immutable.List.flatMap(List.scala:351)
    at viper.silicon.verifier.DefaultMasterVerifier.verify(DefaultMasterVerifier.scala:238)
    at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:234)
    at viper.silicon.Silicon$$anon$1.call(Silicon.scala:194)
    at viper.silicon.Silicon$$anon$1.call(Silicon.scala:193)
    at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
    at java.base/java.lang.Thread.run(Thread.java:840)
Caused by: scala.MatchError: acc(pred1(), write) (of class viper.silver.ast.PredicateAccessPredicate)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:150)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.evaluator$.evalSeqShortCircuit(Evaluator.scala:1368)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:304)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.producer$.produceTlc(Producer.scala:422)
    at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:187)
    at viper.silicon.rules.producer$.produceTlcs(Producer.scala:155)
    at viper.silicon.rules.producer$.$anonfun$produceTlcs$1(Producer.scala:156)
    at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:189)
    at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:204)
    at viper.silicon.rules.producer$.$anonfun$produceTlc$32(Producer.scala:424)
    at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:91)
    at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:143)
    at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:405)
    at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:76)
    at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:79)
    at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:91)
    at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:143)
    at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:405)
    at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:76)
    at viper.silicon.rules.evaluator$.evals(Evaluator.scala:69)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:401)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
    at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:79)
    at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:91)
    at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:143)
    at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:405)
    at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:76)
    at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:79)
    at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:91)
    at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:143)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:160)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
    at viper.silicon.rules.evaluator$.evals(Evaluator.scala:69)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:401)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
    at viper.silicon.rules.evaluator$.evals(Evaluator.scala:69)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:401)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.producer$.produceTlc(Producer.scala:422)
    at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:187)
    at viper.silicon.rules.producer$.produceTlcs(Producer.scala:155)
    at viper.silicon.rules.producer$.$anonfun$produceTlcs$1(Producer.scala:156)
    at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:189)
    at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:204)
    at viper.silicon.rules.producer$.$anonfun$produceTlc$32(Producer.scala:424)
    at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:91)
    at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:143)
    at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1002)
    at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:91)
    at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:143)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:154)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$1(Evaluator.scala:1001)
    at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:91)
    at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:143)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:160)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1000)
    at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
    at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:128)
    at viper.silicon.rules.evaluator$.eval(Evaluator.scala:89)
    at viper.silicon.rules.producer$.produceTlc(Producer.scala:422)
    at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:187)
    at viper.silicon.rules.producer$.produceTlcs(Producer.scala:155)
    at viper.silicon.rules.producer$.produces(Producer.scala:127)
    at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$8(MethodSupporter.scala:80)
    at viper.silicon.rules.executionFlowController$.$anonfun$locally$1(ExecutionFlowController.scala:96)
    at viper.silicon.rules.executionFlowController$.locallyWithResult(ExecutionFlowController.scala:59)
    at viper.silicon.rules.executionFlowController$.locally(ExecutionFlowController.scala:96)
    at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.verify(MethodSupporter.scala:79)
    at viper.silicon.verifier.DefaultMasterVerifier.$anonfun$verify$6(DefaultMasterVerifier.scala:215)
    at viper.silicon.verifier.VerificationPoolManager$SlaveBorrowingVerificationTask.call(VerificationPoolManager.scala:109)
    at viper.silicon.verifier.VerificationPoolManager$SlaveBorrowingVerificationTask.call(VerificationPoolManager.scala:100)
    ... 4 more

Traceback (most recent call last):
  File "/home/omkar/ethz/hs23/prog-ver/nagini-env/lib/python3.8/site-packages/nagini_translation/main.py", line 190, in verify
    vresult = verifier.verify(modules, prog, arp=arp, sif=sif)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-env/lib/python3.8/site-packages/nagini_translation/verifier.py", line 129, in verify
    result = self.silicon.verify(prog)
jpype._jclass.java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: scala.MatchError: acc(pred1(), write) (of class viper.silver.ast.PredicateAccessPredicate)
Verification completed.
Traceback (most recent call last):
  File "/home/omkar/ethz/hs23/prog-ver/nagini-env/bin/nagini", line 8, in <module>
    sys.exit(main())
  File "/home/omkar/ethz/hs23/prog-ver/nagini-env/lib/python3.8/site-packages/nagini_translation/main.py", line 357, in main
    translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-env/lib/python3.8/site-packages/nagini_translation/main.py", line 393, in translate_and_verify
    print(vresult.to_string(args.ide_mode, args.show_viper_errors))
AttributeError: 'NoneType' object has no attribute 'to_string'
marcoeilers commented 7 months ago

Thanks for reporting these! I'll try to get to them next week or the one after.

marcoeilers commented 7 months ago

Fixed in #187