ARM: support for predicate/ternary assignment

Author: sipma

chb/arm/opcodes/ARMMove.py

@@ -61,6 +61,33 @@ class ARMMoveXData(ARMOpcodeXData):
 
     - c expressions:
     0: cresult
+
+    Aggregates:
+
+    - expressions with predicate / ternary assignments
+
+    - nondet:
+      - predicate: none
+      - ternary:
+        0: true assign (constant)
+        1: false assign  (constant)
+
+    - predicate:
+      0: p
+      1: xp
+
+    - ternary:
+      0: p
+      1: xp
+      2: true assign  (constant)
+      3: false assign  (constant)
+
+    - c expressions with predicate /ternary assignments
+
+    - nondet: none
+
+    - predicate/ternary:
+      0: p
     """
 
     def __init__(self, xdata: InstrXData) -> None:
@@ -70,6 +97,22 @@ def __init__(self, xdata: InstrXData) -> None:
     def vrd(self) -> "XVariable":
         return self.var(0, "vrd")
 
+    @property
+    def is_predicate_assign(self) -> bool:
+        return self.xdata.is_predicate_assignment
+
+    @property
+    def is_nondet_predicate_assign(self) -> bool:
+        return self.xdata.is_nondet_predicate_assignment
+
+    @property
+    def is_ternary_assign(self) -> bool:
+        return self.xdata.is_ternary_assignment
+
+    @property
+    def is_nondet_ternary_assign(self) -> bool:
+        return self.xdata.is_nondet_ternary_assignment
+
     @property
     def xrm(self) -> "XXpr":
         return self.xpr(0, "xrm")
@@ -90,6 +133,37 @@ def cresult(self) -> "XXpr":
     def is_cresult_ok(self) -> bool:
         return self.is_cxpr_ok(0)
 
+    @property
+    def predicate(self) -> "XXpr":
+        # known to be valid
+        return self.xpr(0, "p")  # known to be valid
+
+    @property
+    def xpredicate(self) -> "XXpr":
+        return self.xpr(1, "xp")  # known to be valid
+
+    @property
+    def cpredicate(self) -> "XXpr":
+        return self.cxpr(0, "cxp")
+
+    @property
+    def is_cpredicate_ok(self) -> bool:
+        return self.is_cxpr_ok(0)
+
+    @property
+    def tern_assign_true(self) -> "XXpr":  # known to be valid
+        if self.is_nondet_ternary_assign:
+            return self.xpr(1, "xp1")
+        else:
+            return self.xpr(3, "xp1")
+
+    @property
+    def tern_assign_false(self) -> "XXpr":  # known to be valid
+        if self.is_nondet_ternary_assign:
+            return self.xpr(0, "xp2")
+        else:
+            return self.xpr(2, "xp2")
+
     def has_instruction_condition(self) -> bool:
         return self.xdata.has_instruction_condition()
 
@@ -102,10 +176,37 @@ def has_valid_instruction_c_condition(self) -> bool:
     def get_instruction_c_condition(self) -> "XXpr":
         return self.xdata.get_instruction_c_condition()
 
+    def predicate_assignment_ann(self) -> str:
+        if self.is_nondet_predicate_assign:
+            rhs = "? (unknown predicate)"
+        else:
+            crhs = (
+                " (C:"
+                + (str(self.cpredicate) if self.is_cpredicate_ok else "?")
+                + ")")
+            rhs = str(self.xpredicate) + crhs
+        return str(self.vrd) + " := " + rhs
+
+    def ternary_assignment_ann(self) -> str:
+        rhs = str(self.tern_assign_true) + " : " + str(self.tern_assign_false)
+        if self.is_nondet_ternary_assign:
+            rhs = " ? " + rhs
+        else:
+            rhs = str(self.xpredicate) + " ? " + rhs
+        cpred = (
+            " (C:"
+            + (str(self.cpredicate) if self.is_cpredicate_ok else "?")
+            + ")")
+        return str(self.vrd) + " := " + rhs + cpred
+
     @property
     def annotation(self) -> str:
         if self.xdata.instruction_is_subsumed():
             return "subsumed by " + self.xdata.subsumed_by()
+        if self.is_ternary_assign or self.is_nondet_ternary_assign:
+            return self.ternary_assignment_ann()
+        if self.is_predicate_assign or self.is_nondet_predicate_assign:
+            return self.predicate_assignment_ann()
         if self.xdata.instruction_subsumes():
             return "subsumes " + ", ".join(self.xdata.subsumes())
         cx = " (C: " + (str(self.cresult) if self.is_cresult_ok else "None") + ")"
@@ -209,6 +310,141 @@ def ast_prov_subsumed(
 
         return ([], [ll_assign])
 
+    def ast_prov_predicate_assign(
+            self,
+            astree: ASTInterface,
+            iaddr: str,
+            bytestring: str,
+            xdata: InstrXData
+    ) -> Tuple[List[AST.ASTInstruction], List[AST.ASTInstruction]]:
+
+        annotations: List[str] = [iaddr, "MOV (predicate assign)"]
+
+        # low-level assignment
+
+        (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree)
+        (ll_rhs, _, _) = self.opargs[1].ast_rvalue(astree)
+
+        ll_assign = astree.mk_assign(
+            ll_lhs,
+            ll_rhs,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        # high-level assignment
+
+        xd = ARMMoveXData(xdata)
+
+        if xd.is_nondet_predicate_assign:
+            chklogger.logger.warning(
+                "Predicate assignment without associated predicate at "
+                + "address %s", iaddr)
+            return ([], [ll_assign])
+
+        rhs = xd.cpredicate if xd.is_cpredicate_ok else xd.xpredicate
+        lhs = xd.vrd
+        rdefs = xdata.reachingdefs
+        defuses = xdata.defuses
+        defuseshigh = xdata.defuseshigh
+
+        hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs)
+        hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
+
+        hl_assign = astree.mk_assign(
+            hl_lhs,
+            hl_rhs,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        astree.add_instr_mapping(hl_assign, ll_assign)
+        astree.add_instr_address(hl_assign, [iaddr])
+        astree.add_expr_mapping(hl_rhs, ll_rhs)
+        astree.add_lval_mapping(hl_lhs, ll_lhs)
+        astree.add_expr_reachingdefs(hl_rhs, rdefs[1:])
+        astree.add_expr_reachingdefs(ll_rhs, [rdefs[0]])
+        astree.add_lval_defuses(hl_lhs, defuses[0])
+        astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
+
+        if astree.has_register_variable_intro(iaddr):
+            rvintro = astree.get_register_variable_intro(iaddr)
+            if rvintro.has_cast():
+                astree.add_expose_instruction(hl_assign.instrid)
+
+        return ([hl_assign], [ll_assign])
+
+
+    def ast_prov_ternary_assign(
+            self,
+            astree: ASTInterface,
+            iaddr: str,
+            bytestring: str,
+            xdata: InstrXData
+    ) -> Tuple[List[AST.ASTInstruction], List[AST.ASTInstruction]]:
+
+        annotations: List[str] = [iaddr, "MOV (ternary assign)"]
+
+        # low-level assignment
+
+        (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree)
+        (ll_rhs, _, _) = self.opargs[1].ast_rvalue(astree)
+
+        ll_assign = astree.mk_assign(
+            ll_lhs,
+            ll_rhs,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        # high-level assignment
+
+        xd = ARMMoveXData(xdata)
+
+        if xd.is_nondet_ternary_assign:
+            chklogger.logger.warning(
+                "Ternary assignment without associated predicate at address %s",
+                iaddr)
+            return ([], [ll_assign])
+
+        rhsp = xd.cpredicate if xd.is_cpredicate_ok else xd.xpredicate
+        rhs1 = xd.tern_assign_true
+        rhs2 = xd.tern_assign_false
+        lhs = xd.vrd
+        rdefs = xdata.reachingdefs
+        defuses = xdata.defuses
+        defuseshigh = xdata.defuseshigh
+
+        hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
+        hl_rhsp = XU.xxpr_to_ast_def_expr(rhsp, xdata, iaddr, astree)
+        hl_rhs1 = XU.xxpr_to_ast_def_expr(rhs1, xdata, iaddr, astree)
+        hl_rhs2 = XU.xxpr_to_ast_def_expr(rhs2, xdata, iaddr, astree)
+        hl_rhs = astree.mk_question(hl_rhsp, hl_rhs1, hl_rhs2)
+
+        hl_assign = astree.mk_assign(
+            hl_lhs,
+            hl_rhs,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        astree.add_instr_mapping(hl_assign, ll_assign)
+        astree.add_instr_address(hl_assign, [iaddr])
+        astree.add_expr_mapping(hl_rhs, ll_rhs)
+        astree.add_lval_mapping(hl_lhs, ll_lhs)
+        astree.add_expr_reachingdefs(hl_rhs, rdefs[1:])
+        astree.add_expr_reachingdefs(ll_rhs, [rdefs[0]])
+        astree.add_lval_defuses(hl_lhs, defuses[0])
+        astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
+
+        if astree.has_register_variable_intro(iaddr):
+            rvintro = astree.get_register_variable_intro(iaddr)
+            if rvintro.has_cast():
+                astree.add_expose_instruction(hl_assign.instrid)
+
+        return ([hl_assign], [ll_assign])
+
+
     def ast_prov(
             self,
             astree: ASTInterface,
@@ -232,10 +468,22 @@ def ast_prov(
         if xdata.instruction_is_subsumed():
             return self.ast_prov_subsumed(astree, iaddr, bytestring, xdata)
 
+        xd = ARMMoveXData(xdata)
+
         if xdata.instruction_subsumes():
-            chklogger.logger.warning(
-                "MOV instruction at %s is part of an aggregate that is not yet supported",
-                iaddr)
+            if xd.is_predicate_assign or xd.is_nondet_predicate_assign:
+                return self.ast_prov_predicate_assign(
+                    astree, iaddr, bytestring, xdata)
+
+            elif xd.is_ternary_assign or xd.is_nondet_ternary_assign:
+                return self.ast_prov_ternary_assign(
+                    astree, iaddr, bytestring, xdata)
+
+            else:
+                chklogger.logger.warning(
+                    "MOV instruction at %s is part of an aggregate that is "
+                    + "not yet supported",
+                    iaddr)
             return ([], [])
 
         # low-level assignment