@@ -1294,8 +1294,8 @@ bool mustVisitForkBranches(ref<Target> target, KInstruction *instr) {
12941294 // fork branches here
12951295 if (auto reprErrorTarget = dyn_cast<ReproduceErrorTarget>(target)) {
12961296 return reprErrorTarget->isTheSameAsIn (instr) &&
1297- reprErrorTarget->isThatError (
1298- ReachWithError ::NullCheckAfterDerefException);
1297+ reprErrorTarget->isThatError (ReachWithError (
1298+ ReachWithErrorType ::NullCheckAfterDerefException) );
12991299 }
13001300 return false ;
13011301}
@@ -2674,8 +2674,9 @@ void Executor::checkNullCheckAfterDeref(ref<Expr> cond, ExecutionState &state) {
26742674 if (eqPointerCheck && eqPointerCheck->left ->isZero () &&
26752675 state.resolvedPointers .count (
26762676 makePointer (eqPointerCheck->right )->getBase ())) {
2677- reportStateOnTargetError (state,
2678- ReachWithError::NullCheckAfterDerefException);
2677+ reportStateOnTargetError (
2678+ state,
2679+ ReachWithError (ReachWithErrorType::NullCheckAfterDerefException));
26792680 }
26802681}
26812682
@@ -2687,10 +2688,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
26872688 auto target = kvp.first ;
26882689 if (target->shouldFailOnThisTarget () &&
26892690 cast<ReproduceErrorTarget>(target)->isThatError (
2690- ReachWithError::Reachable) &&
2691+ ReachWithError (ReachWithErrorType ::Reachable) ) &&
26912692 target->getBlock () == ki->parent &&
26922693 cast<ReproduceErrorTarget>(target)->isTheSameAsIn (ki)) {
2693- terminateStateOnTargetError (state, ReachWithError::Reachable);
2694+ terminateStateOnTargetError (
2695+ state, ReachWithError (ReachWithErrorType::Reachable));
26942696 return ;
26952697 }
26962698 }
@@ -4998,25 +5000,25 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
49985000 // Proceed with normal `terminateStateOnError` call
49995001 std::string messaget;
50005002 StateTerminationType terminationType;
5001- switch (error) {
5002- case ReachWithError ::MayBeNullPointerException:
5003- case ReachWithError ::MustBeNullPointerException:
5003+ switch (error. type ) {
5004+ case ReachWithErrorType ::MayBeNullPointerException:
5005+ case ReachWithErrorType ::MustBeNullPointerException:
50045006 messaget = " memory error: null pointer exception" ;
50055007 terminationType = StateTerminationType::Ptr;
50065008 break ;
5007- case ReachWithError ::DoubleFree:
5009+ case ReachWithErrorType ::DoubleFree:
50085010 messaget = " double free error" ;
50095011 terminationType = StateTerminationType::Ptr;
50105012 break ;
5011- case ReachWithError ::UseAfterFree:
5013+ case ReachWithErrorType ::UseAfterFree:
50125014 messaget = " use after free error" ;
50135015 terminationType = StateTerminationType::Ptr;
50145016 break ;
5015- case ReachWithError ::Reachable:
5017+ case ReachWithErrorType ::Reachable:
50165018 messaget = " " ;
50175019 terminationType = StateTerminationType::Reachable;
50185020 break ;
5019- case ReachWithError ::None:
5021+ case ReachWithErrorType ::None:
50205022 default :
50215023 messaget = " unspecified error" ;
50225024 terminationType = StateTerminationType::User;
@@ -5025,11 +5027,15 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
50255027 state, new ErrorEvent (locationOf (state), terminationType, messaget));
50265028}
50275029
5028- // TODO: add taint target errors to taint-annotations.json and change function
5029- void Executor::terminateStateOnTargetTaintError (ExecutionState &state, size_t rule) {
5030- const std::string &ruleStr = annotationsData.taintAnnotation .rules [rule];
5030+ void Executor::terminateStateOnTargetTaintError (ExecutionState &state,
5031+ size_t rule) {
5032+ if (rule >= annotationsData.taintAnnotation .rules .size ()) {
5033+ terminateStateOnUserError (state, " Incorrect rule id" );
5034+ }
50315035
5032- // reportStateOnTargetError(state, rule);
5036+ const std::string &ruleStr = annotationsData.taintAnnotation .rules [rule];
5037+ reportStateOnTargetError (
5038+ state, ReachWithError (ReachWithErrorType::MaybeTaint, ruleStr));
50335039
50345040 terminateStateOnProgramError (state, ruleStr + " taint error" ,
50355041 StateTerminationType::Taint);
@@ -5500,8 +5506,8 @@ void Executor::executeFree(ExecutionState &state, ref<PointerExpr> address,
55005506 if (!resolveExact (*zeroPointer.second , address,
55015507 typeSystemManager->getUnknownType (), rl, " free" ) &&
55025508 guidanceKind == GuidanceKind::ErrorGuidance) {
5503- terminateStateOnTargetError (*zeroPointer. second ,
5504- ReachWithError::DoubleFree);
5509+ terminateStateOnTargetError (
5510+ *zeroPointer. second , ReachWithError (ReachWithErrorType ::DoubleFree) );
55055511 return ;
55065512 }
55075513
@@ -5566,9 +5572,9 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
55665572 ExecutionState *bound = branches.first ;
55675573 if (bound) {
55685574 auto error = isReadFromSymbolicArray (uniqueBase)
5569- ? ReachWithError ::MayBeNullPointerException
5570- : ReachWithError ::MustBeNullPointerException;
5571- terminateStateOnTargetError (*bound, error);
5575+ ? ReachWithErrorType ::MayBeNullPointerException
5576+ : ReachWithErrorType ::MustBeNullPointerException;
5577+ terminateStateOnTargetError (*bound, ReachWithError ( error) );
55725578 }
55735579 if (!branches.second ) {
55745580 address =
@@ -6248,9 +6254,9 @@ void Executor::executeMemoryOperation(
62486254 ExecutionState *bound = branches.first ;
62496255 if (bound) {
62506256 auto error = (isReadFromSymbolicArray (base) && branches.second )
6251- ? ReachWithError ::MayBeNullPointerException
6252- : ReachWithError ::MustBeNullPointerException;
6253- terminateStateOnTargetError (*bound, error);
6257+ ? ReachWithErrorType ::MayBeNullPointerException
6258+ : ReachWithErrorType ::MustBeNullPointerException;
6259+ terminateStateOnTargetError (*bound, ReachWithError ( error) );
62546260 }
62556261 if (!branches.second )
62566262 return ;
@@ -6372,7 +6378,8 @@ void Executor::executeMemoryOperation(
63726378 solver->setTimeout (time::Span ());
63736379
63746380 if (!success) {
6375- terminateStateOnTargetError (*state, ReachWithError::UseAfterFree);
6381+ terminateStateOnTargetError (
6382+ *state, ReachWithError (ReachWithErrorType::UseAfterFree));
63766383 return ;
63776384 }
63786385 }
@@ -6986,7 +6993,7 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv,
69866993 auto kCallBlock = kfIt->second ->entryKBlock ;
69876994 forest = new TargetForest (kEntryFunction );
69886995 forest->add (ReproduceErrorTarget::create (
6989- {ReachWithError::Reachable}, " " ,
6996+ {ReachWithError (ReachWithErrorType ::Reachable) }, " " ,
69906997 ErrorLocation (kCallBlock ->getFirstInstruction ()), kCallBlock ));
69916998 }
69926999 }
@@ -7461,9 +7468,9 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
74617468 // we cannot be sure that an irreproducible state proves the presence of an
74627469 // error
74637470 if (uninitObjects.size () > 0 || state.symbolics .size () != symbolics.size ()) {
7464- state.error = ReachWithError::None;
7471+ state.error = ReachWithError (ReachWithErrorType ::None) ;
74657472 } else if (FunctionCallReproduce != " " &&
7466- state.error == ReachWithError ::Reachable) {
7473+ state.error . type == ReachWithErrorType ::Reachable) {
74677474 setHaltExecution (HaltExecution::ReachedTarget);
74687475 }
74697476
0 commit comments