[docs]classSlicecutor(ExplorationTechnique):""" The Slicecutor is an exploration that executes provided code slices. """
[docs]def__init__(self,annotated_cfg,force_taking_exit=False,force_sat:bool=False):""" All parameters except `annotated_cfg` are optional. :param annotated_cfg: The AnnotatedCFG that provides the code slice. :param force_taking_exit: Set to True if you want to create a successor based on our slice in case of unconstrained successors. :param force_sat: If a branch specified by the slice is unsatisfiable, set this option to True if you want to force it to be satisfiable and be taken anyway. """super().__init__()self._annotated_cfg=annotated_cfgself._force_taking_exit=force_taking_exitself._force_sat=force_sat
[docs]deffilter(self,simgr,state,**kwargs):l.debug("Checking state %s for filtering...",state)returnsimgr.filter(state,**kwargs)
[docs]defstep_state(self,simgr,state,**kwargs):l.debug("%s ticking state %s at address %#x.",self,state,state.addr)stashes=simgr.step_state(state,**kwargs)new_active=[]new_cut=[]new_mystery=[]# SimulationManager returns new active states in the None stash by default.flat_successors=stashes.get(None,None)ifflat_successorsisNone:# Did the user explicitly put them into the 'active' stash instead?flat_successors=stashes.pop("active",[])forsuccessorinflat_successors:l.debug("... checking exit to %#x from %#x.",successor.addr,state.addr)try:taken=self._annotated_cfg.should_take_exit(state.addr,successor.addr)exceptAngrExitError:# TODO: which exception?l.debug("... annotated CFG did not know about it!")new_mystery.append(successor)else:iftaken:l.debug("... taking the exit.")new_active.append(successor)# the else case isn't here, because the state should set errored in this# case and we'll catch it belowelse:l.debug("... not taking the exit.")new_cut.append(successor)unconstrained_successors=stashes.get("unconstrained",[])ifnotnew_activeandunconstrained_successorsandself._force_taking_exit:stashes["unconstrained"]=[]# somehow there is no feasible state. We are forced to create a successor based on our sliceiflen(unconstrained_successors)!=1:raiseException("This should absolutely never happen, what?")fortargetinself._annotated_cfg.get_targets(state.addr):successor=unconstrained_successors[0].copy()successor.regs._ip=targetnew_active.append(successor)l.debug("Got unconstrained: %d new states are created based on AnnotatedCFG.",len(new_active))unsat_successors=stashes.get("unsat",None)ifnotnew_activeandunsat_successorsandself._force_sat:stashes["unsat"]=[]# find the statetargets=self._annotated_cfg.get_targets(state.addr)iftargetsisNone:targets=[]fortargetintargets:try:suc=next(iter(uforuinunsat_successorsifu.addr==target))exceptStopIteration:continue# drop all constraintsifsuc.mode=="fastpath":# dropping constraints and making the state satisfiable again under fastpath mode is easysuc.solver._solver.constraints=[]suc._satisfiable=Truenew_active.append(suc)l.debug("Forced unsat at %#x to be sat again.",suc.addr)else:# with multiple possible solver frontends, dropping states in other state modes is not# straightforward. I'll leave it to the next person who uses this featurel.warning("force_sat is not implemented for solver mode %s.",suc.moe)stashes[None]=new_activestashes["mystery"]=new_mysterystashes["cut"]=new_cutreturnstashes