@@ -521,9 +521,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
521521 InterpreterHandler *ih)
522522 : Interpreter(opts), interpreterHandler(ih), searcher(nullptr ),
523523 externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0 ),
524- pathWriter(0 ), symPathWriter(0 ), specialFunctionHandler( 0 ),
525- timers{time::Span (TimerInterval)}, guidanceKind(opts.Guidance) ,
526- codeGraphInfo(new CodeGraphInfo()),
524+ pathWriter(0 ), symPathWriter(0 ),
525+ specialFunctionHandler( 0 ), timers{time::Span (TimerInterval)},
526+ guidanceKind (opts.Guidance), codeGraphInfo(new CodeGraphInfo()),
527527 distanceCalculator(new DistanceCalculator(*codeGraphInfo)),
528528 targetCalculator(new TargetCalculator(*codeGraphInfo)),
529529 targetManager(new TargetManager(guidanceKind, *distanceCalculator,
@@ -2753,8 +2753,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
27532753 branches.first ->lastBrConfidently = false ;
27542754 branches.second ->lastBrConfidently = false ;
27552755 } else {
2756- (branches.first ? branches.first : branches.second )->lastBrConfidently =
2757- true ;
2756+ if (branches.first ) {
2757+ branches.first ->lastBrConfidently = true ;
2758+ }
2759+ if (branches.second ) {
2760+ branches.second ->lastBrConfidently = true ;
2761+ }
27582762 }
27592763
27602764 // NOTE: There is a hidden dependency here, markBranchVisited
@@ -4026,11 +4030,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
40264030 if (iIdx >= vt->getNumElements ()) {
40274031 // Out of bounds write
40284032 terminateStateOnProgramError (
4029- state,
4030- new ErrorEvent (locationOf (state),
4031- StateTerminationType::BadVectorAccess,
4032- " Out of bounds write when inserting element" ),
4033- StateTerminationConfidenceCategory::CONFIDENT);
4033+ state, new ErrorEvent (locationOf (state),
4034+ StateTerminationType::BadVectorAccess,
4035+ StateTerminationConfidenceCategory::CONFIDENT,
4036+ " Out of bounds write when inserting element" ));
40344037 return ;
40354038 }
40364039
@@ -4071,11 +4074,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
40714074 if (iIdx >= vt->getNumElements ()) {
40724075 // Out of bounds read
40734076 terminateStateOnProgramError (
4074- state,
4075- new ErrorEvent (locationOf (state),
4076- StateTerminationType::BadVectorAccess,
4077- " Out of bounds read when extracting element" ),
4078- StateTerminationConfidenceCategory::CONFIDENT);
4077+ state, new ErrorEvent (locationOf (state),
4078+ StateTerminationType::BadVectorAccess,
4079+ StateTerminationConfidenceCategory::CONFIDENT,
4080+ " Out of bounds read when extracting element" ));
40794081 return ;
40804082 }
40814083
@@ -4979,8 +4981,9 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
49794981 terminationType = StateTerminationType::User;
49804982 }
49814983 terminateStateOnProgramError (
4982- state, new ErrorEvent (locationOf (state), terminationType, messaget),
4983- StateTerminationConfidenceCategory::CONFIDENT);
4984+ state,
4985+ new ErrorEvent (locationOf (state), terminationType,
4986+ StateTerminationConfidenceCategory::CONFIDENT, messaget));
49844987}
49854988
49864989void Executor::terminateStateOnError (
@@ -5063,10 +5066,10 @@ void Executor::terminateStateOnExecError(ExecutionState &state,
50635066 StateTerminationConfidenceCategory::CONFIDENT, " " );
50645067}
50655068
5066- void Executor::terminateStateOnProgramError (
5067- ExecutionState &state, const ref<ErrorEvent> &reason,
5068- StateTerminationConfidenceCategory confidence, const llvm::Twine &info,
5069- const char *suffix) {
5069+ void Executor::terminateStateOnProgramError (ExecutionState &state,
5070+ const ref<ErrorEvent> &reason,
5071+ const llvm::Twine &info,
5072+ const char *suffix) {
50705073 assert (reason->ruleID > StateTerminationType::SOLVERERR &&
50715074 reason->ruleID <= StateTerminationType::PROGERR);
50725075 ++stats::terminationProgramError;
@@ -5085,8 +5088,8 @@ void Executor::terminateStateOnProgramError(
50855088 }
50865089 state.eventsRecorder .record (reason);
50875090
5088- terminateStateOnError (state, reason->message , reason->ruleID , confidence,
5089- info, suffix);
5091+ terminateStateOnError (state, reason->message , reason->ruleID ,
5092+ reason-> confidence , info, suffix);
50905093}
50915094
50925095void Executor::terminateStateOnSolverError (ExecutionState &state,
@@ -5300,6 +5303,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
53005303 e->getWidth () == Context::get ().getPointerWidth ()) {
53015304 ref<Expr> symExternCallsCanReturnNullExpr =
53025305 makeMockValue (state, " symExternCallsCanReturnNull" , Expr::Bool);
5306+ state.nullPointerMarkers .push_back (symExternCallsCanReturnNullExpr);
53035307 e = SelectExpr::create (
53045308 symExternCallsCanReturnNullExpr,
53055309 ConstantExpr::alloc (0 , Context::get ().getPointerWidth ()), e);
@@ -5425,7 +5429,7 @@ void Executor::executeAlloc(ExecutionState &state, ref<Expr> size, bool isLocal,
54255429 makeMockValue (state, " symCheckOutOfMemory" , Expr::Bool);
54265430 address = SelectExpr::create (symCheckOutOfMemoryExpr,
54275431 Expr::createPointer (0 ), address);
5428- state.outOfMemoryMarkers .push_back (symCheckOutOfMemoryExpr);
5432+ state.nullPointerMarkers .push_back (symCheckOutOfMemoryExpr);
54295433 }
54305434
54315435 // state.addPointerResolution(address, mo);
@@ -5471,9 +5475,10 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
54715475 *it->second ,
54725476 new ErrorEvent (new AllocEvent (mo->allocSite ),
54735477 locationOf (*it->second ), StateTerminationType::Free,
5478+ rl.size () != 1
5479+ ? StateTerminationConfidenceCategory::PROBABLY
5480+ : StateTerminationConfidenceCategory::CONFIDENT,
54745481 " free of alloca" ),
5475- rl.size () != 1 ? StateTerminationConfidenceCategory::PROBABLY
5476- : StateTerminationConfidenceCategory::CONFIDENT,
54775482 getAddressInfo (*it->second , address));
54785483 } else if (mo->isGlobal ) {
54795484 if (rl.size () != 1 ) {
@@ -5483,9 +5488,10 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
54835488 *it->second ,
54845489 new ErrorEvent (new AllocEvent (mo->allocSite ),
54855490 locationOf (*it->second ), StateTerminationType::Free,
5491+ rl.size () != 1
5492+ ? StateTerminationConfidenceCategory::PROBABLY
5493+ : StateTerminationConfidenceCategory::CONFIDENT,
54865494 " free of global" ),
5487- rl.size () != 1 ? StateTerminationConfidenceCategory::PROBABLY
5488- : StateTerminationConfidenceCategory::CONFIDENT,
54895495 getAddressInfo (*it->second , address));
54905496 } else {
54915497 it->second ->removePointerResolutions (mo);
@@ -5508,12 +5514,12 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55085514
55095515 // If there are no markers on `malloc` returning nullptr,
55105516 // then `confidence` depends on presence of `unbound` state.
5511- if (!bound->outOfMemoryMarkers .empty ()) {
5517+ if (!bound->nullPointerMarkers .empty ()) {
55125518 // bound constraints already contain `Expr::createIsZero()`
55135519 std::vector<const Array *> markersArrays;
5514- markersArrays.reserve (bound->outOfMemoryMarkers .size ());
5515- findSymbolicObjects (bound->outOfMemoryMarkers .begin (),
5516- bound->outOfMemoryMarkers .end (), markersArrays);
5520+ markersArrays.reserve (bound->nullPointerMarkers .size ());
5521+ findSymbolicObjects (bound->nullPointerMarkers .begin (),
5522+ bound->nullPointerMarkers .end (), markersArrays);
55175523
55185524 // Do some iterations (2-3) to figure out if error is confident.
55195525 ref<Expr> allExcludedVectorsOfMarkers = Expr::createTrue ();
@@ -5534,8 +5540,8 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55345540 terminateStateOnProgramError (
55355541 *bound,
55365542 new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr,
5537- " memory error: null pointer exception " ) ,
5538- StateTerminationConfidenceCategory::CONFIDENT );
5543+ StateTerminationConfidenceCategory::CONFIDENT ,
5544+ " memory error: null pointer exception " ) );
55395545 convinced = true ;
55405546 break ;
55415547 }
@@ -5550,7 +5556,7 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55505556 // Exclude this combinations of markers
55515557
55525558 ref<Expr> conjExcludedVectorOfMarkers = Expr::createTrue ();
5553- for (ref<Expr> marker : bound->outOfMemoryMarkers ) {
5559+ for (ref<Expr> marker : bound->nullPointerMarkers ) {
55545560 conjExcludedVectorOfMarkers = AndExpr::create (
55555561 conjExcludedVectorOfMarkers,
55565562 EqExpr::create (marker,
@@ -5567,10 +5573,9 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55675573 ReachWithError::MayBeNullPointerException);
55685574
55695575 terminateStateOnProgramError (
5570- *bound,
5571- new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr,
5572- " memory error: null pointer exception" ),
5573- StateTerminationConfidenceCategory::PROBABLY);
5576+ *bound, new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr,
5577+ StateTerminationConfidenceCategory::PROBABLY,
5578+ " memory error: null pointer exception" ));
55745579 }
55755580
55765581 } else {
@@ -5582,10 +5587,10 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55825587 terminateStateOnProgramError (
55835588 *bound,
55845589 new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr,
5585- " memory error: null pointer exception " ),
5586- branches. second != nullptr
5587- ? StateTerminationConfidenceCategory::PROBABLY
5588- : StateTerminationConfidenceCategory::CONFIDENT );
5590+ branches. second != nullptr
5591+ ? StateTerminationConfidenceCategory::PROBABLY
5592+ : StateTerminationConfidenceCategory::CONFIDENT,
5593+ " memory error: null pointer exception " ) );
55895594 }
55905595
55915596 return branches.second ;
@@ -5666,9 +5671,10 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
56665671 terminateStateOnProgramError (
56675672 *unbound,
56685673 new ErrorEvent (locationOf (*unbound), StateTerminationType::Ptr,
5674+ !results.empty ()
5675+ ? StateTerminationConfidenceCategory::PROBABLY
5676+ : StateTerminationConfidenceCategory::CONFIDENT,
56695677 " memory error: invalid pointer: " + name),
5670- !results.empty () ? StateTerminationConfidenceCategory::PROBABLY
5671- : StateTerminationConfidenceCategory::CONFIDENT,
56725678 getAddressInfo (*unbound, address));
56735679 }
56745680 }
@@ -5757,8 +5763,9 @@ void Executor::concretizeSize(ExecutionState &state, ref<Expr> size,
57575763 *hugeSize.second ,
57585764 new ErrorEvent (locationOf (*hugeSize.second ),
57595765 StateTerminationType::Model,
5766+ StateTerminationConfidenceCategory::CONFIDENT,
57605767 " concretized symbolic size" ),
5761- StateTerminationConfidenceCategory::CONFIDENT, info.str ());
5768+ info.str ());
57625769 }
57635770 }
57645771 }
@@ -6475,8 +6482,8 @@ void Executor::executeMemoryOperation(
64756482 *state,
64766483 new ErrorEvent (new AllocEvent (mo->allocSite ), locationOf (*state),
64776484 StateTerminationType::ReadOnly,
6478- " memory error: object read only " ) ,
6479- StateTerminationConfidenceCategory::CONFIDENT );
6485+ StateTerminationConfidenceCategory::CONFIDENT ,
6486+ " memory error: object read only " ) );
64806487 } else {
64816488 wos->write (mo->getOffsetExpr (address), value);
64826489 }
@@ -6606,13 +6613,13 @@ void Executor::executeMemoryOperation(
66066613 assert (branches.first );
66076614 terminateStateOnProgramError (
66086615 *branches.first ,
6609- new ErrorEvent (new AllocEvent (mo-> allocSite ),
6610- locationOf (*branches.first ),
6611- StateTerminationType::ReadOnly,
6612- " memory error: object read only " ),
6613- mayBeFalsePositive
6614- ? StateTerminationConfidenceCategory::PROBABLY
6615- : StateTerminationConfidenceCategory::CONFIDENT );
6616+ new ErrorEvent (
6617+ new AllocEvent (mo-> allocSite ), locationOf (*branches.first ),
6618+ StateTerminationType::ReadOnly,
6619+ mayBeFalsePositive
6620+ ? StateTerminationConfidenceCategory::PROBABLY
6621+ : StateTerminationConfidenceCategory::CONFIDENT,
6622+ " memory error: object read only " ) );
66166623 state = branches.second ;
66176624 } else {
66186625 ref<Expr> result = SelectExpr::create (
@@ -6681,13 +6688,13 @@ void Executor::executeMemoryOperation(
66816688 ConstantExpr::alloc (size, Context::get ().getPointerWidth ()), true );
66826689 if (wos->readOnly ) {
66836690 terminateStateOnProgramError (
6684- *bound,
6685- new ErrorEvent ( new AllocEvent (mo->allocSite ), locationOf (*bound),
6686- StateTerminationType::ReadOnly,
6687- " memory error: object read only " ),
6688- mayBeFalsePositive
6689- ? StateTerminationConfidenceCategory::PROBABLY
6690- : StateTerminationConfidenceCategory::CONFIDENT );
6691+ *bound, new ErrorEvent (
6692+ new AllocEvent (mo->allocSite ), locationOf (*bound),
6693+ StateTerminationType::ReadOnly,
6694+ mayBeFalsePositive
6695+ ? StateTerminationConfidenceCategory::PROBABLY
6696+ : StateTerminationConfidenceCategory::CONFIDENT,
6697+ " memory error: object read only " ) );
66916698 } else {
66926699 wos->write (mo->getOffsetExpr (address), value);
66936700 }
@@ -6748,9 +6755,10 @@ void Executor::executeMemoryOperation(
67486755 *unbound,
67496756 new ErrorEvent (new AllocEvent (baseObjectPair.first ->allocSite ),
67506757 locationOf (*unbound), StateTerminationType::Ptr,
6751- " memory error: out of bound pointer " ),
6752- mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6758+ mayBeFalsePositive
6759+ ? StateTerminationConfidenceCategory::PROBABLY
67536760 : StateTerminationConfidenceCategory::CONFIDENT,
6761+ " memory error: out of bound pointer" ),
67546762 getAddressInfo (*unbound, address));
67556763 return ;
67566764 }
@@ -6759,9 +6767,10 @@ void Executor::executeMemoryOperation(
67596767 terminateStateOnProgramError (
67606768 *unbound,
67616769 new ErrorEvent (locationOf (*unbound), StateTerminationType::Ptr,
6762- " memory error: out of bound pointer " ),
6763- mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6770+ mayBeFalsePositive
6771+ ? StateTerminationConfidenceCategory::PROBABLY
67646772 : StateTerminationConfidenceCategory::CONFIDENT,
6773+ " memory error: out of bound pointer" ),
67656774 getAddressInfo (*unbound, address));
67666775 }
67676776}
@@ -7413,21 +7422,25 @@ void Executor::getConstraintLog(const ExecutionState &state, std::string &res,
74137422}
74147423
74157424void Executor::addSARIFReport (const ExecutionState &state) {
7416- ResultJson result{};
7417-
7418- CodeFlowJson codeFlow = state.eventsRecorder .serialize ();
7419-
74207425 if (ref<ErrorEvent> lastEvent =
74217426 llvm::dyn_cast<ErrorEvent>(state.eventsRecorder .last ())) {
7427+
7428+ ResultJson result{};
7429+
7430+ CodeFlowJson codeFlow = state.eventsRecorder .serialize ();
7431+
74227432 result.locations .push_back (lastEvent->serialize ());
74237433 result.message = {Message{lastEvent->message }};
74247434 result.ruleId = {terminationTypeName (lastEvent->ruleID )};
7425- result.level = {" error" };
7426- }
7435+ result.level = {lastEvent->confidence ==
7436+ StateTerminationConfidenceCategory::CONFIDENT
7437+ ? " error"
7438+ : " warning" };
74277439
7428- result.codeFlows .push_back (std::move (codeFlow));
7440+ result.codeFlows .push_back (std::move (codeFlow));
74297441
7430- sarifReport.runs .back ().results .push_back (std::move (result));
7442+ sarifReport.runs .back ().results .push_back (std::move (result));
7443+ }
74317444}
74327445
74337446SarifReportJson Executor::getSARIFReport () const { return sarifReport; }
0 commit comments