@@ -521,9 +521,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
521
521
InterpreterHandler *ih)
522
522
: Interpreter(opts), interpreterHandler(ih), searcher(nullptr ),
523
523
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()),
527
527
distanceCalculator(new DistanceCalculator(*codeGraphInfo)),
528
528
targetCalculator(new TargetCalculator(*codeGraphInfo)),
529
529
targetManager(new TargetManager(guidanceKind, *distanceCalculator,
@@ -2753,8 +2753,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
2753
2753
branches.first ->lastBrConfidently = false ;
2754
2754
branches.second ->lastBrConfidently = false ;
2755
2755
} 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
+ }
2758
2762
}
2759
2763
2760
2764
// NOTE: There is a hidden dependency here, markBranchVisited
@@ -4026,11 +4030,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
4026
4030
if (iIdx >= vt->getNumElements ()) {
4027
4031
// Out of bounds write
4028
4032
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" ));
4034
4037
return ;
4035
4038
}
4036
4039
@@ -4071,11 +4074,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
4071
4074
if (iIdx >= vt->getNumElements ()) {
4072
4075
// Out of bounds read
4073
4076
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" ));
4079
4081
return ;
4080
4082
}
4081
4083
@@ -4979,8 +4981,9 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
4979
4981
terminationType = StateTerminationType::User;
4980
4982
}
4981
4983
terminateStateOnProgramError (
4982
- state, new ErrorEvent (locationOf (state), terminationType, messaget),
4983
- StateTerminationConfidenceCategory::CONFIDENT);
4984
+ state,
4985
+ new ErrorEvent (locationOf (state), terminationType,
4986
+ StateTerminationConfidenceCategory::CONFIDENT, messaget));
4984
4987
}
4985
4988
4986
4989
void Executor::terminateStateOnError (
@@ -5063,10 +5066,10 @@ void Executor::terminateStateOnExecError(ExecutionState &state,
5063
5066
StateTerminationConfidenceCategory::CONFIDENT, " " );
5064
5067
}
5065
5068
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) {
5070
5073
assert (reason->ruleID > StateTerminationType::SOLVERERR &&
5071
5074
reason->ruleID <= StateTerminationType::PROGERR);
5072
5075
++stats::terminationProgramError;
@@ -5085,8 +5088,8 @@ void Executor::terminateStateOnProgramError(
5085
5088
}
5086
5089
state.eventsRecorder .record (reason);
5087
5090
5088
- terminateStateOnError (state, reason->message , reason->ruleID , confidence,
5089
- info, suffix);
5091
+ terminateStateOnError (state, reason->message , reason->ruleID ,
5092
+ reason-> confidence , info, suffix);
5090
5093
}
5091
5094
5092
5095
void Executor::terminateStateOnSolverError (ExecutionState &state,
@@ -5300,6 +5303,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
5300
5303
e->getWidth () == Context::get ().getPointerWidth ()) {
5301
5304
ref<Expr> symExternCallsCanReturnNullExpr =
5302
5305
makeMockValue (state, " symExternCallsCanReturnNull" , Expr::Bool);
5306
+ state.nullPointerMarkers .push_back (symExternCallsCanReturnNullExpr);
5303
5307
e = SelectExpr::create (
5304
5308
symExternCallsCanReturnNullExpr,
5305
5309
ConstantExpr::alloc (0 , Context::get ().getPointerWidth ()), e);
@@ -5425,7 +5429,7 @@ void Executor::executeAlloc(ExecutionState &state, ref<Expr> size, bool isLocal,
5425
5429
makeMockValue (state, " symCheckOutOfMemory" , Expr::Bool);
5426
5430
address = SelectExpr::create (symCheckOutOfMemoryExpr,
5427
5431
Expr::createPointer (0 ), address);
5428
- state.outOfMemoryMarkers .push_back (symCheckOutOfMemoryExpr);
5432
+ state.nullPointerMarkers .push_back (symCheckOutOfMemoryExpr);
5429
5433
}
5430
5434
5431
5435
// state.addPointerResolution(address, mo);
@@ -5471,9 +5475,10 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
5471
5475
*it->second ,
5472
5476
new ErrorEvent (new AllocEvent (mo->allocSite ),
5473
5477
locationOf (*it->second ), StateTerminationType::Free,
5478
+ rl.size () != 1
5479
+ ? StateTerminationConfidenceCategory::PROBABLY
5480
+ : StateTerminationConfidenceCategory::CONFIDENT,
5474
5481
" free of alloca" ),
5475
- rl.size () != 1 ? StateTerminationConfidenceCategory::PROBABLY
5476
- : StateTerminationConfidenceCategory::CONFIDENT,
5477
5482
getAddressInfo (*it->second , address));
5478
5483
} else if (mo->isGlobal ) {
5479
5484
if (rl.size () != 1 ) {
@@ -5483,9 +5488,10 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
5483
5488
*it->second ,
5484
5489
new ErrorEvent (new AllocEvent (mo->allocSite ),
5485
5490
locationOf (*it->second ), StateTerminationType::Free,
5491
+ rl.size () != 1
5492
+ ? StateTerminationConfidenceCategory::PROBABLY
5493
+ : StateTerminationConfidenceCategory::CONFIDENT,
5486
5494
" free of global" ),
5487
- rl.size () != 1 ? StateTerminationConfidenceCategory::PROBABLY
5488
- : StateTerminationConfidenceCategory::CONFIDENT,
5489
5495
getAddressInfo (*it->second , address));
5490
5496
} else {
5491
5497
it->second ->removePointerResolutions (mo);
@@ -5508,12 +5514,12 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5508
5514
5509
5515
// If there are no markers on `malloc` returning nullptr,
5510
5516
// then `confidence` depends on presence of `unbound` state.
5511
- if (!bound->outOfMemoryMarkers .empty ()) {
5517
+ if (!bound->nullPointerMarkers .empty ()) {
5512
5518
// bound constraints already contain `Expr::createIsZero()`
5513
5519
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);
5517
5523
5518
5524
// Do some iterations (2-3) to figure out if error is confident.
5519
5525
ref<Expr> allExcludedVectorsOfMarkers = Expr::createTrue ();
@@ -5534,8 +5540,8 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5534
5540
terminateStateOnProgramError (
5535
5541
*bound,
5536
5542
new ErrorEvent (locationOf (*bound), StateTerminationType::Ptr ,
5537
- " memory error: null pointer exception " ) ,
5538
- StateTerminationConfidenceCategory::CONFIDENT );
5543
+ StateTerminationConfidenceCategory::CONFIDENT ,
5544
+ " memory error: null pointer exception " ) );
5539
5545
convinced = true ;
5540
5546
break ;
5541
5547
}
@@ -5550,7 +5556,7 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5550
5556
// Exclude this combinations of markers
5551
5557
5552
5558
ref<Expr> conjExcludedVectorOfMarkers = Expr::createTrue ();
5553
- for (ref<Expr> marker : bound->outOfMemoryMarkers ) {
5559
+ for (ref<Expr> marker : bound->nullPointerMarkers ) {
5554
5560
conjExcludedVectorOfMarkers = AndExpr::create (
5555
5561
conjExcludedVectorOfMarkers,
5556
5562
EqExpr::create (marker,
@@ -5567,10 +5573,9 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5567
5573
ReachWithError::MayBeNullPointerException);
5568
5574
5569
5575
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" ));
5574
5579
}
5575
5580
5576
5581
} else {
@@ -5582,10 +5587,10 @@ ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
5582
5587
terminateStateOnProgramError (
5583
5588
*bound,
5584
5589
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 " ) );
5589
5594
}
5590
5595
5591
5596
return branches.second ;
@@ -5666,9 +5671,10 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
5666
5671
terminateStateOnProgramError (
5667
5672
*unbound,
5668
5673
new ErrorEvent (locationOf (*unbound), StateTerminationType::Ptr ,
5674
+ !results.empty ()
5675
+ ? StateTerminationConfidenceCategory::PROBABLY
5676
+ : StateTerminationConfidenceCategory::CONFIDENT,
5669
5677
" memory error: invalid pointer: " + name),
5670
- !results.empty () ? StateTerminationConfidenceCategory::PROBABLY
5671
- : StateTerminationConfidenceCategory::CONFIDENT,
5672
5678
getAddressInfo (*unbound, address));
5673
5679
}
5674
5680
}
@@ -5757,8 +5763,9 @@ void Executor::concretizeSize(ExecutionState &state, ref<Expr> size,
5757
5763
*hugeSize.second ,
5758
5764
new ErrorEvent (locationOf (*hugeSize.second ),
5759
5765
StateTerminationType::Model,
5766
+ StateTerminationConfidenceCategory::CONFIDENT,
5760
5767
" concretized symbolic size" ),
5761
- StateTerminationConfidenceCategory::CONFIDENT, info.str ());
5768
+ info.str ());
5762
5769
}
5763
5770
}
5764
5771
}
@@ -6475,8 +6482,8 @@ void Executor::executeMemoryOperation(
6475
6482
*state,
6476
6483
new ErrorEvent (new AllocEvent (mo->allocSite ), locationOf (*state),
6477
6484
StateTerminationType::ReadOnly,
6478
- " memory error: object read only " ) ,
6479
- StateTerminationConfidenceCategory::CONFIDENT );
6485
+ StateTerminationConfidenceCategory::CONFIDENT ,
6486
+ " memory error: object read only " ) );
6480
6487
} else {
6481
6488
wos->write (mo->getOffsetExpr (address), value);
6482
6489
}
@@ -6606,13 +6613,13 @@ void Executor::executeMemoryOperation(
6606
6613
assert (branches.first );
6607
6614
terminateStateOnProgramError (
6608
6615
*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 " ) );
6616
6623
state = branches.second ;
6617
6624
} else {
6618
6625
ref<Expr> result = SelectExpr::create (
@@ -6681,13 +6688,13 @@ void Executor::executeMemoryOperation(
6681
6688
ConstantExpr::alloc (size, Context::get ().getPointerWidth ()), true );
6682
6689
if (wos->readOnly ) {
6683
6690
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 " ) );
6691
6698
} else {
6692
6699
wos->write (mo->getOffsetExpr (address), value);
6693
6700
}
@@ -6748,9 +6755,10 @@ void Executor::executeMemoryOperation(
6748
6755
*unbound,
6749
6756
new ErrorEvent (new AllocEvent (baseObjectPair.first ->allocSite ),
6750
6757
locationOf (*unbound), StateTerminationType::Ptr ,
6751
- " memory error: out of bound pointer " ),
6752
- mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6758
+ mayBeFalsePositive
6759
+ ? StateTerminationConfidenceCategory::PROBABLY
6753
6760
: StateTerminationConfidenceCategory::CONFIDENT,
6761
+ " memory error: out of bound pointer" ),
6754
6762
getAddressInfo (*unbound, address));
6755
6763
return ;
6756
6764
}
@@ -6759,9 +6767,10 @@ void Executor::executeMemoryOperation(
6759
6767
terminateStateOnProgramError (
6760
6768
*unbound,
6761
6769
new ErrorEvent (locationOf (*unbound), StateTerminationType::Ptr ,
6762
- " memory error: out of bound pointer " ),
6763
- mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6770
+ mayBeFalsePositive
6771
+ ? StateTerminationConfidenceCategory::PROBABLY
6764
6772
: StateTerminationConfidenceCategory::CONFIDENT,
6773
+ " memory error: out of bound pointer" ),
6765
6774
getAddressInfo (*unbound, address));
6766
6775
}
6767
6776
}
@@ -7413,21 +7422,25 @@ void Executor::getConstraintLog(const ExecutionState &state, std::string &res,
7413
7422
}
7414
7423
7415
7424
void Executor::addSARIFReport (const ExecutionState &state) {
7416
- ResultJson result{};
7417
-
7418
- CodeFlowJson codeFlow = state.eventsRecorder .serialize ();
7419
-
7420
7425
if (ref<ErrorEvent> lastEvent =
7421
7426
llvm::dyn_cast<ErrorEvent>(state.eventsRecorder .last ())) {
7427
+
7428
+ ResultJson result{};
7429
+
7430
+ CodeFlowJson codeFlow = state.eventsRecorder .serialize ();
7431
+
7422
7432
result.locations .push_back (lastEvent->serialize ());
7423
7433
result.message = {Message{lastEvent->message }};
7424
7434
result.ruleId = {terminationTypeName (lastEvent->ruleID )};
7425
- result.level = {" error" };
7426
- }
7435
+ result.level = {lastEvent->confidence ==
7436
+ StateTerminationConfidenceCategory::CONFIDENT
7437
+ ? " error"
7438
+ : " warning" };
7427
7439
7428
- result.codeFlows .push_back (std::move (codeFlow));
7440
+ result.codeFlows .push_back (std::move (codeFlow));
7429
7441
7430
- sarifReport.runs .back ().results .push_back (std::move (result));
7442
+ sarifReport.runs .back ().results .push_back (std::move (result));
7443
+ }
7431
7444
}
7432
7445
7433
7446
SarifReportJson Executor::getSARIFReport () const { return sarifReport; }
0 commit comments