@@ -2749,8 +2749,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
2749
2749
branches.first ->lastBrConfidently = false ;
2750
2750
branches.second ->lastBrConfidently = false ;
2751
2751
} 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
+ }
2754
2758
}
2755
2759
2756
2760
// NOTE: There is a hidden dependency here, markBranchVisited
@@ -4022,11 +4026,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
4022
4026
if (iIdx >= vt->getNumElements ()) {
4023
4027
// Out of bounds write
4024
4028
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" ));
4030
4033
return ;
4031
4034
}
4032
4035
@@ -4067,11 +4070,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
4067
4070
if (iIdx >= vt->getNumElements ()) {
4068
4071
// Out of bounds read
4069
4072
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" ));
4075
4077
return ;
4076
4078
}
4077
4079
@@ -4975,8 +4977,9 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
4975
4977
terminationType = StateTerminationType::User;
4976
4978
}
4977
4979
terminateStateOnProgramError (
4978
- state, new ErrorEvent (locationOf (state), terminationType, messaget),
4979
- StateTerminationConfidenceCategory::CONFIDENT);
4980
+ state,
4981
+ new ErrorEvent (locationOf (state), terminationType,
4982
+ StateTerminationConfidenceCategory::CONFIDENT, messaget));
4980
4983
}
4981
4984
4982
4985
void Executor::terminateStateOnError (
@@ -5059,10 +5062,10 @@ void Executor::terminateStateOnExecError(ExecutionState &state,
5059
5062
StateTerminationConfidenceCategory::CONFIDENT, " " );
5060
5063
}
5061
5064
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) {
5066
5069
assert (reason->ruleID > StateTerminationType::SOLVERERR &&
5067
5070
reason->ruleID <= StateTerminationType::PROGERR);
5068
5071
++stats::terminationProgramError;
@@ -5081,8 +5084,8 @@ void Executor::terminateStateOnProgramError(
5081
5084
}
5082
5085
state.eventsRecorder .record (reason);
5083
5086
5084
- terminateStateOnError (state, reason->message , reason->ruleID , confidence,
5085
- info, suffix);
5087
+ terminateStateOnError (state, reason->message , reason->ruleID ,
5088
+ reason-> confidence , info, suffix);
5086
5089
}
5087
5090
5088
5091
void Executor::terminateStateOnSolverError (ExecutionState &state,
@@ -5274,6 +5277,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
5274
5277
e->getWidth () == Context::get ().getPointerWidth ()) {
5275
5278
ref<Expr> symExternCallsCanReturnNullExpr =
5276
5279
makeMockValue (state, " symExternCallsCanReturnNull" , Expr::Bool);
5280
+ state.nullPointerMarkers .push_back (symExternCallsCanReturnNullExpr);
5277
5281
e = SelectExpr::create (
5278
5282
symExternCallsCanReturnNullExpr,
5279
5283
ConstantExpr::alloc (0 , Context::get ().getPointerWidth ()), e);
@@ -5399,7 +5403,7 @@ void Executor::executeAlloc(ExecutionState &state, ref<Expr> size, bool isLocal,
5399
5403
makeMockValue (state, " symCheckOutOfMemory" , Expr::Bool);
5400
5404
address = SelectExpr::create (symCheckOutOfMemoryExpr,
5401
5405
Expr::createPointer (0 ), address);
5402
- state.outOfMemoryMarkers .push_back (symCheckOutOfMemoryExpr);
5406
+ state.nullPointerMarkers .push_back (symCheckOutOfMemoryExpr);
5403
5407
}
5404
5408
5405
5409
// state.addPointerResolution(address, mo);
@@ -5445,9 +5449,10 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
5445
5449
*it->second ,
5446
5450
new ErrorEvent (new AllocEvent (mo->allocSite ),
5447
5451
locationOf (*it->second ), StateTerminationType::Free,
5452
+ rl.size () != 1
5453
+ ? StateTerminationConfidenceCategory::PROBABLY
5454
+ : StateTerminationConfidenceCategory::CONFIDENT,
5448
5455
" free of alloca" ),
5449
- rl.size () != 1 ? StateTerminationConfidenceCategory::PROBABLY
5450
- : StateTerminationConfidenceCategory::CONFIDENT,
5451
5456
getAddressInfo (*it->second , address));
5452
5457
} else if (mo->isGlobal ) {
5453
5458
if (rl.size () != 1 ) {
@@ -5457,9 +5462,10 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
5457
5462
*it->second ,
5458
5463
new ErrorEvent (new AllocEvent (mo->allocSite ),
5459
5464
locationOf (*it->second ), StateTerminationType::Free,
5465
+ rl.size () != 1
5466
+ ? StateTerminationConfidenceCategory::PROBABLY
5467
+ : StateTerminationConfidenceCategory::CONFIDENT,
5460
5468
" free of global" ),
5461
- rl.size () != 1 ? StateTerminationConfidenceCategory::PROBABLY
5462
- : StateTerminationConfidenceCategory::CONFIDENT,
5463
5469
getAddressInfo (*it->second , address));
5464
5470
} else {
5465
5471
it->second ->removePointerResolutions (mo);
@@ -5482,12 +5488,12 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5482
5488
5483
5489
// If there are no markers on `malloc` returning nullptr,
5484
5490
// then `confidence` depends on presence of `unbound` state.
5485
- if (!bound->outOfMemoryMarkers .empty ()) {
5491
+ if (!bound->nullPointerMarkers .empty ()) {
5486
5492
// bound constraints already contain `Expr::createIsZero()`
5487
5493
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);
5491
5497
5492
5498
// Do some iterations (2-3) to figure out if error is confident.
5493
5499
ref<Expr> allExcludedVectorsOfMarkers = Expr::createTrue ();
@@ -5508,8 +5514,8 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5508
5514
terminateStateOnProgramError (
5509
5515
*bound,
5510
5516
new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr ,
5511
- " memory error: null pointer exception " ) ,
5512
- StateTerminationConfidenceCategory::CONFIDENT );
5517
+ StateTerminationConfidenceCategory::CONFIDENT ,
5518
+ " memory error: null pointer exception " ) );
5513
5519
convinced = true ;
5514
5520
break ;
5515
5521
}
@@ -5524,7 +5530,7 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5524
5530
// Exclude this combinations of markers
5525
5531
5526
5532
ref<Expr> conjExcludedVectorOfMarkers = Expr::createTrue ();
5527
- for (ref<Expr> marker : bound->outOfMemoryMarkers ) {
5533
+ for (ref<Expr> marker : bound->nullPointerMarkers ) {
5528
5534
conjExcludedVectorOfMarkers = AndExpr::create (
5529
5535
conjExcludedVectorOfMarkers,
5530
5536
EqExpr::create (marker,
@@ -5541,10 +5547,9 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5541
5547
ReachWithError::MayBeNullPointerException);
5542
5548
5543
5549
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" ));
5548
5553
}
5549
5554
5550
5555
} else {
@@ -5556,10 +5561,10 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5556
5561
terminateStateOnProgramError (
5557
5562
*bound,
5558
5563
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 " ) );
5563
5568
}
5564
5569
5565
5570
return branches.second ;
@@ -5640,9 +5645,10 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
5640
5645
terminateStateOnProgramError (
5641
5646
*unbound,
5642
5647
new ErrorEvent (locationOf (*unbound), StateTerminationType::Ptr ,
5648
+ !results.empty ()
5649
+ ? StateTerminationConfidenceCategory::PROBABLY
5650
+ : StateTerminationConfidenceCategory::CONFIDENT,
5643
5651
" memory error: invalid pointer: " + name),
5644
- !results.empty () ? StateTerminationConfidenceCategory::PROBABLY
5645
- : StateTerminationConfidenceCategory::CONFIDENT,
5646
5652
getAddressInfo (*unbound, address));
5647
5653
}
5648
5654
}
@@ -5731,8 +5737,9 @@ void Executor::concretizeSize(ExecutionState &state, ref<Expr> size,
5731
5737
*hugeSize.second ,
5732
5738
new ErrorEvent (locationOf (*hugeSize.second ),
5733
5739
StateTerminationType::Model,
5740
+ StateTerminationConfidenceCategory::CONFIDENT,
5734
5741
" concretized symbolic size" ),
5735
- StateTerminationConfidenceCategory::CONFIDENT, info.str ());
5742
+ info.str ());
5736
5743
}
5737
5744
}
5738
5745
}
@@ -6425,8 +6432,8 @@ void Executor::executeMemoryOperation(
6425
6432
*state,
6426
6433
new ErrorEvent (new AllocEvent (mo->allocSite ), locationOf (*state),
6427
6434
StateTerminationType::ReadOnly,
6428
- " memory error: object read only " ) ,
6429
- StateTerminationConfidenceCategory::CONFIDENT );
6435
+ StateTerminationConfidenceCategory::CONFIDENT ,
6436
+ " memory error: object read only " ) );
6430
6437
} else {
6431
6438
wos->write (mo->getOffsetExpr (address), value);
6432
6439
}
@@ -6546,13 +6553,13 @@ void Executor::executeMemoryOperation(
6546
6553
assert (branches.first );
6547
6554
terminateStateOnProgramError (
6548
6555
*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 " ) );
6556
6563
state = branches.second ;
6557
6564
} else {
6558
6565
ref<Expr> result = SelectExpr::create (
@@ -6621,13 +6628,13 @@ void Executor::executeMemoryOperation(
6621
6628
ConstantExpr::alloc (size, Context::get ().getPointerWidth ()), true );
6622
6629
if (wos->readOnly ) {
6623
6630
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 " ) );
6631
6638
} else {
6632
6639
wos->write (mo->getOffsetExpr (address), value);
6633
6640
}
@@ -6678,9 +6685,10 @@ void Executor::executeMemoryOperation(
6678
6685
*unbound,
6679
6686
new ErrorEvent (new AllocEvent (baseObjectPair.first ->allocSite ),
6680
6687
locationOf (*unbound), StateTerminationType::Ptr ,
6681
- " memory error: out of bound pointer " ),
6682
- mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6688
+ mayBeFalsePositive
6689
+ ? StateTerminationConfidenceCategory::PROBABLY
6683
6690
: StateTerminationConfidenceCategory::CONFIDENT,
6691
+ " memory error: out of bound pointer" ),
6684
6692
getAddressInfo (*unbound, address));
6685
6693
return ;
6686
6694
}
@@ -6689,9 +6697,10 @@ void Executor::executeMemoryOperation(
6689
6697
terminateStateOnProgramError (
6690
6698
*unbound,
6691
6699
new ErrorEvent (locationOf (*unbound), StateTerminationType::Ptr ,
6692
- " memory error: out of bound pointer " ),
6693
- mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6700
+ mayBeFalsePositive
6701
+ ? StateTerminationConfidenceCategory::PROBABLY
6694
6702
: StateTerminationConfidenceCategory::CONFIDENT,
6703
+ " memory error: out of bound pointer" ),
6695
6704
getAddressInfo (*unbound, address));
6696
6705
}
6697
6706
}
@@ -7343,21 +7352,25 @@ void Executor::getConstraintLog(const ExecutionState &state, std::string &res,
7343
7352
}
7344
7353
7345
7354
void Executor::addSARIFReport (const ExecutionState &state) {
7346
- ResultJson result{};
7347
-
7348
- CodeFlowJson codeFlow = state.eventsRecorder .serialize ();
7349
-
7350
7355
if (ref<ErrorEvent> lastEvent =
7351
7356
llvm::dyn_cast<ErrorEvent>(state.eventsRecorder .last ())) {
7357
+
7358
+ ResultJson result{};
7359
+
7360
+ CodeFlowJson codeFlow = state.eventsRecorder .serialize ();
7361
+
7352
7362
result.locations .push_back (lastEvent->serialize ());
7353
7363
result.message = {Message{lastEvent->message }};
7354
7364
result.ruleId = {terminationTypeName (lastEvent->ruleID )};
7355
- result.level = {" error" };
7356
- }
7365
+ result.level = {lastEvent->confidence ==
7366
+ StateTerminationConfidenceCategory::CONFIDENT
7367
+ ? " error"
7368
+ : " warning" };
7357
7369
7358
- result.codeFlows .push_back (std::move (codeFlow));
7370
+ result.codeFlows .push_back (std::move (codeFlow));
7359
7371
7360
- sarifReport.runs .back ().results .push_back (std::move (result));
7372
+ sarifReport.runs .back ().results .push_back (std::move (result));
7373
+ }
7361
7374
}
7362
7375
7363
7376
SarifReportJson Executor::getSARIFReport () const { return sarifReport; }
0 commit comments