ARM:LDRH: conversion for c expressions

Author: sipma

chb/arm/opcodes/ARMLoadRegisterHalfword.py

@@ -52,6 +52,21 @@
 
 
 class ARMLoadRegisterHalfwordXData(ARMOpcodeXData):
+    """Data format:
+    - variables:
+    0: vrt (lhs)
+
+    - expressions:
+    0: xrn
+    1: xrm
+    2: xmem (rhs)
+    3: xrmem (rhs, rewritten)
+    4: xaddr (address of rhs)
+
+    - c expressions:
+    0: cxrmem (rhs)
+    1: cxaddr (address of rhs)
+    """
 
     def __init__(self, xdata: InstrXData) -> None:
         ARMOpcodeXData.__init__(self, xdata)
@@ -61,36 +76,79 @@ def vrt(self) -> "XVariable":
         return self.var(0, "vrt")
 
     @property
-    def vmem(self) -> "XVariable":
-        return self.var(1, "vmem")
+    def xrn(self) -> "XXpr":
+        return self.xpr(0, "xrn")
+
+    @property
+    def xrm(self) -> "XXpr":
+        return self.xpr(1, "xrm")
 
     @property
     def xmem(self) -> "XXpr":
         return self.xpr(2, "xmem")
 
+    @property
+    def is_xmem_ok(self) -> bool:
+        return self.is_xpr_ok(2)
+
     @property
     def xrmem(self) -> "XXpr":
         return self.xpr(3, "xrmem")
 
+    @property
+    def is_xrmem_ok(self) -> bool:
+        return self.is_xpr_ok(3)
+
+    @property
+    def cxrmem(self) -> "XXpr":
+        return self.cxpr(0, "cxrmem")
+
+    @property
+    def is_cxrmem_ok(self) -> bool:
+        return self.is_cxpr_ok(0)
+
     @property
     def xaddr(self) -> "XXpr":
         return self.xpr(4, "xaddr")
 
     @property
-    def is_xrmem_unknown(self) -> bool:
-        return self.xdata.xprs_r[3] is None
+    def is_xaddr_ok(self) -> bool:
+        return self.is_xpr_ok(4)
+
+    @property
+    def xxaddr(self) -> "XXpr":
+        return self.xpr(5, "xxaddr")
+
+    @property
+    def is_xxaddr_ok(self) -> bool:
+        return self.is_xpr_ok(5)
+
+    @property
+    def cxaddr(self) -> "XXpr":
+        return self.cxpr(1, "cxaddr")
 
     @property
-    def is_address_known(self) -> bool:
-        return self.xdata.xprs_r[4] is not None
+    def is_cxaddr_ok(self) -> bool:
+        return self.is_cxpr_ok(1)
 
     @property
     def annotation(self) -> str:
         wbu = self.writeback_update()
-        if self.is_ok:
-            assignment = str(self.vrt) + " := " + str(self.xrmem)
-        elif self.is_xrmem_unknown and self.is_address_known:
-            assignment = str(self.vrt) + " := *(" + str(self.xaddr) + ")"
+        if self.is_cxrmem_ok:
+            crhs = str(self.cxrmem)
+        elif self.is_cxaddr_ok:
+            crhs = "*(" + str(self.cxaddr) + ")"
+        else:
+            crhs = "None"
+        cx = " (C: " + crhs + ")"
+        addr = str(self.xxaddr if self.is_xxaddr_ok else self.xaddr)
+        caddr = str(self.cxaddr if self.is_cxaddr_ok else "None")
+        caddr = " (addr: " + addr + "; C: " + caddr + ")"
+        if self.is_ok or self.is_xrmem_ok:
+            assignment = str(self.vrt) + " := " + str(self.xrmem) + cx + caddr
+        elif self.is_xaddr_ok:
+            assignment = (
+                str(self.vrt) + " := *(" + str(self.xaddr) + ")" + cx + caddr)
         else:
             assignment = "Error value"
         return self.add_instruction_condition(assignment) + wbu
@@ -109,27 +167,14 @@ class ARMLoadRegisterHalfword(ARMOpcode):
     args[3]: index of memory location in armdictionary
     args[4]: is-wide (thumb)
 
-    xdata format: a:vxxxxrrrdh
-    --------------------------
-    vars[0]: lhs
-    vars[1]: memory location expressed as a variable
-    xprs[0]: value in rn
-    xprs[1]: value in rm
-    xprs[2]: value in memory location
-    xprs[3]: value in memory location (simplified)
-    xprs[4]: address of memory location
+    xdata format:
+    -------------
     rdefs[0]: reaching definitions rn
     rdefs[1]: reaching definitions rm
     rdefs[2]: reaching definitions memory location
     rdefs[3..]: reaching definitions for memory value
     uses[0]: use of lhs
     useshigh[0]: use of lhs at high level
-
-    optional:
-    vars[1]: lhs base register (if base update)
-
-    xprs[.]: instruction condition (if has condition)
-    xprs[.]: new address for base register
     """
 
     def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
@@ -149,13 +194,20 @@ def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(self.args[i]) for i in [0, 1, 2, 3]]
 
     def lhs(self, xdata: InstrXData) -> List[XVariable]:
-        return [xdata.vars[0]]
+        xd = ARMLoadRegisterHalfwordXData(xdata)
+        return [xd.vrt]
 
     def is_load_instruction(self, xdata: InstrXData) -> bool:
         return True
 
     def rhs(self, xdata: InstrXData) -> List[XXpr]:
-        return [xdata.xprs[1]]
+        xd = ARMLoadRegisterHalfwordXData(xdata)
+        if xd.is_xrmem_ok:
+            return [xd.xrmem]
+        elif xd.is_xmem_ok:
+            return [xd.xmem]
+        else:
+            return []
 
     def annotation(self, xdata: InstrXData) -> str:
         return ARMLoadRegisterHalfwordXData(xdata).annotation
@@ -189,38 +241,63 @@ def ast_prov(
 
         # high-level assignment
 
+        def has_cast() -> bool:
+            return (
+                astree.has_register_variable_intro(iaddr)
+                and astree.get_register_variable_intro(iaddr).has_cast())
+
+        lhs = xd.vrt
+
         if xd.is_ok:
-            lhs = xd.vrt
-            rhs = xd.xrmem
-            xaddr = xd.xaddr
-            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, memaddr=xaddr, size=2)
+            rhs = xd.cxrmem
+            rhsval = None if has_cast() else xd.cxrmem
+            hl_lhs = XU.xvariable_to_ast_lval(
+                lhs, xdata, iaddr, astree, rhs=rhsval)
+            hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
+
+        elif xd.is_cxaddr_ok:
+            cxaddr = xd.cxaddr
+            hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
+            hl_rhs = XU.xmemory_dereference_lval_expr(
+                cxaddr, xdata, iaddr, astree)
 
-        elif xd.is_xrmem_unknown and xd.is_address_known:
+        elif xd.is_xaddr_ok:
             xaddr = xd.xaddr
-            lhs = xd.vrt
             hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
             hl_rhs = XU.xmemory_dereference_lval_expr(
-                xaddr, xdata, iaddr, astree, size=2)
+                xaddr, xdata, iaddr, astree)
+
+            chklogger.logger.warning(
+                "LDRH: Unable to use a C expression for rhs. Fall back to "
+                + "native byte-based address: %s to form rhs %s at address %s",
+                str(xaddr), str(hl_rhs), iaddr)
 
         else:
             chklogger.logger.error(
                 "LDRH: both memory value and address values are error values "
                 + "at address %s: ", iaddr)
-            return ([], [])
+            return ([], (ll_pre + [ll_assign] + ll_post))
+
 
         rdefs = xdata.reachingdefs
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
 
+        if has_cast():
+            lhstype = hl_lhs.ctype(astree.ctyper)
+            if lhstype is not None:
+                hl_rhs = astree.mk_cast_expr(lhstype, hl_rhs)
+
         hl_assign = astree.mk_assign(
             hl_lhs,
             hl_rhs,
             iaddr=iaddr,
             bytestring=bytestring,
             annotations=annotations)
 
+        if has_cast():
+            astree.add_expose_instruction(hl_assign.instrid)
+
         astree.add_instr_mapping(hl_assign, ll_assign)
         astree.add_instr_address(hl_assign, [iaddr])
         astree.add_expr_mapping(hl_rhs, ll_rhs)
@@ -245,7 +322,7 @@ def ast_prov(
             ll_assigns: List[AST.ASTInstruction] = [ll_assign, ll_addr_assign]
 
             basereg = xd.get_base_update_var()
-            newaddr = xd.get_base_update_xpr()
+            newaddr = xd.get_base_update_cxpr()
             hl_addr_lhs = XU.xvariable_to_ast_lval(basereg, xdata, iaddr, astree)
             hl_addr_rhs = XU.xxpr_to_ast_def_expr(newaddr, xdata, iaddr, astree)