@@ -126,12 +126,19 @@ class TerminatorVisitor
126
126
127
127
private:
128
128
TerminatorVisitorRetTy extendFlowCondition (const Expr &Cond) {
129
+ // The terminator sub-expression might not be evaluated.
130
+ if (Env.getValue (Cond) == nullptr )
131
+ transfer (StmtToEnv, Cond, Env);
132
+
129
133
auto *Val = Env.get <BoolValue>(Cond);
130
- // In transferCFGBlock(), we ensure that we always have a `Value` for the
131
- // terminator condition, so assert this.
132
- // We consciously assert ourselves instead of asserting via `cast()` so
133
- // that we get a more meaningful line number if the assertion fails.
134
- assert (Val != nullptr );
134
+ // Value merging depends on flow conditions from different environments
135
+ // being mutually exclusive -- that is, they cannot both be true in their
136
+ // entirety (even if they may share some clauses). So, we need *some* value
137
+ // for the condition expression, even if just an atom.
138
+ if (Val == nullptr ) {
139
+ Val = &Env.makeAtomicBoolValue ();
140
+ Env.setValue (Cond, *Val);
141
+ }
135
142
136
143
bool ConditionValue = true ;
137
144
// The condition must be inverted for the successor that encompasses the
@@ -481,31 +488,6 @@ transferCFGBlock(const CFGBlock &Block, AnalysisContext &AC,
481
488
}
482
489
AC.Log .recordState (State);
483
490
}
484
-
485
- // If we have a terminator, evaluate its condition.
486
- // This `Expr` may not appear as a `CFGElement` anywhere else, and it's
487
- // important that we evaluate it here (rather than while processing the
488
- // terminator) so that we put the corresponding value in the right
489
- // environment.
490
- if (const Expr *TerminatorCond =
491
- dyn_cast_or_null<Expr>(Block.getTerminatorCondition ())) {
492
- if (State.Env .getValue (*TerminatorCond) == nullptr )
493
- // FIXME: This only runs the builtin transfer, not the analysis-specific
494
- // transfer. Fixing this isn't trivial, as the analysis-specific transfer
495
- // takes a `CFGElement` as input, but some expressions only show up as a
496
- // terminator condition, but not as a `CFGElement`. The condition of an if
497
- // statement is one such example.
498
- transfer (StmtToEnvMap (AC.CFCtx , AC.BlockStates ), *TerminatorCond,
499
- State.Env );
500
-
501
- // If the transfer function didn't produce a value, create an atom so that
502
- // we have *some* value for the condition expression. This ensures that
503
- // when we extend the flow condition, it actually changes.
504
- if (State.Env .getValue (*TerminatorCond) == nullptr )
505
- State.Env .setValue (*TerminatorCond, State.Env .makeAtomicBoolValue ());
506
- AC.Log .recordState (State);
507
- }
508
-
509
491
return State;
510
492
}
511
493
0 commit comments