XPR: add checks for loopcounter; extend ssa-value recording

Author: sipma

chb/invariants/XSymbol.py

@@ -63,6 +63,9 @@ def name(self) -> str:
     def attrs(self) -> List[str]:
         return self.tags[1:]
 
+    def has_attribute(self, attr: str) -> bool:
+        return attr in self.attrs
+
     @property
     def seqnr(self) -> int:
         return self.args[0]

chb/invariants/XVariable.py

@@ -82,6 +82,10 @@ def type(self) -> str:
     def is_tmp(self) -> bool:
         return (self.seqnr == -1)
 
+    @property
+    def is_loop_counter(self) -> bool:
+        return self.symbol.has_attribute("lc")
+
     @property
     def is_constant_value_variable(self) -> bool:
         return self.has_denotation() and self.denotation.is_auxiliary_variable

chb/invariants/XXpr.py

@@ -294,6 +294,14 @@ def has_variables_with_property(
             self, p: Callable[[XVariable], bool]) -> bool:
         return False
 
+    def all_variables_with_property(
+            self, p: Callable[[XVariable], bool]) -> bool:
+        return False
+
+    @property
+    def is_loop_counter_expression(self) -> bool:
+        return self.all_variables_with_property(lambda v: v.is_loop_counter)
+
     def negated_value(self) -> int:
         raise UF.CHBError("Get_negated_value not supported for " + str(self))
 
@@ -349,6 +357,10 @@ def __init__(
     def variable(self) -> XVariable:
         return self.xd.variable(self.args[0])
 
+    @property
+    def is_loop_counter(self) -> bool:
+        return self.variable.is_loop_counter
+
     @property
     def is_constant_value_variable(self) -> bool:
         return self.variable.is_constant_value_variable
@@ -447,6 +459,10 @@ def has_variables_with_property(
             self, p: Callable[[XVariable], bool]) -> bool:
         return p(self.variable)
 
+    def all_variables_with_property(
+            self, p: Callable[[XVariable], bool]) -> bool:
+        return p(self.variable)
+
     def argument_index(self) -> int:
         if self.is_argument_value:
             return self.variable.denotation.argument_index()
@@ -577,6 +593,10 @@ def intvalue(self) -> int:
             raise UF.CHBError(
                 "Constant is not an integer constant: " + str(self))
 
+    def all_variables_with_property(
+            self, p: Callable[[XVariable], bool]) -> bool:
+        return True
+
     @property
     def is_constant(self) -> bool:
         return True
@@ -759,6 +779,10 @@ def has_variables_with_property(
             self, p: Callable[[XVariable], bool]) -> bool:
         return any([op.has_variables_with_property(p) for op in self.operands])
 
+    def all_variables_with_property(
+            self, p: Callable[[XVariable], bool]) -> bool:
+        return all([op.all_variables_with_property(p) for op in self.operands])
+
     @property
     def is_stack_address(self) -> bool:
         args = self.operands

chb/invariants/XXprUtil.py

@@ -1848,12 +1848,26 @@ def xvariable_to_ast_lval(
             bctype = xdata.function.register_lhs_type(iaddr, str(xv))
             if bctype is not None:
                 ctype = bctype.convert(astree.typconverter)
+
+        # Note: Ideally the rhs parameter should be replaced with an astrhs
+        # parameter supplied by all of the instructions. The replacement would
+        # avoid having to compute the astrhs twice. Furthermore, for some
+        # instructions the rhs may be computed in a non-standard way, causing
+        # the assigned value to diverge from the value computed here.
         if (
                 rhs is not None
                 and (rhs.is_constant
-                     or (rhs.is_constant_value_variable))):
+                     or (rhs.is_constant_value_variable)
+                     or (rhs.is_loop_counter_expression))):
             astrhs: Optional[AST.ASTExpr] = xxpr_to_ast_def_expr(
                 rhs, xdata, iaddr, astree, anonymous=anonymous)
+
+        elif rhs is not None:
+            astrhs = xxpr_to_ast_def_expr(
+                rhs, xdata, iaddr, astree, anonymous=anonymous)
+            if not astrhs.is_constant_value_expression:
+                astrhs = None
+
         else:
             astrhs = None