ARM:AST: astprov conversion for result types

Author: sipma

chb/arm/opcodes/ARMAdd.py

@@ -237,6 +237,11 @@ 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())
+
         xd = ARMAddXData(xdata)
         if not xdata.is_ok:
             chklogger.logger.error("Error value encountered at %s", iaddr)
@@ -252,16 +257,10 @@ def ast_prov(
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
 
-        if rhs3.is_string_reference:
-            ctype = astree.astree.mk_pointer_type(astree.astree.char_type)
-            hl_lhs = XU.xvariable_to_ast_lvals(
-                lhs,
-                xdata,
-                astree,
-                ispointer=True,
-                ctype=ctype)[0]
-        else:
-            hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
+        hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
+
+        def hl_rhs_default () -> AST.ASTExpr:
+            return XU.xxpr_to_ast_def_expr(rhs3, xdata, iaddr, astree)
 
         if str(lhs) == "PC":
             chklogger.logger.info(
@@ -276,11 +275,11 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
             hl_rhs2_type = hl_rhs2.ctype(astree.ctyper)
 
             if hl_rhs1_type is None and hl_rhs2_type is None:
-                chklogger.logger.error(
+                chklogger.logger.info(
                     "Unable to lift pointer arithmetic without type for "
                     + "%s at address %s",
                     str(rhs3), iaddr)
-                return astree.mk_temp_lval_expression()
+                return hl_rhs_default()
 
             if hl_rhs2_type is not None and hl_rhs2_type.is_pointer:
                 rhs2tgttyp = cast(AST.ASTTypPtr, hl_rhs2_type).tgttyp
@@ -290,7 +289,6 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
                         "Unable to lift pointer arithmetic without size for "
                         + "%s at address %s; set type size to 1",
                         str(hl_rhs2_type), iaddr)
-                    # return astree.mk_temp_lval_expression()
                     tgttypsize = 1
 
                 if tgttypsize == 1:
@@ -311,11 +309,11 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
                 rhs1tgttyp = cast(AST.ASTTypPtr, hl_rhs1_type).tgttyp
                 tgttypsize = astree.type_size_in_bytes(rhs1tgttyp)
                 if tgttypsize is None:
-                    chklogger.logger.error(
+                    chklogger.logger.info(
                         "Unable to lift pointer arithmetic without size for "
                         + "%s at address %s",
                         str(hl_rhs1_type), iaddr)
-                    return astree.mk_temp_lval_expression()
+                    return hl_rhs_default()
 
                 if hl_rhs1.is_ast_startof:
                     arraylval = cast(AST.ASTStartOf, hl_rhs1).lval
@@ -345,13 +343,13 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
                 return astree.mk_binary_op("plus", hl_rhs1, scaled)
 
             if hl_rhs2_type is None:
-                chklogger.logger.error(
+                chklogger.logger.info(
                     "Unable to lift pointer arithmetic without type for "
                     + "%s at address %s",
                     str(rhs2), iaddr)
-                return astree.mk_temp_lval_expression()
+                return hl_rhs_default()
 
-            chklogger.logger.error(
+            chklogger.logger.info(
                 "Second operand pointer variable not yet supported for %s at "
                 + "address %s; rrhs1: %s; hl_rhs1: %s; hl_rhs2: %s; hl_rhs1_type: %s;"
                 + " hl_rhs2_type: %s",
@@ -362,8 +360,7 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
                 str(hl_rhs2),
                 str(hl_rhs1_type),
                 str(hl_rhs2_type))
-            return astree.mk_temp_lval_expression()
-
+            return hl_rhs_default()
 
         # resulting expression is a stack address
         if (
@@ -408,7 +405,7 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
                 if rhs3.is_constant_expression:
                     astree.set_ssa_value(str(hl_lhs), hl_rhs)
         else:
-            hl_rhs = XU.xxpr_to_ast_def_expr(rhs3, xdata, iaddr, astree)
+            hl_rhs = hl_rhs_default ()
 
         hl_assign = astree.mk_assign(
             hl_lhs,

chb/arm/opcodes/ARMBitFieldInsert.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021-2024  Aarno Labs LLC
+# Copyright (c) 2021-2025  Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -30,7 +30,7 @@
 from chb.app.InstrXData import InstrXData
 
 from chb.arm.ARMDictionaryRecord import armregistry
-from chb.arm.ARMOpcode import ARMOpcode, simplify_result
+from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
 from chb.arm.ARMOperand import ARMOperand
 
 import chb.arm.ARMPseudoCode as APC
@@ -46,6 +46,27 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XXpr
+
+
+class ARMBitFieldInsertXData(ARMOpcodeXData):
+    """BFI <rd> <rn>"""
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def vrd(self) -> "XVariable":
+        return self.var(0, "vrd")
+
+    @property
+    def xrd(self) -> "XXpr":
+        return self.xpr(0, "xrd")
+
+    @property
+    def xrn(self) -> "XXpr":
+        return self.xpr(1, "xrn")
 
 
 @armregistry.register_tag("BFI", ARMOpcode)
@@ -102,26 +123,30 @@ def width(self) -> int:
         return self.args[2]
 
     def annotation(self, xdata: InstrXData) -> str:
-        lhs = str(xdata.vars[0])
-        rhs1 = str(xdata.xprs[0])
-        rhs2 = str(xdata.xprs[1])
-        assignment = (
-            lhs
-            + " := bit-field-insert("
-            + rhs1
-            + ", "
-            + rhs2
-            + ", lsb:"
-            + str(self.lsb)
-            + ", width:"
-            + str(self.width))
-        if xdata.has_unknown_instruction_condition():
-            return "if ? then " + assignment
-        elif xdata.has_instruction_condition():
-            c = str(xdata.xprs[1])
-            return "if " + c + " then " + assignment
+        xd = ARMBitFieldInsertXData(xdata)
+        if xd.is_ok:
+            lhs = str(xd.vrd)
+            rhs1 = str(xd.xrd)
+            rhs2 = str(xd.xrn)
+            assignment = (
+                lhs
+                + " := bit-field-insert("
+                + rhs1
+                + ", "
+                + rhs2
+                + ", lsb:"
+                + str(self.lsb)
+                + ", width:"
+                + str(self.width))
+            if xdata.has_unknown_instruction_condition():
+                return "if ? then " + assignment
+            elif xdata.has_instruction_condition():
+                c = str(xdata.xprs[1])
+                return "if " + c + " then " + assignment
+            else:
+                return assignment
         else:
-            return assignment
+            return "Error value"
 
     def ast_prov(
             self,

chb/arm/opcodes/ARMByteReverseWord.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021-2023  Aarno Labs LLC
+# Copyright (c) 2021-2025  Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -30,7 +30,7 @@
 from chb.app.InstrXData import InstrXData
 
 from chb.arm.ARMDictionaryRecord import armregistry
-from chb.arm.ARMOpcode import ARMOpcode, simplify_result
+from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
 from chb.arm.ARMOperand import ARMOperand
 
 import chb.ast.ASTNode as AST
@@ -44,6 +44,28 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XXpr
+
+
+class ARMByteReverseWordXData(ARMOpcodeXData):
+    """REV <rd> <rn>"""
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def vrd(self) -> "XVariable":
+        return self.var(0, "vrd")
+
+    @property
+    def xrn(self) -> "XXpr":
+        return self.xpr(0, "xrn")
+
+    @property
+    def xxrn(self) -> "XXpr":
+        return self.xpr(1, "xxrn")
+
 
 
 @armregistry.register_tag("REV", ARMOpcode)
@@ -89,16 +111,14 @@ def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args[:-1]]
 
     def annotation(self, xdata: InstrXData) -> str:
-        lhs = str(xdata.vars[0])
-        rhs = str(xdata.xprs[1])
-        assignment = lhs + " := __rev(" + str(rhs) + ") intrinsic"
-        if xdata.has_unknown_instruction_condition():
-            return "if ? then " + assignment
-        elif xdata.has_instruction_condition():
-            c = str(xdata.xprs[1])
-            return "if " + c + " then " + assignment
-        else:
+        xd = ARMByteReverseWordXData(xdata)
+        if xd.is_ok:
+            lhs = str(xd.vrd)
+            rhs = str(xd.xxrn)
+            assignment = lhs + " := __rev(" + str(rhs) + ") intrinsic"
             return assignment
+        else:
+            return "Error value"
 
     # --------------------------------------------------------------------------
     # Operation

chb/arm/opcodes/ARMCountLeadingZeros.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021-2022 Aarno Labs LLC
+# Copyright (c) 2021-2025 Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -30,7 +30,7 @@
 from chb.app.InstrXData import InstrXData
 
 from chb.arm.ARMDictionaryRecord import armregistry
-from chb.arm.ARMOpcode import ARMOpcode, simplify_result
+from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
 from chb.arm.ARMOperand import ARMOperand
 
 import chb.ast.ASTNode as AST
@@ -44,6 +44,28 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XXpr
+
+
+class ARMCountLeadingZerosXData(ARMOpcodeXData):
+    """CLZ <rd> <rn>"""
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def vrd(self) -> "XVariable":
+        return self.var(0, "vrd")
+
+    @property
+    def xrn(self) -> "XXpr":
+        return self.xpr(0, "xrn")
+
+    @property
+    def xxrn(self) -> "XXpr":
+        return self.xpr(1, "xxrn")
+
 
 
 @armregistry.register_tag("CLZ", ARMOpcode)
@@ -82,16 +104,14 @@ def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args]
 
     def annotation(self, xdata: InstrXData) -> str:
-        lhs = str(xdata.vars[0])
-        rhs = str(xdata.xprs[1])
-        assignment = lhs + " := __clz(" + rhs + ") (intrinsic)"
-        if xdata.has_unknown_instruction_condition():
-            return "if ? then " + assignment
-        elif xdata.has_instruction_condition():
-            c = str(xdata.xprs[1])
-            return "if " + c + " then " + assignment
-        else:
+        xd = ARMCountLeadingZerosXData(xdata)
+        if xd.is_ok:
+            lhs = str(xd.vrd)
+            rhs = str(xd.xxrn)
+            assignment = lhs + " := __clz(" + rhs + ") (intrinsic)"
             return assignment
+        else:
+            return "Error value"
 
     def ast_prov(
             self,

chb/arm/opcodes/ARMLoadRegisterByte.py

@@ -233,12 +233,6 @@ def ast_prov(
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
 
-        '''
-        hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
-        hl_rhs = XU.xxpr_to_ast_def_expr(
-            rhs, xdata, iaddr, astree, size=1, memaddr=xaddr)
-        '''
-
         hl_assign = astree.mk_assign(
             hl_lhs,
             hl_rhs,
@@ -269,8 +263,8 @@ def ast_prov(
                 annotations=annotations)
             ll_assigns: List[AST.ASTInstruction] = [ll_assign, ll_addr_assign]
 
-            basereg = xdata.vars[1]
-            newaddr = xdata.xprs[4]
+            basereg = xd.get_base_update_var()
+            newaddr = xd.get_base_update_xpr()
             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)