[cfe-dev] Several questions about UncheckedReturn statistic Checker

Ted Kremenek kremenek at apple.com
Mon Dec 6 20:27:51 PST 2010


Hi Lei,

I think this is a good first step.  Comments inline.

On Dec 6, 2010, at 5:59 PM, 章磊 wrote:

> Hi clang,
> 
> I'm trying to find out how to implement this statistic checker. IMO, there could be several steps.
> Add a ConjuredSymbol to all the CallExpr in PostVisitCallExpr, set the state to Unchecked.
CallExprs are almost always guaranteed to evaluate to a symbolic value, so you don't need to create a new one.  For example:

+void UncheckedReturnChecker::PostVisitCallExpr(CheckerContext &C, 
+                                               const CallExpr *CE) {
+  unsigned Count = C.getNodeBuilder().getCurrentBlockCount();
+  SValBuilder &svalBuilder = C.getSValBuilder();
+  SymbolRef Sym = svalBuilder.getConjuredSymbolVal(0, CE, Count).getAsSymbol();
+
+  const GRState *state = C.getState();
+
+  // Once we encounter a call expr, set the initial state to Unchecked.
+  state = 
+    state->set<CheckedReturnState>(Sym, CheckedReturnState::getUnchecked(CE));
+
+  C.addTransition(state);
+  return;
+}

Instead of conjuring a new symbol, try querying the SVal for the CallExpr.  If it is a symbol, you can just add it to the GDM.  For example:

const GRState *state = C.getState();
if (SymExpr *sym = state->getSVal(CE)->getAsSymbol()) {
  state = state->set<CheckedReturnState>(sym, CheckReturnState::getUnchecked(CE));
  C.addTransition(state);
}

The nice thing about this approach is that you associate your tracking state with the actual symbol returned by the CallExpr.  That value is then tracked through assignments, etc.

> In VisitBranchCondition, if a callexpr is checked, set the state to checked.
I think this logic looks alright, although it takes a highly syntactic approach instead of reasoning about symbolic values.  One shortcoming of this approach is that it won't handle:

  p = foo();
  bool b = p == NULL;
  if (b) { ... }

It is possible to handle this with a more sophisticated (albeit more complicated analysis) that reasons about symbolic values.  Essentially, 'p == NULL' would evaluate to an SVal for which you could attach tracking state.  Then, in VisitBranchCondition() you only need to reason about the SVal for the condition instead of its raw syntactic form.

> After all the decl was analyzed, do the first part(in a translationunit) of statistic count (and/or check) in AnalysisConsumer::HandleTranslationUnit.
Seems reasonable.
> Implement a script to do the whole project's statistic check.
Seems reasonable.

> This patch try to do the first two steps. 
> 
> I register the checker in RegisterExperimentalChecks, but a new action seems more appropriate. Statistic checkers are some different from the checkers in RegisterExperimentalChecks.

Experimental checks is just a catch-all bucket for checks that are in development, but I agree with you that I think it makes sense to add a new flag for this case.

> 
> In order to generate ExplodedNode but not a blockedge, i add a new "generateNode" function in GRBranchNodeBuilder. I think this function is not quite right. I use poststmt as the ProgramPoint, maybe we need a new ProgramPoint here?

Yes, we'll likely need a new ProgramPoint.  Since the condition is a Stmt*, it will have already been evaluated (with ExplodedNodes with a PostStmt program point).  You might get unintended caching in the ExplodedGraph.

> 
> Beacause this is a really experimental checker and not all the steps are finished, i can't give a testcase to show what i did. 
> 
> More comments inline.

One other nit is that the checker should implement 'evalDeadSymbols()' so that it clears out tracked symbols from the state.  Otherwise we'll get artificial path explosion.  Eventually we'll probably engineer the GDM so that it does this automatically for common cases.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20101206/a2e2597b/attachment.html>


More information about the cfe-dev mailing list