Available facts analysis #1152

arbipher · 2021-08-11T21:08:20Z

I have fixed the issues in our previous code review.

…ent (#1139)" (#1141) This reverts commit 980321d.

We introduce a 2-bit field called CheckedScopeSpecifier in the Stmt class. During parsing when a compound statement is created we iterate the elements (statements) of the compound statement and set the checked scope specifier for each element to the checked scope specifier of the compound statement. We can get the checked scope specifier for a statement by calling the getCheckedScopeSpecifier method on the statement.

* Updated the instructions for upgrade of LLVM/Clang. Also added a new file LLVM-Upgrade-Notes.md to track important information related to upgrades. * Fixed typos. * Addressed review comments. * Fixed an inadvertent deletion. * Addressed review comments. * Incorporated review comments. * Fixed minor typos. * Fixed typos.

…BoundsExpr

Add InferredFact and adjust WhereClauseFact to be a subclass of AbstractFact

`IsSwitchCaseBlock`: use `dyn_cast_or_null` to cover the null pointer case. `ConditionOnEdge`: do not test if there is no edge between pred to curr since it will only be called if there is an edge. `GetModifiedVars`: use `TranspareCasts` to bypass some casting. The feature to deal with membership access and the array indexing is still TODO.

from the previous available facts analysis)

It also fixes a bug to visit dead blocks.

…-wip

The community has introduced a new annotation called "contains-errors" on AST nodes that contain semantic errors. As a result, after the upgrade of Checked C sources to LLVM 12 we need to check if an expr contains errors before operating on the expr. One such place is in InverseUtil::IsInvertible where we need to check if the input modifying expr contains errors. * Added containsErrors checks to InverUtil::Inverse

Support bounds widening in presence of complex conditionals like: "if (*p != 0)", "if ((c = *p) == 'a')", etc.

kkjeer · 2021-08-12T17:29:55Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+      SemaRef(SemaRef), Cfg(Cfg), Ctx(Ctx), Lex(Lex), OS(llvm::outs()),
+      FactComparisionMap(FactComparisionMapTy()) {}
+
+    // Pretty print a expr


Suggested comment change: Pretty print a expr => Pretty print an expression.

If you don't mind my snooping on PRs in your repository unrelated to 3C: The GitHub "suggested change" feature (the "±" icon in the toolbar when writing a review comment) might provide a more streamlined process for changes like this. (GitHub's documentation is in item 6 here.) An example of what it looks like:

Suggested change

// Pretty print a expr

// Pretty print an expression.

Thank you all. I will reword this and I learn the new GitHub primitive!

kkjeer · 2021-08-12T17:30:17Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+    // Pretty print a expr
+    void Print(const Expr *) const;
+
+    // Pretty print a Stmt


Suggested comment change: Pretty print a Stmt => Pretty print a statement.

kkjeer · 2021-08-12T17:30:48Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+    // Pretty print a Stmt
+    void Print(const Stmt *) const;
+
+    // Pretty print an abstract fact


Suggested comment change Pretty print an abstract fact => Pretty print an abstract fact.

kkjeer · 2021-08-12T17:31:14Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+    // Pretty print an abstract fact
+    void DumpAbstractFact(const AbstractFact *Fact) const;
+
+    // Pretty print a list of abstract facts


Suggested comment change: Pretty print a list of abstract facts => Pretty print a list of abstract facts.

kkjeer · 2021-08-12T17:31:35Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+    // Pretty print a set of variables.
+    void PrintKillVarSet(KillVarSetTy VarSet) const;
+
+   // Determine if the edge from PredBlock to CurrBlock is a fallthrough.


Nit: add a space before // Determine if...

kkjeer · 2021-08-12T17:32:18Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+    // Determine if a variable is used in a fact.
+    bool IsVarInFact(const AbstractFact *Fact, const VarDecl *Var) const;
+
+    // Determine if two facts equal. First check if the comparision is check before,


Nit: two facts equal => two facts are equal, comparision => comparison, is check before => is checked before

kkjeer · 2021-08-12T20:20:58Z

clang/lib/Sema/AvailableWhereFactsAnalysis.cpp

+  for (auto *Fact : WC->getFacts()) {
+    if (auto *BF = dyn_cast<BoundsDeclFact>(Fact)) {
+      // ignore the result value here,
+      // just take the side-effect to save the normalzied bounds


normalzied => normalized

kkjeer · 2021-08-12T20:21:37Z

clang/lib/Sema/AvailableWhereFactsAnalysis.cpp

+  }
+}
+
+// Initiazlize Gen and Out of a block


Initiazlize => Initialize

mgrang · 2021-08-13T01:02:59Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+  using OrderedBlocksTy = std::vector<const CFGBlock *>;
+
+  // AvailableFactsKillKind denotes two kinds of kill variables.
+  // KillExpr denotes a variable to kill a EqualityOpFact or a InferredFact


Maybe these could be rephrased as:

// KillExpr denotes a variable that kills an EqualityOpFact or an InferredFact // KillBounds denotes a variable that kills a BoundsDeclFact.

mgrang · 2021-08-13T01:04:37Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+  // AvailableFactsKillKind denotes two kinds of kill variables.
+  // KillExpr denotes a variable to kill a EqualityOpFact or a InferredFact
+  // KillBounds denotes a variable to kill a BoundsDeclFact.
+  enum AvailableFactsKillKind {


You might want to declare this as an enum class to possibly avoid future conflicts of KillExpr and KillBounds with variables of the same name.

mgrang · 2021-08-13T01:05:43Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+  using StmtKillVarSetTy = llvm::DenseMap<const Stmt *, KillVarSetTy>;
+
+  // FactComparisionMapTy denotes the comparision result of two facts.
+  using FactComparision = std::pair<const AbstractFact *, const AbstractFact *>;


Typos in comment: FactComparisionMapTy denotes the comparision result of two facts. --> FactComparisonMapTy denotes the comparison result of two facts.

Typo in variable name: FactComparision --> FactComparison

mgrang · 2021-08-13T01:09:48Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+    bool IsSwitchCaseBlock(const CFGBlock *PredBlock,
+                           const CFGBlock *CurrBlock) const;
+
+    // Determine the boolean state of an edge when the 


This comment seems incomplete.

mgrang · 2021-08-13T01:12:12Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+
+      const CFGBlock *Block;
+
+      // Block-wise


Nit: Period (.) needed after each comment.

mgrang · 2021-08-13T01:13:55Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+    void DumpAvailableFacts(FunctionDecl *FD);
+
+  private:
+    void AddSuccsToWorkList(const CFGBlock *CurrBlock, WorkListTy &WorkList);


Comments needed for the function.

mgrang · 2021-08-13T01:14:23Z

clang/include/clang/Sema/AvailableWhereFactsAnalysis.h

+    void ComputeStmtGenKillSets(ElevatedCFGBlock *EB, const Stmt *CurrStmt,
+                                StmtSetTy NestedStmts);
+
+    void CollectFactsInDecl(AbstractFactListTy &Gen,


Comments needed for function.

mgrang · 2021-08-13T01:16:51Z

clang/lib/Sema/AvailableWhereFactsAnalysis.cpp

+// This file implements a dataflow analysis for available facts analysis.
+//===---------------------------------------------------------------------===//
+
+#include "clang/AST/ExprUtils.h"


Please order the includes alphabetically.

mgrang · 2021-08-13T01:24:50Z

clang/lib/Sema/AvailableWhereFactsAnalysis.cpp

+      EB->Kill = EB->StmtKill[CurrStmt];
+      EB->GenAllSucc = EB->StmtGen[CurrStmt];
+    } else {
+      EB->Kill = AFUtil.Union(EB->Kill, EB->StmtKill[CurrStmt]);


It might be costly (in terms of space) to persist the accumulated Kill and StmtGen sets. Is it possible to locally compute them when needed?

Oh you are right. The accumulated Kill is one per block which may not be large, but definitely StmtGem is costly. That is for debugging originally.

… 1 in TargetSrcEquality (#1162) * Add AllowTempEquality parameter to RecordEqualityWithTarget * Use a ModifiedSameValue variable to determine the return value for UpdateSameValueAfterAssignment * Rename ModifiedSameValue to RemovedAnyExprs and clean up comments

…nces (#1163) * In CheckAddressOfOperand, add case for address-of array subscripts to C99-specific logic * Move address-of array subscript check after other checks such as taking the address of an lvalue * Adjust expected AST output to account for different types of address-of array subscripts * Restore deleted comment about checking for array subscript expressions * Add comment explaining the placement of the address-of array subscript logic * Put &e1[e2] typing rules under a Checked C flag

arbipher · 2021-08-25T16:29:46Z

I have fixed the issues you mentioned (sorry for so many typos).
When developing the code for SMT prover, I made some changes to the analysis and later I will split the related part to this PR.

sulekhark

LGTM! Thank you very much for this work!

Mandeep Singh Grang and others added 29 commits August 5, 2021 10:51

Revert "[BoundsWidening] Determine checked scope specifier per statem…

9326e89

…ent (#1139)" (#1141) This reverts commit 980321d.

Add new flags for available facts analysis

76e3e53

Add the analysis into the build script and the sema bounds

820a2bb

Add utility functions to check whether a var is used in a Expr and a …

0d28f64

…BoundsExpr

Add AbstractFact as a basic available fact;

7c67bed

Add InferredFact and adjust WhereClauseFact to be a subclass of AbstractFact

Add data structures used in the analysis

7ce39cd

Add print and dump functions

820186f

Add utility functions which are also used by BoundsWideningAnalysis.

dbc7421

Add fact comparision and fact-realted set oerations (contains TODO).

1cf53e0

Add testscases (one covers basic features and the other is converted

95af48e

from the previous available facts analysis)

Dataflow analysis: Add statement-based Gen/Kill.

298fe7f

Dataflow analysis: Add block-edge-based Gen set.

1628720

Dataflow analysis: Add function to compute In and Out set.

47cd2d5

Dataflow analysis: Addworklist algorithm.

30f3bbe

Add desctrutors to release the memory

94c119f

Fix: modify the Gen/Kill rules to match the design doc;

6dea61d

It also fixes a bug to visit dead blocks.

Cleanup comments

fc839ce

Fix: use the exisiting functions to find a VarDecl in an expr

6f436dc

Change the equal check on fact collections to equal size check

d72250e

Update the testcases with the updated Gen/Kill

dfe37d9

Remove debug flag for available facts.

a649db8

Use lexco-compare for EqualityOpFact and InferredFact.

c62fb9d

Add a map to store the comparision results of facts.

f180ccb

Change the source location of a fact to its near expr.

7c9eedc

Use a dedicated list to collect created facts and clean them finally.

6cc600c

Merge branch 'internship-2021-checkins' into available-facts-analysis…

424ef4a

…-wip

arbipher requested a review from mgrang August 11, 2021 21:48

arbipher requested review from kkjeer and sulekhark August 11, 2021 21:48

Mandeep Singh Grang added 2 commits August 12, 2021 11:24

[BoundsWidening] Handle complex conditionals in bounds widening (#1149)

c218fc6

Support bounds widening in presence of complex conditionals like: "if (*p != 0)", "if ((c = *p) == 'a')", etc.

kkjeer reviewed Aug 13, 2021

View reviewed changes

mgrang reviewed Aug 13, 2021

View reviewed changes

kkjeer and others added 3 commits August 20, 2021 15:05

Merge branch 'master' into available-facts-analysis-wip

2e5631a

arbipher changed the title ~~Available facts analysis wip~~ Available facts analysis Aug 25, 2021

Update the available facts analysis.

4f8aa5b

arbipher force-pushed the available-facts-analysis-wip branch from 5bae193 to 4f8aa5b Compare August 25, 2021 17:41

sulekhark approved these changes Aug 26, 2021

View reviewed changes

arbipher merged commit a167f43 into internship-2021-checkins Aug 26, 2021

secure-sw-dev-bot mentioned this pull request Jan 17, 2022

Available facts analysis checkedc/checkedc-llvm-project#1151

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Available facts analysis #1152

Available facts analysis #1152

arbipher commented Aug 11, 2021

kkjeer Aug 12, 2021

mattmccutchen-cci Aug 13, 2021 •

edited

arbipher Aug 25, 2021

kkjeer Aug 12, 2021

arbipher Aug 25, 2021

kkjeer Aug 12, 2021

kkjeer Aug 12, 2021

kkjeer Aug 12, 2021

kkjeer Aug 12, 2021

kkjeer Aug 12, 2021

kkjeer Aug 12, 2021

mgrang Aug 13, 2021

mgrang Aug 13, 2021

arbipher Aug 13, 2021

mgrang Aug 13, 2021

mgrang Aug 13, 2021

mgrang Aug 13, 2021

mgrang Aug 13, 2021

mgrang Aug 13, 2021

mgrang Aug 13, 2021

mgrang Aug 13, 2021

arbipher Aug 13, 2021

arbipher commented Aug 25, 2021

sulekhark left a comment

Available facts analysis #1152

Available facts analysis #1152

Conversation

arbipher commented Aug 11, 2021

Choose a reason for hiding this comment

mattmccutchen-cci Aug 13, 2021 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arbipher commented Aug 25, 2021

sulekhark left a comment

Choose a reason for hiding this comment

mattmccutchen-cci Aug 13, 2021 •

edited