[docs]classSimStatePreconstrainer(SimStatePlugin):""" This state plugin manages the concept of preconstraining - adding constraints which you would like to remove later. :param constrained_addrs: SimActions for memory operations whose addresses should be constrained during crash analysis """
[docs]def__init__(self,constrained_addrs=None):SimStatePlugin.__init__(self)# map of variable string names to preconstraints, for re-applying constraints.self.variable_map={}self.preconstraints=[]self._constrained_addrs=[]ifconstrained_addrsisNoneelseconstrained_addrsself.address_concretization=[]
[docs]defmerge(self,others,merge_conditions,common_ancestor=None):# pylint: disable=unused-argumentl.warning("Merging is not implemented for preconstrainer!")returnFalse
[docs]defwiden(self,others):# pylint: disable=unused-argumentl.warning("Widening is not implemented for preconstrainer!")returnFalse
[docs]defpreconstrain(self,value,variable):""" Add a preconstraint that ``variable == value`` to the state. :param value: The concrete value. Can be a bitvector or a bytestring or an integer. :param variable: The BVS to preconstrain. """ifnotisinstance(value,claripy.ast.Base):value=self.state.solver.BVV(value,len(variable))elifvalue.op!="BVV":raiseValueError("Passed a value to preconstrain that was not a BVV or a string")ifvariable.opnotinclaripy.operations.leaf_operations:l.warning("The variable %s to preconstrain is not a leaf AST. This may cause replacement failures in the ""claripy replacement backend.",variable,)l.warning("Please use a leaf AST as the preconstraining variable instead.")# Add the constraint with a simplification avoidance tag. If# this is not added, claripy may simplify new constraints if# they are redundant with respect to the preconstraints. This# is problematic when the preconstraints are removed.constraint=(variable==value).annotate(claripy.SimplificationAvoidanceAnnotation())l.debug("Preconstraint: %s",constraint)# add the constraint for reconstraining laterifnext(iter(variable.variables))inself.variable_map:l.warning("%s is already preconstrained. Are you misusing preconstrainer?",next(iter(variable.variables)))self.variable_map[next(iter(variable.variables))]=constraintself.preconstraints.append(constraint)ifo.REPLACEMENT_SOLVERinself.state.options:self.state.solver._solver.add_replacement(variable,value,invalidate_cache=False)else:self.state.add_constraints(constraint)ifnotself.state.satisfiable():l.warning("State went unsat while adding preconstraints")
[docs]defpreconstrain_file(self,content,simfile,set_length=False):""" Preconstrain the contents of a file. :param content: The content to preconstrain the file to. Can be a bytestring or a list thereof. :param simfile: The actual simfile to preconstrain """repair_entry_state_opts=Falseifo.TRACK_ACTION_HISTORYinself.state.options:repair_entry_state_opts=Trueself.state.options-={o.TRACK_ACTION_HISTORY}ifset_length:# disable read boundssimfile.has_end=Falsepos=0forwriteincontent:iftype(write)isint:write=bytes([write])data,length,pos=simfile.read(pos,len(write),disable_actions=True,inspect=False,short_reads=False)ifnotclaripy.is_true(length==len(write)):raiseAngrError("Bug in either SimFile or in usage of preconstrainer: couldn't get requested data from file")self.preconstrain(write,data)# if the file is a stream, reset its positionifsimfile.posisnotNone:simfile.pos=0ifset_length:# enable read bounds; size is now maximum sizesimfile.has_end=Trueifrepair_entry_state_opts:self.state.options|={o.TRACK_ACTION_HISTORY}
[docs]defpreconstrain_flag_page(self,magic_content):""" Preconstrain the data in the flag page. :param magic_content: The content of the magic page as a bytestring. """form,vinzip(magic_content,self.state.cgc.flag_bytes):self.preconstrain(m,v)
[docs]defremove_preconstraints(self,to_composite_solver=True,simplify=True):""" Remove the preconstraints from the state. If you are using the zen plugin, this will also use that to filter the constraints. :param to_composite_solver: Whether to convert the replacement solver to a composite solver. You probably want this if you're switching from tracing to symbolic analysis. :param simplify: Whether to simplify the resulting set of constraints. """ifnotself.preconstraints:return# cache key set creationprecon_cache_keys=set()forconinself.preconstraints:precon_cache_keys.add(con.cache_key)# if we used the replacement solver we didn't add constraints we need to remove so keep all constraintsifo.REPLACEMENT_SOLVERinself.state.options:new_constraints=self.state.solver.constraintselse:new_constraints=[xforxinself.state.solver.constraintsifx.cache_keynotinprecon_cache_keys]ifself.state.has_plugin("zen_plugin"):new_constraints=self.state.get_plugin("zen_plugin").filter_constraints(new_constraints)ifto_composite_solver:self.state.options.discard(o.REPLACEMENT_SOLVER)self.state.options.add(o.COMPOSITE_SOLVER)# clear the solver's internal memory and replace it with the new solver options and constraintsself.state.solver.reload_solver(new_constraints)ifsimplify:l.debug("simplifying solver...")self.state.solver.simplify()l.debug("...simplification done")
[docs]defreconstrain(self):""" Split the solver. If any of the subsolvers time out after a short timeout (10 seconds), re-add the preconstraints associated with each of its variables. Hopefully these constraints still allow us to do meaningful things to the state. """# test all solver splitssubsolvers=self.state.solver._solver.split()forsolverinsubsolvers:solver.timeout=1000*10# 10 secondstry:solver.satisfiable()exceptclaripy.errors.ClaripySolverInterruptError:forvarinsolver.variables:ifvarinself.variable_map:self.state.add_constraints(self.variable_map[var])else:l.warning("var %s not found in self.variable_map",var)