From 4dd665d5d668666df9a938c415978b098df12707 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 5 Feb 2025 00:16:13 -0800 Subject: [PATCH] INV: add more support for typecast value --- chb/app/CHVersion.py | 2 +- chb/arm/opcodes/ARMLoadRegister.py | 13 ++++--- chb/invariants/XXprUtil.py | 59 ++++++++++++++++++++++++------ 3 files changed, 55 insertions(+), 19 deletions(-) diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index 34d0dc97..1aa94f99 100644 --- a/chb/app/CHVersion.py +++ b/chb/app/CHVersion.py @@ -1 +1 @@ -chbversion: str = "0.3.0-20250203" +chbversion: str = "0.3.0-20250204" diff --git a/chb/arm/opcodes/ARMLoadRegister.py b/chb/arm/opcodes/ARMLoadRegister.py index 4ebe741e..5f91a5d3 100644 --- a/chb/arm/opcodes/ARMLoadRegister.py +++ b/chb/arm/opcodes/ARMLoadRegister.py @@ -205,12 +205,18 @@ 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: rhs = xd.xrmem + rhsval = None if has_cast() else xd.xrmem xaddr = xd.xaddr - hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + 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, memaddr=xaddr) @@ -230,11 +236,6 @@ def ast_prov( defuses = xdata.defuses defuseshigh = xdata.defuseshigh - def has_cast() -> bool: - return ( - astree.has_register_variable_intro(iaddr) - and astree.get_register_variable_intro(iaddr).has_cast()) - if has_cast(): lhstype = hl_lhs.ctype(astree.ctyper) if lhstype is not None: diff --git a/chb/invariants/XXprUtil.py b/chb/invariants/XXprUtil.py index 3265b94d..ac2c2ae4 100644 --- a/chb/invariants/XXprUtil.py +++ b/chb/invariants/XXprUtil.py @@ -374,6 +374,34 @@ def memory_variable_to_lval_expression( size: int = 4, anonymous: bool = False) -> AST.ASTExpr: + if base.is_basevar: + base = cast("VMemoryBaseBaseVar", base) + if base.basevar.is_typecast_value: + tcval = cast("VTypeCastValue", base.basevar.denotation.auxvar) + asttgttype = tcval.tgttype.convert(astree.typconverter) + vinfo = astree.mk_vinfo(tcval.name, vtype=asttgttype) + astbase = astree.mk_vinfo_lval_expression(vinfo) + if offset.is_field_offset: + offset = cast("VMemoryOffsetFieldOffset", offset) + astoffset: AST.ASTOffset = field_offset_to_ast_offset( + offset, xdata, iaddr, astree) + elif offset.is_array_index_offset: + offset = cast("VMemoryOffsetArrayIndexOffset", offset) + astoffset = array_offset_to_ast_offset(offset, xdata, iaddr, astree) + elif offset.is_constant_value_offset: + astoffset = astree.mk_scalar_index_offset(offset.offsetvalue()) + else: + astoffset = nooffset + return astree.mk_memref_expr( + astbase, offset=astoffset, anonymous=anonymous) + + else: + chklogger.logger.error( + "AST conversion of non-typecast basevar %s at address %s " + + "not yet supported", + str(base), iaddr) + return astree.mk_temp_lval_expression() + name = str(base) if not astree.globalsymboltable.has_symbol(name): @@ -690,6 +718,9 @@ def vinitmemory_value_to_ast_lval_expression( if astbasetype.is_pointer: tgttype = cast(AST.ASTTypPtr, astbasetype).tgttyp + if tgttype.is_scalar: + return astree.mk_memref_expr(astbase, anonymous=anonymous) + if tgttype.is_compound: compkey = cast(AST.ASTTypComp, tgttype).compkey @@ -1050,12 +1081,13 @@ def default() -> AST.ASTExpr: return default() subfoffset = astree.mk_field_offset(subfield.fieldname, fcompkey) else: - chklogger.logger.error( - "Non-struct type %s for field %s in second-level rest " - + "offset not yet " - + "handled for %s with offset %s at %s: %d", - str(field.fieldtype), field.fieldname, - str(axpr1), str(axpr2), iaddr, restoffset) + if not anonymous: + chklogger.logger.error( + "Non-struct type %s for field %s in second-level rest " + + "offset not yet " + + "handled for %s with offset %s at %s: %d", + str(field.fieldtype), field.fieldname, + str(axpr1), str(axpr2), iaddr, restoffset) return default() else: subfoffset = nooffset @@ -1125,8 +1157,9 @@ def default() -> AST.ASTExpr: if xpr1.is_compound and xpr2.is_constant: xc = cast(X.XprCompound, xpr1) - astxpr1 = xcompound_to_ast_def_expr(xc, xdata, iaddr, astree) - astxpr2 = xxpr_to_ast_expr(xpr2, xdata, iaddr, astree) + astxpr1 = xcompound_to_ast_def_expr( + xc, xdata, iaddr, astree, anonymous=anonymous) + astxpr2 = xxpr_to_ast_expr(xpr2, xdata, iaddr, astree, anonymous=anonymous) if operator in ["plus", "minus"]: return astree.mk_binary_expression(operator, astxpr1, astxpr2) else: @@ -1656,6 +1689,7 @@ def xvariable_to_ast_lval( rhs, xdata, iaddr, astree) else: astrhs = None + return astree.mk_ssa_register_variable_lval( str(xv), iaddr, vtype=ctype, ssavalue=astrhs) @@ -1795,10 +1829,11 @@ def vargument_deref_value_to_ast_lval( return astree.mk_memref_lval(vexpr, anonymous=anonymous) if not offset.is_constant_value_offset: - chklogger.logger.error( - "Non-constant offset: %s with variable %s not yet supported at " - + "address %s", - str(offset), str(basevar), iaddr) + if not anonymous: + chklogger.logger.error( + "Non-constant offset: %s with variable %s not yet supported at " + + "address %s", + str(offset), str(basevar), iaddr) return astree.mk_temp_lval() coff = offset.offsetvalue()