Merge branch 'develop' into main

cozy/analysis.py

@@ -231,7 +231,8 @@ def difference(self,
                    compute_reg_diff=True,
                    compute_side_effect_diff=True,
                    use_unsat_core=True,
-                   simplify=False) -> DiffResult | None:
+                   simplify=False,
+                   extra_constraints=[]) -> DiffResult | None:
         """
         Compares two states to find differences in memory. This function will return None if the two states have\
         non-intersecting inputs. Otherwise, it will return a dict of addresses and a dict of registers which are\
@@ -271,6 +272,9 @@ def difference(self,
         joint_solver.add(sl.solver.constraints)
         joint_solver.add(sr.solver.constraints)
 
+        for constraint in extra_constraints:
+            joint_solver.add(constraint)
+
         try:
             is_sat = joint_solver.satisfiable()
         except claripy.ClaripyZ3Error as err:
@@ -481,7 +485,7 @@ def concrete_examples(self, args: any, num_examples=3) -> list[CompatiblePairInp
         Concretizes the arguments used to put the program in these states by jointly using the constraints attached to\
         the compatible states.
 
-        :param any args: The input arguments to concretize. This argument may be a Python datastructure, the\
+        :param any args: The input arguments to concretize. This argument may be a Python datastructure, the \
         concretizer will make a deep copy with claripy symbolic variables replaced with concrete values.
         :param int num_examples: The maximum number of concrete examples to generate for this particular pair.
         :return: A list of concrete inputs that satisfy both constraints attached to the states.
@@ -574,6 +578,8 @@ def __init__(self, pre_patched: RunResult, post_patched: RunResult, ignore_addrs
         total_num_pairs = len(states_pre_patched) * len(states_post_patched)
         count = 0
 
+        extra_constraints = []
+
         for (i, state_pre) in enumerate(states_pre_patched):
             for (j, state_post) in enumerate(states_post_patched):
                 count += 1
@@ -589,12 +595,14 @@ def __init__(self, pre_patched: RunResult, post_patched: RunResult, ignore_addrs
                 is_deadended_comparison = isinstance(state_pre, DeadendedState) and isinstance(state_post, DeadendedState)
 
                 diff = memoized_diff.difference(
-                    state_pre.state, state_post.state, pair_ignore_addrs,
+                    state_pre.state, state_post.state,
+                    pair_ignore_addrs,
                     compute_mem_diff=compare_memory if is_deadended_comparison else False,
                     compute_reg_diff=compare_registers if is_deadended_comparison else False,
                     compute_side_effect_diff=compare_side_effects if is_deadended_comparison else False,
                     use_unsat_core=use_unsat_core,
-                    simplify=simplify
+                    simplify=simplify,
+                    extra_constraints=extra_constraints
                 )
 
                 if diff is not None:

cozy/claripy_ext.py

@@ -39,6 +39,14 @@ def simplify_kb(expr: claripy.ast.bits, kb: claripy.ast.Bool) -> claripy.ast.bit
 def get_symbol_name(sym):
     return sym.args[0]
 
+def sub_asts(expr):
+    yield expr
+    for child in expr.children_asts():
+        yield child
+
+def sym_variables(expr):
+    return {child for child in sub_asts(expr) if child.depth == 1 and child.symbolic}
+
 def model(constraints,
           extra_symbols: set[typing.Union[claripy.BVS, claripy.FPS]] | frozenset[typing.Union[claripy.BVS, claripy.FPS]]=frozenset(),
           n=1,
@@ -95,7 +103,11 @@ def value(sym, v):
                             else:
                                 ret[leaf] = zero(leaf)
             else:
-                raise ValueError("Failed to generate a model for a satisfiable solution")
+                if len(solver.constraints) == 0:
+                    for extra in extra_symbols:
+                        ret[extra] = zero(extra)
+                else:
+                    raise ValueError("Failed to generate a model for a satisfiable solution")
 
             # Set any symbols not in the model to 0
             for extra in extra_symbols:

cozy/primitives.py

@@ -18,8 +18,8 @@ def sym_ptr(arch: Type[Arch], name: str | None=None) -> claripy.BVS:
     """
     global _malloc_name_ctr
     if name is None:
-        name = "symbolic_ptr_{}".format(_name_ctr)
-        _name_ctr += 1
+        name = "symbolic_ptr_{}".format(_malloc_name_ctr)
+        _malloc_name_ctr += 1
     return claripy.BVS(name, arch.bits)
 
 def sym_ptr_constraints(symbolic_ptr: claripy.ast.bits, concrete_addr: int, can_be_null: bool=True) -> claripy.ast.bool:

cozy/project.py

@@ -6,7 +6,7 @@
 from angr import SimProcedure
 from cle import Backend
 
-from cozy.session import Session
+from cozy.session import Session, UnderconstrainedMachineState
 
 
 class Project:
@@ -44,6 +44,13 @@ def object_ranges(self, obj_filter: Callable[[Backend], bool] | None=None) -> li
             obj_filter = lambda x: True
         return [range(obj.min_addr, obj.max_addr + 1) for obj in self.angr_proj.loader.all_objects if obj_filter(obj)]
 
+    def try_find_symbol_addr(self, sym_name: str) -> int | None:
+        sym = self.angr_proj.loader.find_symbol(sym_name)
+        if sym is not None:
+            return sym.rebased_addr
+        else:
+            return None
+
     def find_symbol_addr(self, sym_name: str) -> int:
         """
         Finds the rebased addressed of a symbol. Functions are the most common symbol type.
@@ -70,15 +77,25 @@ def add_prototype(self, fun: str | int, fun_prototype: str) -> None:
         """
         self.fun_prototypes[fun] = fun_prototype
 
-    def session(self, start_fun: str | int | None=None) -> Session:
+    def session(self, start_fun: str | int | None=None, underconstrained_execution: bool=False,
+                underconstrained_initial_state: UnderconstrainedMachineState | None=None) -> Session:
         """
         Returns a new session derived from this project.
 
-        :param str | int | None start_fun: The name or address of the function which this session will start with. If None is specified, then the program will start at the entry point (main function).
+        :param str | int | None start_fun: The name or address of the function which this session will start with.\
+        If None is specified, then the program will start at the entry point (main function).
+        :param bool underconstrained_execution: Set to True to enable underconstrained symbolic execution. With this\
+        option, all initial registers will be initialized with unconstrained fresh symbolic variables, and memory\
+        contents that are not initialized will likewise return fresh unconstrained symbolic variables.
+        :param UnderconstrainedMachineState underconstrained_initial_state: If this value is not None, then\
+        the inferred memory layout from a previous unconstrained symbolic execution should be used. You can retrieve\
+        this value from a previous :py:class:`~cozy.session.RunResult` via the\
+        :py:class:`cozy.session.RunResult.underconstrained_machine_state` field.
         :return: The fresh session.
         :rtype: Session
         """
-        return Session(self, start_fun=start_fun)
+        return Session(self, start_fun=start_fun, underconstrained_execution=underconstrained_execution,
+                       underconstrained_initial_state=underconstrained_initial_state)
 
     @property
     def cfg(self):