@@ -2749,8 +2749,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
27492749 branches.first ->lastBrConfidently = false ;
27502750 branches.second ->lastBrConfidently = false ;
27512751 } else {
2752- (branches.first ? branches.first : branches.second )->lastBrConfidently =
2753- true ;
2752+ if (branches.first ) {
2753+ branches.first ->lastBrConfidently = true ;
2754+ }
2755+ if (branches.second ) {
2756+ branches.second ->lastBrConfidently = true ;
2757+ }
27542758 }
27552759
27562760 // NOTE: There is a hidden dependency here, markBranchVisited
@@ -4022,11 +4026,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
40224026 if (iIdx >= vt->getNumElements ()) {
40234027 // Out of bounds write
40244028 terminateStateOnProgramError (
4025- state,
4026- new ErrorEvent (locationOf (state),
4027- StateTerminationType::BadVectorAccess,
4028- " Out of bounds write when inserting element" ),
4029- StateTerminationConfidenceCategory::CONFIDENT);
4029+ state, new ErrorEvent (locationOf (state),
4030+ StateTerminationType::BadVectorAccess,
4031+ StateTerminationConfidenceCategory::CONFIDENT,
4032+ " Out of bounds write when inserting element" ));
40304033 return ;
40314034 }
40324035
@@ -4067,11 +4070,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
40674070 if (iIdx >= vt->getNumElements ()) {
40684071 // Out of bounds read
40694072 terminateStateOnProgramError (
4070- state,
4071- new ErrorEvent (locationOf (state),
4072- StateTerminationType::BadVectorAccess,
4073- " Out of bounds read when extracting element" ),
4074- StateTerminationConfidenceCategory::CONFIDENT);
4073+ state, new ErrorEvent (locationOf (state),
4074+ StateTerminationType::BadVectorAccess,
4075+ StateTerminationConfidenceCategory::CONFIDENT,
4076+ " Out of bounds read when extracting element" ));
40754077 return ;
40764078 }
40774079
@@ -4975,8 +4977,9 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
49754977 terminationType = StateTerminationType::User;
49764978 }
49774979 terminateStateOnProgramError (
4978- state, new ErrorEvent (locationOf (state), terminationType, messaget),
4979- StateTerminationConfidenceCategory::CONFIDENT);
4980+ state,
4981+ new ErrorEvent (locationOf (state), terminationType,
4982+ StateTerminationConfidenceCategory::CONFIDENT, messaget));
49804983}
49814984
49824985void Executor::terminateStateOnError (
@@ -5059,10 +5062,10 @@ void Executor::terminateStateOnExecError(ExecutionState &state,
50595062 StateTerminationConfidenceCategory::CONFIDENT, " " );
50605063}
50615064
5062- void Executor::terminateStateOnProgramError (
5063- ExecutionState &state, const ref<ErrorEvent> &reason,
5064- StateTerminationConfidenceCategory confidence, const llvm::Twine &info,
5065- const char *suffix) {
5065+ void Executor::terminateStateOnProgramError (ExecutionState &state,
5066+ const ref<ErrorEvent> &reason,
5067+ const llvm::Twine &info,
5068+ const char *suffix) {
50665069 assert (reason->ruleID > StateTerminationType::SOLVERERR &&
50675070 reason->ruleID <= StateTerminationType::PROGERR);
50685071 ++stats::terminationProgramError;
@@ -5081,8 +5084,8 @@ void Executor::terminateStateOnProgramError(
50815084 }
50825085 state.eventsRecorder .record (reason);
50835086
5084- terminateStateOnError (state, reason->message , reason->ruleID , confidence,
5085- info, suffix);
5087+ terminateStateOnError (state, reason->message , reason->ruleID ,
5088+ reason-> confidence , info, suffix);
50865089}
50875090
50885091void Executor::terminateStateOnSolverError (ExecutionState &state,
@@ -5274,6 +5277,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
52745277 e->getWidth () == Context::get ().getPointerWidth ()) {
52755278 ref<Expr> symExternCallsCanReturnNullExpr =
52765279 makeMockValue (state, " symExternCallsCanReturnNull" , Expr::Bool);
5280+ state.nullPointerMarkers .push_back (symExternCallsCanReturnNullExpr);
52775281 e = SelectExpr::create (
52785282 symExternCallsCanReturnNullExpr,
52795283 ConstantExpr::alloc (0 , Context::get ().getPointerWidth ()), e);
@@ -5399,7 +5403,7 @@ void Executor::executeAlloc(ExecutionState &state, ref<Expr> size, bool isLocal,
53995403 makeMockValue (state, " symCheckOutOfMemory" , Expr::Bool);
54005404 address = SelectExpr::create (symCheckOutOfMemoryExpr,
54015405 Expr::createPointer (0 ), address);
5402- state.outOfMemoryMarkers .push_back (symCheckOutOfMemoryExpr);
5406+ state.nullPointerMarkers .push_back (symCheckOutOfMemoryExpr);
54035407 }
54045408
54055409 // state.addPointerResolution(address, mo);
@@ -5445,9 +5449,10 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
54455449 *it->second ,
54465450 new ErrorEvent (new AllocEvent (mo->allocSite ),
54475451 locationOf (*it->second ), StateTerminationType::Free,
5452+ rl.size () != 1
5453+ ? StateTerminationConfidenceCategory::PROBABLY
5454+ : StateTerminationConfidenceCategory::CONFIDENT,
54485455 " free of alloca" ),
5449- rl.size () != 1 ? StateTerminationConfidenceCategory::PROBABLY
5450- : StateTerminationConfidenceCategory::CONFIDENT,
54515456 getAddressInfo (*it->second , address));
54525457 } else if (mo->isGlobal ) {
54535458 if (rl.size () != 1 ) {
@@ -5457,9 +5462,10 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
54575462 *it->second ,
54585463 new ErrorEvent (new AllocEvent (mo->allocSite ),
54595464 locationOf (*it->second ), StateTerminationType::Free,
5465+ rl.size () != 1
5466+ ? StateTerminationConfidenceCategory::PROBABLY
5467+ : StateTerminationConfidenceCategory::CONFIDENT,
54605468 " free of global" ),
5461- rl.size () != 1 ? StateTerminationConfidenceCategory::PROBABLY
5462- : StateTerminationConfidenceCategory::CONFIDENT,
54635469 getAddressInfo (*it->second , address));
54645470 } else {
54655471 it->second ->removePointerResolutions (mo);
@@ -5482,12 +5488,12 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
54825488
54835489 // If there are no markers on `malloc` returning nullptr,
54845490 // then `confidence` depends on presence of `unbound` state.
5485- if (!bound->outOfMemoryMarkers .empty ()) {
5491+ if (!bound->nullPointerMarkers .empty ()) {
54865492 // bound constraints already contain `Expr::createIsZero()`
54875493 std::vector<const Array *> markersArrays;
5488- markersArrays.reserve (bound->outOfMemoryMarkers .size ());
5489- findSymbolicObjects (bound->outOfMemoryMarkers .begin (),
5490- bound->outOfMemoryMarkers .end (), markersArrays);
5494+ markersArrays.reserve (bound->nullPointerMarkers .size ());
5495+ findSymbolicObjects (bound->nullPointerMarkers .begin (),
5496+ bound->nullPointerMarkers .end (), markersArrays);
54915497
54925498 // Do some iterations (2-3) to figure out if error is confident.
54935499 ref<Expr> allExcludedVectorsOfMarkers = Expr::createTrue ();
@@ -5508,8 +5514,8 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55085514 terminateStateOnProgramError (
55095515 *bound,
55105516 new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr,
5511- " memory error: null pointer exception " ) ,
5512- StateTerminationConfidenceCategory::CONFIDENT );
5517+ StateTerminationConfidenceCategory::CONFIDENT ,
5518+ " memory error: null pointer exception " ) );
55135519 convinced = true ;
55145520 break ;
55155521 }
@@ -5524,7 +5530,7 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55245530 // Exclude this combinations of markers
55255531
55265532 ref<Expr> conjExcludedVectorOfMarkers = Expr::createTrue ();
5527- for (ref<Expr> marker : bound->outOfMemoryMarkers ) {
5533+ for (ref<Expr> marker : bound->nullPointerMarkers ) {
55285534 conjExcludedVectorOfMarkers = AndExpr::create (
55295535 conjExcludedVectorOfMarkers,
55305536 EqExpr::create (marker,
@@ -5541,10 +5547,9 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55415547 ReachWithError::MayBeNullPointerException);
55425548
55435549 terminateStateOnProgramError (
5544- *bound,
5545- new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr,
5546- " memory error: null pointer exception" ),
5547- StateTerminationConfidenceCategory::PROBABLY);
5550+ *bound, new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr,
5551+ StateTerminationConfidenceCategory::PROBABLY,
5552+ " memory error: null pointer exception" ));
55485553 }
55495554
55505555 } else {
@@ -5556,10 +5561,10 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
55565561 terminateStateOnProgramError (
55575562 *bound,
55585563 new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr,
5559- " memory error: null pointer exception " ),
5560- branches. second != nullptr
5561- ? StateTerminationConfidenceCategory::PROBABLY
5562- : StateTerminationConfidenceCategory::CONFIDENT );
5564+ branches. second != nullptr
5565+ ? StateTerminationConfidenceCategory::PROBABLY
5566+ : StateTerminationConfidenceCategory::CONFIDENT,
5567+ " memory error: null pointer exception " ) );
55635568 }
55645569
55655570 return branches.second ;
@@ -5640,9 +5645,10 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
56405645 terminateStateOnProgramError (
56415646 *unbound,
56425647 new ErrorEvent (locationOf (*unbound), StateTerminationType::Ptr,
5648+ !results.empty ()
5649+ ? StateTerminationConfidenceCategory::PROBABLY
5650+ : StateTerminationConfidenceCategory::CONFIDENT,
56435651 " memory error: invalid pointer: " + name),
5644- !results.empty () ? StateTerminationConfidenceCategory::PROBABLY
5645- : StateTerminationConfidenceCategory::CONFIDENT,
56465652 getAddressInfo (*unbound, address));
56475653 }
56485654 }
@@ -5731,8 +5737,9 @@ void Executor::concretizeSize(ExecutionState &state, ref<Expr> size,
57315737 *hugeSize.second ,
57325738 new ErrorEvent (locationOf (*hugeSize.second ),
57335739 StateTerminationType::Model,
5740+ StateTerminationConfidenceCategory::CONFIDENT,
57345741 " concretized symbolic size" ),
5735- StateTerminationConfidenceCategory::CONFIDENT, info.str ());
5742+ info.str ());
57365743 }
57375744 }
57385745 }
@@ -6425,8 +6432,8 @@ void Executor::executeMemoryOperation(
64256432 *state,
64266433 new ErrorEvent (new AllocEvent (mo->allocSite ), locationOf (*state),
64276434 StateTerminationType::ReadOnly,
6428- " memory error: object read only " ) ,
6429- StateTerminationConfidenceCategory::CONFIDENT );
6435+ StateTerminationConfidenceCategory::CONFIDENT ,
6436+ " memory error: object read only " ) );
64306437 } else {
64316438 wos->write (mo->getOffsetExpr (address), value);
64326439 }
@@ -6546,13 +6553,13 @@ void Executor::executeMemoryOperation(
65466553 assert (branches.first );
65476554 terminateStateOnProgramError (
65486555 *branches.first ,
6549- new ErrorEvent (new AllocEvent (mo-> allocSite ),
6550- locationOf (*branches.first ),
6551- StateTerminationType::ReadOnly,
6552- " memory error: object read only " ),
6553- mayBeFalsePositive
6554- ? StateTerminationConfidenceCategory::PROBABLY
6555- : StateTerminationConfidenceCategory::CONFIDENT );
6556+ new ErrorEvent (
6557+ new AllocEvent (mo-> allocSite ), locationOf (*branches.first ),
6558+ StateTerminationType::ReadOnly,
6559+ mayBeFalsePositive
6560+ ? StateTerminationConfidenceCategory::PROBABLY
6561+ : StateTerminationConfidenceCategory::CONFIDENT,
6562+ " memory error: object read only " ) );
65566563 state = branches.second ;
65576564 } else {
65586565 ref<Expr> result = SelectExpr::create (
@@ -6621,13 +6628,13 @@ void Executor::executeMemoryOperation(
66216628 ConstantExpr::alloc (size, Context::get ().getPointerWidth ()), true );
66226629 if (wos->readOnly ) {
66236630 terminateStateOnProgramError (
6624- *bound,
6625- new ErrorEvent ( new AllocEvent (mo->allocSite ), locationOf (*bound),
6626- StateTerminationType::ReadOnly,
6627- " memory error: object read only " ),
6628- mayBeFalsePositive
6629- ? StateTerminationConfidenceCategory::PROBABLY
6630- : StateTerminationConfidenceCategory::CONFIDENT );
6631+ *bound, new ErrorEvent (
6632+ new AllocEvent (mo->allocSite ), locationOf (*bound),
6633+ StateTerminationType::ReadOnly,
6634+ mayBeFalsePositive
6635+ ? StateTerminationConfidenceCategory::PROBABLY
6636+ : StateTerminationConfidenceCategory::CONFIDENT,
6637+ " memory error: object read only " ) );
66316638 } else {
66326639 wos->write (mo->getOffsetExpr (address), value);
66336640 }
@@ -6678,9 +6685,10 @@ void Executor::executeMemoryOperation(
66786685 *unbound,
66796686 new ErrorEvent (new AllocEvent (baseObjectPair.first ->allocSite ),
66806687 locationOf (*unbound), StateTerminationType::Ptr,
6681- " memory error: out of bound pointer " ),
6682- mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6688+ mayBeFalsePositive
6689+ ? StateTerminationConfidenceCategory::PROBABLY
66836690 : StateTerminationConfidenceCategory::CONFIDENT,
6691+ " memory error: out of bound pointer" ),
66846692 getAddressInfo (*unbound, address));
66856693 return ;
66866694 }
@@ -6689,9 +6697,10 @@ void Executor::executeMemoryOperation(
66896697 terminateStateOnProgramError (
66906698 *unbound,
66916699 new ErrorEvent (locationOf (*unbound), StateTerminationType::Ptr,
6692- " memory error: out of bound pointer " ),
6693- mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6700+ mayBeFalsePositive
6701+ ? StateTerminationConfidenceCategory::PROBABLY
66946702 : StateTerminationConfidenceCategory::CONFIDENT,
6703+ " memory error: out of bound pointer" ),
66956704 getAddressInfo (*unbound, address));
66966705 }
66976706}
@@ -7343,21 +7352,25 @@ void Executor::getConstraintLog(const ExecutionState &state, std::string &res,
73437352}
73447353
73457354void Executor::addSARIFReport (const ExecutionState &state) {
7346- ResultJson result{};
7347-
7348- CodeFlowJson codeFlow = state.eventsRecorder .serialize ();
7349-
73507355 if (ref<ErrorEvent> lastEvent =
73517356 llvm::dyn_cast<ErrorEvent>(state.eventsRecorder .last ())) {
7357+
7358+ ResultJson result{};
7359+
7360+ CodeFlowJson codeFlow = state.eventsRecorder .serialize ();
7361+
73527362 result.locations .push_back (lastEvent->serialize ());
73537363 result.message = {Message{lastEvent->message }};
73547364 result.ruleId = {terminationTypeName (lastEvent->ruleID )};
7355- result.level = {" error" };
7356- }
7365+ result.level = {lastEvent->confidence ==
7366+ StateTerminationConfidenceCategory::CONFIDENT
7367+ ? " error"
7368+ : " warning" };
73577369
7358- result.codeFlows .push_back (std::move (codeFlow));
7370+ result.codeFlows .push_back (std::move (codeFlow));
73597371
7360- sarifReport.runs .back ().results .push_back (std::move (result));
7372+ sarifReport.runs .back ().results .push_back (std::move (result));
7373+ }
73617374}
73627375
73637376SarifReportJson Executor::getSARIFReport () const { return sarifReport; }
0 commit comments