Fix a few bugs with lark parser for CBMC

Author: lou1306

sliver/backends/cbmc.py

@@ -97,26 +97,21 @@ class State:
 class CbmcCexTransformer(BaseTransformer):
     def state(self, n):
         header, lhs, rhs, *_ = n
-        state_id, file, function, line, _ = header.children
+        state_id, file, function, line, *_ = header.children
         return State(state_id, file, function, line, lhs, rhs)
 
 
 def translateCPROVER54(cex, info):
     with resources.path("sliver.grammars", "cbmc_cex.lark") as grammar_path:
         with open(grammar_path) as grammar:
-            lark_parser = Lark(grammar,
-                               parser='lalr',
-                               start='start54',
-                               transformer=CbmcCexTransformer())
+            lark_parser = Lark(grammar, parser='lalr', start='start54')
     yield from translateCPROVER(cex, info, parser=lark_parser)
 
 
 def translateCPROVERNEW(cex, info):
     with resources.path("sliver.grammars", "cbmc_cex.lark") as grammar_path:
         with open(grammar_path) as grammar:
-            lark_parser = Lark(grammar,
-                               parser='lalr',
-                               transformer=CbmcCexTransformer())
+            lark_parser = Lark(grammar, parser='lalr')
     yield from translateCPROVER(cex, info, parser=lark_parser)
 
 
@@ -147,7 +142,10 @@ def fmt(match, store_name, tid):
 
     cex_start_pos = cex.find("Counterexample:") + 15
     cex_end_pos = cex.rfind("Violated property:")
-    states = parser.parse(cex[cex_start_pos:cex_end_pos]).children
+    tree = parser.parse(cex[cex_start_pos:cex_end_pos])
+    transformer = CbmcCexTransformer()
+    tree = transformer.transform(tree)
+    states = tree.children
 
     inits = [
         (s.lhs, s.rhs) for s in states

sliver/backends/common.py

@@ -50,14 +50,12 @@ def false(self, _):
         return False
 
     def SIGNED_NUMBER(self, n):
+        n = "".join(n)
         try:
             return int(n)
         except Exception:
             return float(n)
 
-    def NAME(self, n):
-        return str(n)
-
 
 class Backend:
     """Base class representing a generic analysis backend."""

sliver/grammars/cbmc_cex.lark

@@ -14,22 +14,18 @@ _SEP: "----------------------------------------------------"
 
 ?rhs    : "TRUE"  -> true
         | "FALSE"  -> false
-        | SIGNED_NUMBER ["u"]
+        | SIGNED_NUMBER [ "ul" | "u" | "l" ]
         | "{" rhs ("," rhs)* "}"
 
-integer : INT
+integer : INT 
 _name : NAME
 
-_rhs_bits    : BITS
+_rhs_bits   : BITS
             | "{" _rhs_bits ("," _rhs_bits)* "}"
 
-header : \
-    "State" integer "file" _name "function" _name \
-    "line" integer "thread" integer
+header : "State" integer "file" _name "function" _name "line" integer "thread" integer
 
-header_54 : \
-    "State" integer "file" _name "line" integer \
-    "function" _name "thread" integer
+header_54 : "State" integer "file" _name "line" integer "function" _name "thread" integer
 
 _asgn : _name "=" rhs "(" _rhs_bits ")"
 state : header _SEP _asgn