ASTI: add support for stack arguments

Author: sipma

chb/api/AppFunctionSignature.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2023  Aarno Labs LLC
+# Copyright (c) 2023-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
@@ -54,7 +54,9 @@ class AppFunctionSignature(InterfaceDictionaryRecord):
     args[6..]: indices of registers preserved (not normally preserved)
     """
 
-    def __init__(self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
+    def __init__(
+            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue
+    ) -> None:
         InterfaceDictionaryRecord.__init__(self, ixd, ixval)
 
     @property
@@ -69,16 +71,22 @@ def parameter_list(self) -> List["FtsParameter"]:
     def returntype(self) -> "BCTyp":
         return self.bcd.typ(self.args[3])
 
-    def index_of_register_parameter_location(self, r: "Register") -> Optional[int]:
+    def index_of_register_parameter_location(
+            self, r: "Register") -> Optional[int]:
         for p in self.parameter_list:
             if p.is_register_parameter_location(r):
                 return p.argindex
         return None
 
+    def index_of_stack_parameter_location(self, offset: int) -> Optional[int]:
+        for p in self.parameter_list:
+            if p.is_stack_parameter_location(offset):
+                return p.argindex
+        return None
+
     def __str__(self) -> str:
         return (
             str(self.returntype)
             + " ("
             + ", ".join(str(p) for p in self.parameter_list)
             + ")")
-        

chb/api/FtsParameter.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2023  Aarno Labs LLC
+# Copyright (c) 2023-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
@@ -80,5 +80,10 @@ def is_register_parameter_location(self, r: "Register") -> bool:
             return self.parameter_location_list[0].is_register_parameter_location_of(r)
         return False
 
+    def is_stack_parameter_location(self, offset: int) -> bool:
+        if len(self.parameter_location_list) == 1:
+            return self.parameter_location_list[0].is_stack_parameter_location_of(offset)
+        return False
+
     def __str__(self) -> str:
         return str(self.typ) + " " + str(self.name)

chb/api/FtsParameterLocation.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2023  Aarno Labs LLC
+# Copyright (c) 2023-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
@@ -81,6 +81,9 @@ def is_unknown_location(self) -> bool:
     def is_register_parameter_location_of(self, r: "Register") -> bool:
         return False
 
+    def is_stack_parameter_location_of(self, offset: int) -> bool:
+        return False
+
 
 @apiregistry.register_tag("s", FtsParameterLocation)
 class FtsStackParameter(FtsParameterLocation):
@@ -98,9 +101,12 @@ def is_stack_parameter(self) -> bool:
         return True
 
     @property
-    def index(self) -> int:
+    def offset(self) -> int:
         return self.args[0]
 
+    def is_stack_parameter_location_of(self, offset: int) -> bool:
+        return offset == self.offset
+
     def __str__(self) -> str:
         return "stack-parameter " + str(self.index)
 

chb/invariants/VAssemblyVariable.py

@@ -250,7 +250,7 @@ def is_stack_argument(self) -> bool:
         return (
             self.base.is_local_stack_frame
             and self.offset.is_constant_value_offset
-            and self.offset.offsetvalue() > 0)
+            and self.offset.offsetvalue() >= 0)
 
     @property
     def is_local_stack_variable(self) -> bool:

chb/invariants/XXprUtil.py

@@ -601,6 +601,40 @@ def vargument_deref_value_to_ast_lval_expression(
     return astree.mk_temp_lval_expression()
 
 
+def stack_argument_to_ast_lval_expression(
+        offset: int,
+        xdata: "InstrXData",
+        iaddr: str,
+        astree: ASTInterface,
+        anonymous: bool = False) -> AST.ASTExpr:
+
+    fsig = astree.appsignature
+    if fsig is None:
+        chklogger.logger.error(
+            "Unable to judge stack argument with offset %d without app "
+            + "at address %s",
+            offset, iaddr)
+        return astree.mk_temp_lval_expression()
+
+    optindex = fsig.index_of_stack_parameter_location(offset)
+    if optindex is not None:
+        arglvals = astree.function_argument(optindex - 1)
+        if len(arglvals) != 1:
+            chklogger.logger.error(
+                "Encountered multiple arg values for initial stack argument "
+                + "%s at address %s",
+                str(offset), iaddr)
+            return astree.mk_temp_lval_expression()
+        else:
+            return astree.mk_lval_expression(arglvals[0], anonymous=anonymous)
+    else:
+        chklogger.logger.error(
+            "Cannot determine argument index for initial stack argument %s "
+            + "at address %s",
+            str(offset), iaddr)
+        return astree.mk_temp_lval_expression()
+
+
 def vinitmemory_value_to_ast_lval_expression(
         vconstvar: "VInitialMemoryValue",
         xdata: "InstrXData",
@@ -678,6 +712,10 @@ def vinitmemory_value_to_ast_lval_expression(
             iaddr)
         return astree.mk_temp_lval_expression()
 
+    if avar.is_memory_variable and avar.is_stack_argument:
+        return stack_argument_to_ast_lval_expression(
+            avar.offset.offsetvalue(), xdata, iaddr, astree, anonymous=anonymous)
+
     chklogger.logger.error(
         "AST conversion of vinitmemory value %s of %s not yet supported at "
         + "address %s",