Increase depth and emit a trace when pruning vacuous branches in `Pro…

…xy.hs` (#3974) Fixes #3973
runtimeverification · Jul 12, 2024 · 95d7d59 · 95d7d59
1 parent 561a538
commit 95d7d59
Show file tree

Hide file tree

Showing 3 changed files with 185 additions and 46 deletions.
diff --git a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json
@@ -58,13 +58,69 @@
                                                             ]
                                                         },
                                                         {
-                                                            "tag": "EVar",
-                                                            "name": "VarCONTINUATION",
-                                                            "sort": {
-                                                                "tag": "SortApp",
-                                                                "name": "SortK",
-                                                                "args": []
-                                                            }
+                                                            "tag": "App",
+                                                            "name": "kseq",
+                                                            "sorts": [],
+                                                            "args": [
+                                                                {
+                                                                    "tag": "App",
+                                                                    "name": "inj",
+                                                                    "sorts": [
+                                                                        {
+                                                                            "tag": "SortApp",
+                                                                            "name": "SortInternalOp",
+                                                                            "args": []
+                                                                        },
+                                                                        {
+                                                                            "tag": "SortApp",
+                                                                            "name": "SortKItem",
+                                                                            "args": []
+                                                                        }
+                                                                    ],
+                                                                    "args": [
+                                                                        {
+                                                                            "tag": "App",
+                                                                            "name": "Lbl'Hash'pc'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode",
+                                                                            "sorts": [],
+                                                                            "args": [
+                                                                                {
+                                                                                    "tag": "App",
+                                                                                    "name": "inj",
+                                                                                    "sorts": [
+                                                                                        {
+                                                                                            "tag": "SortApp",
+                                                                                            "name": "SortBinStackOp",
+                                                                                            "args": []
+                                                                                        },
+                                                                                        {
+                                                                                            "tag": "SortApp",
+                                                                                            "name": "SortOpCode",
+                                                                                            "args": []
+                                                                                        }
+                                                                                    ],
+                                                                                    "args": [
+                                                                                        {
+                                                                                            "tag": "App",
+                                                                                            "name": "LblJUMPI'Unds'EVM'Unds'BinStackOp",
+                                                                                            "sorts": [],
+                                                                                            "args": []
+                                                                                        }
+                                                                                    ]
+                                                                                }
+                                                                            ]
+                                                                        }
+                                                                    ]
+                                                                },
+                                                                {
+                                                                    "tag": "EVar",
+                                                                    "name": "VarCONTINUATION",
+                                                                    "sort": {
+                                                                        "tag": "SortApp",
+                                                                        "name": "SortK",
+                                                                        "args": []
+                                                                    }
+                                                                }
+                                                            ]
                                                         }
                                                     ]
                                                 }
@@ -8757,18 +8813,18 @@
             },
             {
                 "tag": "rewrite",
-                "origin": "booster",
+                "origin": "proxy",
                 "result": {
                     "tag": "success",
-                    "rule-id": "20bc9774d59030dcada92e997351315ed198a464546f5b36d67578cfd12938d1"
+                    "rule-id": "0ee7a2c1d6ff36a91ac9e9ed19a2c624ba21b97f4511af22044f6169bb8adfa1"
                 }
             },
             {
                 "tag": "rewrite",
                 "origin": "booster",
                 "result": {
                     "tag": "success",
-                    "rule-id": "d40db55be13c107a708382df2ae9cea0d6305bbf5d6804de46250d7076a392e2"
+                    "rule-id": "20bc9774d59030dcada92e997351315ed198a464546f5b36d67578cfd12938d1"
                 }
             }
         ]

diff --git a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json
@@ -58,13 +58,69 @@
                                                             ]
                                                         },
                                                         {
-                                                            "tag": "EVar",
-                                                            "name": "VarCONTINUATION",
-                                                            "sort": {
-                                                                "tag": "SortApp",
-                                                                "name": "SortK",
-                                                                "args": []
-                                                            }
+                                                            "tag": "App",
+                                                            "name": "kseq",
+                                                            "sorts": [],
+                                                            "args": [
+                                                                {
+                                                                    "tag": "App",
+                                                                    "name": "inj",
+                                                                    "sorts": [
+                                                                        {
+                                                                            "tag": "SortApp",
+                                                                            "name": "SortInternalOp",
+                                                                            "args": []
+                                                                        },
+                                                                        {
+                                                                            "tag": "SortApp",
+                                                                            "name": "SortKItem",
+                                                                            "args": []
+                                                                        }
+                                                                    ],
+                                                                    "args": [
+                                                                        {
+                                                                            "tag": "App",
+                                                                            "name": "Lbl'Hash'pc'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode",
+                                                                            "sorts": [],
+                                                                            "args": [
+                                                                                {
+                                                                                    "tag": "App",
+                                                                                    "name": "inj",
+                                                                                    "sorts": [
+                                                                                        {
+                                                                                            "tag": "SortApp",
+                                                                                            "name": "SortBinStackOp",
+                                                                                            "args": []
+                                                                                        },
+                                                                                        {
+                                                                                            "tag": "SortApp",
+                                                                                            "name": "SortOpCode",
+                                                                                            "args": []
+                                                                                        }
+                                                                                    ],
+                                                                                    "args": [
+                                                                                        {
+                                                                                            "tag": "App",
+                                                                                            "name": "LblJUMPI'Unds'EVM'Unds'BinStackOp",
+                                                                                            "sorts": [],
+                                                                                            "args": []
+                                                                                        }
+                                                                                    ]
+                                                                                }
+                                                                            ]
+                                                                        }
+                                                                    ]
+                                                                },
+                                                                {
+                                                                    "tag": "EVar",
+                                                                    "name": "VarCONTINUATION",
+                                                                    "sort": {
+                                                                        "tag": "SortApp",
+                                                                        "name": "SortK",
+                                                                        "args": []
+                                                                    }
+                                                                }
+                                                            ]
                                                         }
                                                     ]
                                                 }
@@ -8749,18 +8805,18 @@
         "logs": [
             {
                 "tag": "rewrite",
-                "origin": "booster",
+                "origin": "proxy",
                 "result": {
                     "tag": "success",
-                    "rule-id": "20bc9774d59030dcada92e997351315ed198a464546f5b36d67578cfd12938d1"
+                    "rule-id": "0ee7a2c1d6ff36a91ac9e9ed19a2c624ba21b97f4511af22044f6169bb8adfa1"
                 }
             },
             {
                 "tag": "rewrite",
                 "origin": "booster",
                 "result": {
                     "tag": "success",
-                    "rule-id": "d40db55be13c107a708382df2ae9cea0d6305bbf5d6804de46250d7076a392e2"
+                    "rule-id": "20bc9774d59030dcada92e997351315ed198a464546f5b36d67578cfd12938d1"
                 }
             }
         ]