AST: add prettyprinter support for baseptr array expr

Author: sipma

chb/ast/ASTCPrettyPrinter.py

@@ -495,8 +495,21 @@ def visit_variable(self, var: AST.ASTVariable) -> None:
 
     def visit_memref(self, memref: AST.ASTMemRef) -> None:
         if memref.memexp.is_ast_addressof:
-            memexp = cast(AST.ASTAddressOf, memref.memexp)
-            memexp.lval.accept(self)
+            memexpa = cast(AST.ASTAddressOf, memref.memexp)
+            memexpa.lval.accept(self)
+        elif memref.memexp.is_ast_binary_op:
+            memexpb = cast(AST.ASTBinaryOp, memref.memexp)
+            exp1 = memexpb.exp1
+            exp2 = memexpb.exp2
+            if exp1.is_ast_lval_expr:
+                exp1.accept(self)
+                self.ccode.write("[")
+                exp2.accept(self)
+                self.ccode.write("]")
+            else:
+                self.ccode.write("(*(")
+                memref.memexp.accept(self)
+                self.ccode.write("))")
         else:
             self.ccode.write("(*(")
             memref.memexp.accept(self)

chb/invariants/XXprUtil.py

@@ -468,13 +468,9 @@ def memory_variable_to_lval_expression(
             offset = cast("VMemoryOffsetBasePtrArrayIndexOffset", offset)
             (ptroffset, astoffset) = base_ptr_array_offset_to_ast_offset(
                 offset, xdata, iaddr, astree, anonymous=anonymous)
-            if ptroffset.is_integer_constant_zero:
-                return astree.mk_memref_expr(
-                    astlval, offset=astoffset, anonymous=anonymous)
-            else:
-                ptrexpr = astree.mk_binary_op("plus", ptroffset, astlval)
-                return astree.mk_memref_expr(
-                    ptrexpr, offset=astoffset, anonymous=anonymous)
+            ptrexpr = astree.mk_binary_op("plus", astlval, ptroffset)
+            return astree.mk_memref_expr(
+                ptrexpr, offset=astoffset, anonymous=anonymous)
 
     name = str(base)