ARM:AST: update ast_prov methods

sipma · sipma · commit 298b95135c6c · 2024-11-12T00:46:11.000-08:00
diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py
@@ -1 +1 @@
-chbversion: str = "0.3.0-20241028"
+chbversion: str = "0.3.0-20241111"
diff --git a/chb/arm/opcodes/ARMBitwiseExclusiveOr.py b/chb/arm/opcodes/ARMBitwiseExclusiveOr.py
@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021-2023  Aarno Labs LLC
+# Copyright (c) 2021-2024  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
@@ -118,12 +118,6 @@ def ast_prov(
 
         annotations: List[str] = [iaddr, "EOR"]
 
-        lhs = xdata.vars[0]
-        rhs = xdata.xprs[3]
-        rdefs = xdata.reachingdefs
-        defuses = xdata.defuses
-        defuseshigh = xdata.defuseshigh
-
         (ll_lhs, _, _) = self.operands[0].ast_lvalue(astree)
         (ll_op1, _, _) = self.operands[0].ast_rvalue(astree)
         (ll_op2, _, _) = self.operands[0].ast_rvalue(astree)
@@ -136,27 +130,20 @@ def ast_prov(
             bytestring=bytestring,
             annotations=annotations)
 
-        lhsasts = XU.xvariable_to_ast_lvals(lhs, xdata, astree)
-        if len(lhsasts) == 0:
-            raise UF.CHBError("BitwiseExclusiveOr (EOR): no lval found")
-
-        if len(lhsasts) > 1:
-            raise UF.CHBError(
-                "BitwiseExclusiveOr (EOR): multiple lvals found: "
-                + ", ".join(str(v) for v in lhsasts))
+        rdefs = xdata.reachingdefs
 
-        hl_lhs = lhsasts[0]
+        astree.add_expr_reachingdefs(ll_op1, [rdefs[0]])
+        astree.add_expr_reachingdefs(ll_op2, [rdefs[1]])
 
-        rhsasts = XU.xxpr_to_ast_def_exprs(rhs, xdata, iaddr, astree)
-        if len(rhsasts) == 0:
-            raise UF.CHBError("BitwiseExclusiveOr (EOR): no lval found")
+        # high-level assignment
 
-        if len(rhsasts) > 1:
-            raise UF.CHBError(
-                "BitwiseExclusiveOr (EOR): multiple rhs values found: "
-                + ", ".join(str(v) for v in rhsasts))
+        lhs = xdata.vars[0]
+        rhs = xdata.xprs[3]
+        defuses = xdata.defuses
+        defuseshigh = xdata.defuseshigh
 
-        hl_rhs = rhsasts[0]
+        hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
+        hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
 
         hl_assign = astree.mk_assign(
             hl_lhs,
@@ -165,13 +152,12 @@ def ast_prov(
             bytestring=bytestring,
             annotations=annotations)
 
-        astree.add_reg_definition(iaddr, hl_lhs, hl_rhs)
         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(ll_op1, [rdefs[0]])
-        astree.add_expr_reachingdefs(ll_op2, [rdefs[1]])
+        astree.add_expr_reachingdefs(hl_rhs, rdefs[2:])
+        astree.add_expr_reachingdefs(ll_rhs, rdefs[:2])
         astree.add_lval_defuses(hl_lhs, defuses[0])
         astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
 
diff --git a/chb/arm/opcodes/ARMCompareBranchZero.py b/chb/arm/opcodes/ARMCompareBranchZero.py
@@ -131,22 +131,7 @@ def ast_condition_prov(
             else:
                 condition = ftconds[1]
 
-            astconds = XU.xxpr_to_ast_def_exprs(condition, xdata, iaddr, astree)
-            if len(astconds) == 0:
-                chklogger.logger.error(
-                    "CompareBranchZero (CBZ) at address %s: no rhs values "
-                    + "found; returning zero", iaddr)
-                return (zero, zero)
-
-            if len(astconds) > 1:
-                chklogger.logger.error(
-                    "CompareBranchZero (CBZ) at address %s: multiple rhs "
-                    + "values found at address %s: %s; returning zero",
-                    iaddr,
-                    ", ".join(str(v) for v in astconds))
-                return (zero, zero)
-
-            hl_cond = astconds[0]
+            hl_cond = XU.xxpr_to_ast_def_expr(condition, xdata, iaddr, astree)
 
             astree.add_expr_mapping(hl_cond, ll_cond)
             astree.add_expr_reachingdefs(hl_cond, rdefs)
diff --git a/chb/arm/opcodes/ARMStoreRegisterByte.py b/chb/arm/opcodes/ARMStoreRegisterByte.py
@@ -150,12 +150,19 @@ def ast_prov(
 
         lhs = xdata.vars[0]
         rhs = xdata.xprs[3]
+        rhs_basic = xdata.xprs[2]
         memaddr = xdata.xprs[4]
         rdefs = xdata.reachingdefs
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
 
-        hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
+        if rhs.has_variables_with_property(
+                lambda v: v.is_initial_memory_value
+                and xdata.function.has_var_disequality(iaddr, v)):
+            hl_rhs = XU.xxpr_to_ast_def_expr(rhs_basic, xdata, iaddr, astree)
+        else:
+            hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
+
         hl_lhs = XU.xvariable_to_ast_lval(
             lhs, xdata, iaddr, astree, memaddr=memaddr)
 
diff --git a/chb/arm/opcodes/ARMUnsignedBitFieldExtract.py b/chb/arm/opcodes/ARMUnsignedBitFieldExtract.py
@@ -111,44 +111,43 @@ def ast_prov(
 
         annotations: List[str] = [iaddr, "UBFX"]
 
+        (ll_rhs, _, _) = self.opargs[1].ast_rvalue(astree)
+        (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree)
+
+        ll_assign = astree.mk_assign(
+            ll_lhs,
+            ll_rhs,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        rdefs = xdata.reachingdefs
+
+        astree.add_expr_reachingdefs(ll_rhs, [rdefs[0]])
+
+        # high-level assignment
+
         lhs = xdata.vars[0]
         rhs = xdata.xprs[1]
-        rdefs = xdata.reachingdefs
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
 
-        (ll_rhs, _, _) = self.opargs[1].ast_rvalue(astree)
-        (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree)
-
-        hl_lhss = XU.xvariable_to_ast_lvals(lhs, xdata, astree)
-
-        try:
-            hl_rhss = XU.xxpr_to_ast_def_exprs(rhs, xdata, iaddr, astree)
-        except UF.CHBError as e:
-            chklogger.logger.error(
-                "Error in UBFX at address %s: %s", iaddr, str(e))
-            hl_rhss = [ll_rhs]
-
-        if len(hl_rhss) == 1 and len(hl_lhss) == 1:
-            hl_lhs = hl_lhss[0]
-            hl_rhs = hl_rhss[0]
-
-            return self.ast_variable_intro(
-                astree,
-                astree.astree.unsigned_char_type,
-                hl_lhs,
-                hl_rhs,
-                ll_lhs,
-                ll_rhs,
-                rdefs[1:],
-                [rdefs[0]],
-                defuses[0],
-                defuseshigh[0],
-                True,
-                iaddr,
-                annotations,
-                bytestring)
-
-        else:
-            raise UF.CHBError(
-                "ARMUnsignedBitFieldExtract: multiple expressions/lvals in ast")
+        hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
+        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_lval_defuses(hl_lhs, defuses[0])
+        astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
+
+        return ([hl_assign], [ll_assign])
diff --git a/chb/arm/opcodes/ARMUnsignedExtendHalfword.py b/chb/arm/opcodes/ARMUnsignedExtendHalfword.py
@@ -120,42 +120,42 @@ def ast_prov(
 
         annotations: List[str] = [iaddr, "UXTH"]
 
-        lhs = xdata.vars[0]
-        rhs = xdata.xprs[2]
-        rdefs = xdata.reachingdefs
-        defuses = xdata.defuses
-        defuseshigh = xdata.defuseshigh
-
         (ll_rhs, _, _) = self.opargs[1].ast_rvalue(astree)
         (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree)
 
-        hl_lhss = XU.xvariable_to_ast_lvals(lhs, xdata, astree)
-        hl_rhss = XU.xxpr_to_ast_def_exprs(rhs, xdata, iaddr, astree)
+        ll_assign = astree.mk_assign(
+            ll_lhs,
+            ll_rhs,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
 
-        if len(hl_lhss) == 0:
-            raise UF.CHBError("UXTH: no lvals in ast")
-        if len(hl_lhss) > 1:
-            raise UF.CHBError("UXTH: multiple lvals in ast")
-        if len(hl_rhss) == 0:
-            raise UF.CHBError("UXTH: no rhs expressions in ast")
-        if len(hl_rhss) > 1:
-            raise UF.CHBError("UXTH: multiplve rhs expressions in ast")
+        rdefs = xdata.reachingdefs
 
-        hl_lhs = hl_lhss[0]
-        hl_rhs = hl_rhss[0]
+        astree.add_expr_reachingdefs(ll_rhs, [rdefs[0]])
 
-        return self.ast_variable_intro(
-            astree,
-            astree.astree.unsigned_short_type,
+        lhs = xdata.vars[0]
+        rhs = xdata.xprs[2]
+        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)
+
+        hl_assign = astree.mk_assign(
             hl_lhs,
             hl_rhs,
-            ll_lhs,
-            ll_rhs,
-            rdefs[1:],
-            [rdefs[0]],
-            defuses[0],
-            defuseshigh[0],
-            True,
-            iaddr,
-            annotations,
-            bytestring)
+            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[:1])
+        astree.add_lval_defuses(hl_lhs, defuses[0])
+        astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
+
+        return ([hl_assign], [ll_assign])
diff --git a/chb/invariants/XXpr.py b/chb/invariants/XXpr.py
@@ -39,7 +39,7 @@
 
 """
 from typing import (
-    Any, cast, Dict, List, Mapping, Optional, Sequence, TYPE_CHECKING)
+    Any, Callable, cast, Dict, List, Mapping, Optional, Sequence, TYPE_CHECKING)
 
 from chb.api.CallTarget import CallTarget
 
@@ -287,6 +287,10 @@ def has_global_variables(self) -> bool:
     def has_global_references(self) -> bool:
         return False
 
+    def has_variables_with_property(
+            self, p: Callable[[XVariable], bool]) -> bool:
+        return False
+
     def negated_value(self) -> int:
         raise UF.CHBError("Get_negated_value not supported for " + str(self))
 
@@ -437,6 +441,10 @@ def has_global_variables(self) -> bool:
     def has_global_references(self) -> bool:
         return self.has_global_variables()
 
+    def has_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()
@@ -737,6 +745,10 @@ def has_global_variables(self) -> bool:
     def has_global_references(self) -> bool:
         return any([op.has_global_references() for op in self.operands])
 
+    def has_variables_with_property(
+            self, p: Callable[[XVariable], bool]) -> bool:
+        return any([op.has_variables_with_property(p) for op in self.operands])
+
     @property
     def is_stack_address(self) -> bool:
         args = self.operands
diff --git a/chb/invariants/XXprUtil.py b/chb/invariants/XXprUtil.py
@@ -390,7 +390,7 @@ def memory_variable_to_lval_expression(
         return astree.mk_vinfo_lval_expression(
             vinfo, astoffset, anonymous=anonymous)
 
-    elif offset.is_array_index_offset:
+    if offset.is_array_index_offset:
         offset = cast("VMemoryOffsetArrayIndexOffset", offset)
         index = offset.index_expression
         astindex = xxpr_to_ast_def_expr(
@@ -411,10 +411,22 @@ def memory_variable_to_lval_expression(
             return astree.mk_vinfo_lval_expression(
                 vinfo,astindexoffset, anonymous=anonymous)
 
+    if offset.is_index_offset:
+        offset = cast("VMemoryOffsetIndexOffset", offset)
+        indexvar = offset.indexvariable
+        astindexvar = xvariable_to_ast_def_lval_expression(
+            indexvar, xdata, iaddr, astree, anonymous=anonymous)
+        suboffset = offset.offset
+
+        if suboffset.is_no_offset:
+            astindexoffset = astree.mk_expr_index_offset(astindexvar)
+            return astree.mk_vinfo_lval_expression(
+                vinfo, astindexoffset, anonymous=anonymous)
+
     chklogger.logger.error(
-        "AST conversion of memory variable %s with other offset not yet "
+        "AST conversion of memory variable %s with other offset: %s not yet "
         + "supported at address %s",
-        name, iaddr)
+        name, str(offset), iaddr)
 
     return astree.mk_temp_lval_expression()
 
@@ -1000,7 +1012,7 @@ def default() -> AST.ASTExpr:
             xpr2, xdata, iaddr, astree, anonymous=anonymous)
         if operator in [
                 "plus", "minus", "mult", "div",
-                "band", "land", "lor", "bor", "asr",
+                "band", "land", "lor", "bor", "asr", "bxor",
                 "lsl", "lsr", "eq", "ne", "gt", "le", "lt", "ge"]:
             return astree.mk_binary_expression(operator, astxpr1, astxpr2)
         else:

Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-chbversion: str = "0.3.0-20241028"`
	`1`	`+chbversion: str = "0.3.0-20241111"`