Return failure data from pass chain executions #2186

shonfeder · 2022-09-28T03:11:35Z

This PR enriches the PassResult so that it can it can include data about the reasons for pass failures. The approach here is currently going for the shortest path to getting the needed JSON-encodable data for RPC calls.

Further work could be useful to impose a more rigorous interface. In particular, it could be helpful to reorganize the package dependencies so that the failure data returned by different passes could be enumerated in a case class, allowing static specification of the supported data structures. This is apposed to he approach taken here, which just converts the pass data into ujson. The latter approach is expedient given the current motivating need, but won't be nice to work with if we decide we want to use this data for purposes other than returning RPC results.

Tests added for any new code
Ran make fmt-fix (or had formatting run automatically on all files edited)
Documentation added for any new functionality
Entries added to ./unreleased/ for any new functionality

codecov-commenter · 2022-09-30T15:13:46Z

Codecov Report

Merging #2186 (6a43f7f) into main (38d0666) will decrease coverage by 0.00%.
The diff coverage is 66.98%.

@@            Coverage Diff             @@
##             main    #2186      +/-   ##
==========================================
- Coverage   80.63%   80.62%   -0.01%     
==========================================
  Files         423      426       +3     
  Lines       13898    13927      +29     
  Branches     1887     1840      -47     
==========================================
+ Hits        11206    11229      +23     
- Misses       2692     2698       +6

Impacted Files	Coverage Δ
...syte/apalache/infra/passes/PassChainExecutor.scala	`100.00% <ø> (ø)`
...at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala	`0.00% <0.00%> (ø)`
...at/forsyte/apalache/tla/tooling/opt/ParseCmd.scala	`0.00% <0.00%> (ø)`
.../at/forsyte/apalache/tla/tooling/opt/TestCmd.scala	`0.00% <0.00%> (ø)`
...orsyte/apalache/tla/tooling/opt/TranspileCmd.scala	`0.00% <0.00%> (ø)`
...orsyte/apalache/tla/tooling/opt/TypeCheckCmd.scala	`0.00% <0.00%> (ø)`
...syte/apalache/io/lir/ItfCounterexampleWriter.scala	`92.00% <0.00%> (ø)`
...e/apalache/tla/imp/passes/SanyParserPassImpl.scala	`55.17% <0.00%> (+5.17%)`	⬆️
...yte/apalache/tla/pp/passes/PreproPassPartial.scala	`56.66% <0.00%> (-1.96%)`	⬇️
.../typecheck/passes/LoggingTypeCheckerListener.scala	`50.00% <ø> (-16.67%)`	⬇️
... and 20 more

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

Cannot link to a type alias I guess

konnov

In general, this looks good to me. I can see how serialization for the server mode requires these changes. One thing I could not understand is: Why are we using upickle now? Is it a replacement for ujson or is it complimentary?

konnov · 2022-10-04T09:30:15Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Counterexample.scala

+  def apply(module: TlaModule, trace: DecodedExecution, invViolated: TlaEx): Counterexample = {
+    // TODO(shonfeder): This conversion seems kind of senseless: we just swap the tuple and convert the transition index to
+    // a string. Lots depends on this particular format, but it seems like a pretty pointless intermediary structure?
+    val states = trace.path.map(p => (p._2.toString, p._1))


Why do we convert an integer to a string here? Is it for the future compatibility, or is it because JSON has limitations on numbers?

I don't know why this conversion is done. In fact, I don't know why we transform a "tract" into this "states" structure at all. But several other structures depend on it, and i was trying to limit the scope the of this changeset. This was picked up from DumpFilesModelCheckerLIstener.scala line 41. I was thinking to remove this conversion in a followup, but could include it in this PR if you'd prefer. WDYT?

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/DumpFilesModelCheckerListener.scala

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Counterexample.scala

tla-io/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala

shonfeder

Thanks for the review!

I think I could use a bit more info on how to effect the reorganization you've suggested.

re: upickle -- ujson is a json specific library that is part of the upickle toolkit. upickle is a more general purpose serialization/deserialiation library, and it enables automated derivation of serializers and deserializers. It is being used here to automatically derive the converts for PassFailure and used for the serialization implicts in CheckerResult and Counterexample.

I expect I could do without it tho, if you think it'd better for us to avoid the dependency. WDYT?

shonfeder · 2022-10-04T12:17:50Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Counterexample.scala

+  def apply(module: TlaModule, trace: DecodedExecution, invViolated: TlaEx): Counterexample = {
+    // TODO(shonfeder): This conversion seems kind of senseless: we just swap the tuple and convert the transition index to
+    // a string. Lots depends on this particular format, but it seems like a pretty pointless intermediary structure?
+    val states = trace.path.map(p => (p._2.toString, p._1))


I don't know why this conversion is done. In fact, I don't know why we transform a "tract" into this "states" structure at all. But several other structures depend on it, and i was trying to limit the scope the of this changeset. This was picked up from DumpFilesModelCheckerLIstener.scala line 41. I was thinking to remove this conversion in a followup, but could include it in this PR if you'd prefer. WDYT?

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Counterexample.scala

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/DumpFilesModelCheckerListener.scala

Co-authored-by: Igor Konnov <igor@informal.systems>

shonfeder · 2022-10-05T03:08:01Z

Thanks for the review! Definitely improved thanks to the comments.

shonfeder · 2022-10-05T04:00:50Z

Welp, getting rid of that seemingly useless conversion to strings broke something in the tests, and they are proving to be quite brittle and hard to get signal from. All they'll tell me off the bat is:

[info] - JSON single state *** FAILED *** (56 milliseconds)
[info]   java.lang.AssertionError: assertion failed
[info]   at scala.Predef$.assert(Predef.scala:264)
[info]   at at.forsyte.apalache.io.lir.TestCounterexampleWriterBase.compare(TestCounterexampleWriterBase.scala:40)
[info]   at at.forsyte.apalache.io.lir.TestCounterexampleWriterBase.compare$(TestCounterexampleWriterBase.scala:23)
[info]   at at.forsyte.apalache.io.lir.TestCounterexampleWriter.compare(TestCounterexampleWriter.scala:11)
[info]   at at.forsyte.apalache.io.lir.TestCounterexampleWriter.$anonfun$new$7(TestCounterexampleWriter.scala:232)
[info]   at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
[info]   at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
[info]   at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
[info]   at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
[info]   at org.scalatest.Transformer.apply(Transformer.scala:22)

And getting feedback on the comparison doesn't help much:

[info] - JSON single state *** FAILED *** (12 milliseconds)
[info]   "...  "formalParams": [
[info]   [            
[info]             ],
[info]             "isRecursive": false,
[info]             "body": {
[info]               "type": "Untyped",
[info]               "kind": "ValEx",
[info]               "value": {
[info]                 "kind": "TlaBool",
[info]                 "value": true
[info]               }
[info]             }
[info]           },
[info]           {
[info]             "type": "Untyped",
[info]             "kind": "TlaOperDecl",
[info]             "name": "State0",
[info]             "formalParams": [
[info]               
[info]             ],
[info]             "isRecursive": false,
[info]             "body": {
[info]               "type": "Untyped",
[info]               "kind": "OperEx",
[info]               "oper": "AND",
[info]               "args": [
[info]                 {
[info]                   "type": "Untyped",
[info]                   "kind": "OperEx",
[info]                   "oper": "EQ",
[info]                   "args": [
[info]                     {
[info]                       "type": "Untyped",
[info]                       "kind": "NameEx",
[info]                       "name": "x"
[info]                     },
[info]                     {
[info]                       "type": "Untyped",
[info]                       "kind": "ValEx",
[info]                       "value": {
[info]                         "kind": "TlaInt",
[info]                         "value": 2
[info]                       }
[info]                     }
[info]                   ]
[info]                 }
[info]               ]
[info]             }
[info]           },
[info]           {
[info]             "type": "Untyped",
[info]             "kind": "TlaOperDecl",
[info]             "name": "InvariantViolation",
[info]             "formalParams": [
[info]               ]
[info]             ],
[info]         ..." did not equal "...  "formalParams": [
[info]   [
[info]             ],
[info]             "isRecursive": false,
[info]             "body": {
[info]               "type": "Untyped",
[info]               "kind": "ValEx",
[info]               "value": {
[info]                 "kind": "TlaBool",
[info]                 "value": true
[info]               }
[info]             }
[info]           },
[info]           {
[info]             "type": "Untyped",
[info]             "kind": "TlaOperDecl",
[info]             "name": "State0",
[info]             "formalParams": [
[info]   
[info]             ],
[info]             "isRecursive": false,
[info]             "body": {
[info]               "type": "Untyped",
[info]               "kind": "OperEx",
[info]               "oper": "AND",
[info]               "args": [
[info]                 {
[info]                   "type": "Untyped",
[info]                   "kind": "OperEx",
[info]                   "oper": "EQ",
[info]                   "args": [
[info]                     {
[info]                       "type": "Untyped",
[info]                       "kind": "NameEx",
[info]                       "name": "x"
[info]                     },
[info]                     {
[info]                       "type": "Untyped",
[info]                       "kind": "ValEx",
[info]                       "value": {
[info]                         "kind": "TlaInt",
[info]                         "value": 2
[info]                       }
[info]                     }
[info]                   ]
[info]                 }
[info]               ]
[info]             }
[info]           },
[info]           {
[info]             "type": "Untyped",
[info]             "kind": "TlaOperDecl",
[info]             "name": "InvariantViolation",
[info]             "formalParams": [
[info]   ]
[info]             ],
[info]         ..." (TestCounterexampleWriterBase.scala:41)
[info]   Analysis:
[info]   "...  "formalParams": [
[info] [            
[info]           ],
[info]           "isRecursive": false,
[info]           "body": {
[info]             "type": "Untyped",
[info]             "kind": "ValEx",
[info]             "value": {
[info]               "kind": "TlaBool",
[info]               "value": true
[info]             }
[info]           }
[info]         },
[info]         {
[info]           "type": "Untyped",
[info]           "kind": "TlaOperDecl",
[info]           "name": "State0",
[info]           "formalParams": [
[info]             
[info]           ],
[info]           "isRecursive": false,
[info]           "body": {
[info]             "type": "Untyped",
[info]             "kind": "OperEx",
[info]             "oper": "AND",
[info]             "args": [
[info]               {
[info]                 "type": "Untyped",
[info]                 "kind": "OperEx",
[info]                 "oper": "EQ",
[info]                 "args": [
[info]                   {
[info]                     "type": "Untyped",
[info]                     "kind": "NameEx",
[info]                     "name": "x"
[info]                   },
[info]                   {
[info]                     "type": "Untyped",
[info]                     "kind": "ValEx",
[info]                     "value": {
[info]                       "kind": "TlaInt",
[info]                       "value": 2
[info]                     }
[info]                   }
[info]                 ]
[info]               }
[info]             ]
[info]           }
[info]         },
[info]         {
[info]           "type": "Untyped",
[info]           "kind": "TlaOperDecl",
[info]           "name": "InvariantViolation",
[info]           "formalParams": [
[info]             ]
[info]           ],
[info]       ..." -> "...  "formalParams": [
[info] [
[info]           ],
[info]           "isRecursive": false,
[info]           "body": {
[info]             "type": "Untyped",
[info]             "kind": "ValEx",
[info]             "value": {
[info]               "kind": "TlaBool",
[info]               "value": true
[info]             }
[info]           }
[info]         },
[info]         {
[info]           "type": "Untyped",
[info]           "kind": "TlaOperDecl",
[info]           "name": "State0",
[info]           "formalParams": [
[info] 
[info]           ],
[info]           "isRecursive": false,
[info]           "body": {
[info]             "type": "Untyped",
[info]             "kind": "OperEx",
[info]             "oper": "AND",
[info]             "args": [
[info]               {
[info]                 "type": "Untyped",
[info]                 "kind": "OperEx",
[info]                 "oper": "EQ",
[info]                 "args": [
[info]                   {
[info]                     "type": "Untyped",
[info]                     "kind": "NameEx",
[info]                     "name": "x"
[info]                   },
[info]                   {
[info]                     "type": "Untyped",
[info]                     "kind": "ValEx",
[info]                     "value": {
[info]                       "kind": "TlaInt",
[info]                       "value": 2
[info]                     }
[info]                   }
[info]                 ]
[info]               }
[info]             ]
[info]           }
[info]         },
[info]         {
[info]           "type": "Untyped",
[info]           "kind": "TlaOperDecl",
[info]           "name": "InvariantViolation",
[info]           "formalParams": [
[info] ]
[info]           ],
[info]       ..."

These errors look to me to be white space differences, due to the tests relying on hardcoded formatted JSON comparisons 😭

We talk tomorrow whether this superficial cleanup is worth the slowdown for the moment (also I guess risking breaking some quirk of the coutnerexamples?).

shonfeder · 2022-10-05T04:30:32Z

I've dropped the refactoring commits, and will merge this as is to unblock server-mode work. I've created a separate WIP branch to track to the refactoring to move the Counterexample class: #2194

Co-authored-by: Igor Konnov <igor@informal.systems>

Shon Feder added 10 commits September 26, 2022 13:35

Return error data in PassResult

df7c112

Include counterexamples in Checker.Error

869ef48

Fix comment typos

a4b00b2

Gather failure data from pass executions

840845c

Fix tests

0a50eb6

Unsure what to do about this fromRoot method

306fbf8

Fix Shai tests

f9a7671

One more unit test fix

0136f6e

Fix scala doc

cf41274

Self-review cleanup

fee1e08

Shon Feder added 2 commits September 30, 2022 12:21

Fix support for multi module JSON loading

1bde649

Fix comment

76fef1f

shonfeder changed the title ~~WIP: Return failure data from pass chain executions~~ Return failure data from pass chain executions Sep 30, 2022

shonfeder marked this pull request as ready for review September 30, 2022 16:32

shonfeder requested review from rodrigo7491, Kukovec and konnov as code owners September 30, 2022 16:32

Shon Feder added 2 commits September 30, 2022 12:39

Fix scala doc

df6eb13

Cannot link to a type alias I guess

Add changelog entry

b58a6b0

shonfeder mentioned this pull request Oct 3, 2022

Shai: Support returning structured verification data in RPC responses #2170

Closed

5 tasks

shonfeder requested a review from thpani October 3, 2022 13:36

konnov approved these changes Oct 4, 2022

View reviewed changes

shonfeder commented Oct 4, 2022

View reviewed changes

Update tla-io/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala

6a43f7f

Co-authored-by: Igor Konnov <igor@informal.systems>

shonfeder enabled auto-merge (squash) October 5, 2022 03:07

shonfeder mentioned this pull request Oct 5, 2022

Shai: Add ping RPC to services #2193

Merged

shonfeder force-pushed the 2181/passchain-output branch from aaa793d to 6a43f7f Compare October 5, 2022 04:28

shonfeder merged commit fb972ee into main Oct 5, 2022

shonfeder deleted the 2181/passchain-output branch October 5, 2022 13:34

This was referenced Oct 5, 2022

2181/followup refactor #2194

Closed

Shai: Return proper data from parse errors #2199

Closed

apalache-bot mentioned this pull request Oct 10, 2022

[release] 0.29.3 #2200

Closed

Kukovec pushed a commit that referenced this pull request Oct 20, 2022

Return failure data from pass chain executions (#2186)

d89dbbd

Co-authored-by: Igor Konnov <igor@informal.systems>

This was referenced Oct 24, 2022

[release] 0.29.3 #2248

Closed

[release] 0.30.0 #2250

Closed

apalache-bot mentioned this pull request Oct 31, 2022

[release] 0.30.0 #2263

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Return failure data from pass chain executions #2186

Return failure data from pass chain executions #2186

shonfeder commented Sep 28, 2022 •

edited

Loading

codecov-commenter commented Sep 30, 2022 •

edited

Loading

konnov left a comment

konnov Oct 4, 2022

shonfeder Oct 4, 2022

shonfeder left a comment

shonfeder Oct 4, 2022

shonfeder commented Oct 5, 2022

shonfeder commented Oct 5, 2022 •

edited

Loading

shonfeder commented Oct 5, 2022

Return failure data from pass chain executions #2186

Return failure data from pass chain executions #2186

Conversation

shonfeder commented Sep 28, 2022 • edited Loading

codecov-commenter commented Sep 30, 2022 • edited Loading

Codecov Report

konnov left a comment

Choose a reason for hiding this comment

konnov Oct 4, 2022

Choose a reason for hiding this comment

shonfeder Oct 4, 2022

Choose a reason for hiding this comment

shonfeder left a comment

Choose a reason for hiding this comment

shonfeder Oct 4, 2022

Choose a reason for hiding this comment

shonfeder commented Oct 5, 2022

shonfeder commented Oct 5, 2022 • edited Loading

shonfeder commented Oct 5, 2022

shonfeder commented Sep 28, 2022 •

edited

Loading

codecov-commenter commented Sep 30, 2022 •

edited

Loading

shonfeder commented Oct 5, 2022 •

edited

Loading