Symbolic program analysis using term rewriting and generalization
View Patent ↗Systems and methods are disclosed for analyzing data-flow using program expressions or terms by extracting a control flow graph node from a work list; merging symbolic term values at join nodes; performing simplification of term values using rewriting logic; determining successors of the graph node to which data must be propagated; and updating symbolic data for elements of the successors.
1. A computer implemented method for analyzing data-flow using program expressions or terms, comprising:
a. extracting a control flow graph node from a work list;
b. representing a symbolic state as a condition-map pair (C, σ) where C denotes a current path condition predicate and σ denotes a map from program variables to symbolic values;
c. merging symbolic term values at join nodes to avoid path-explosion by using choose and if-then-else (ite) function operators, where choose is a term of form choose ((C 1 ,t 1 ),(C 2 ,t 2 ),(C 3 ,t 3 )) on expression sort with a non-deterministic choice between the values t 1 (1≦i≦3) given a corresponding condition C 1 ;
d. performing simplification of term values using rewriting logic, wherein a set of rules for simplifying choose and ite terms are used along with rules for simplifying Presburger arithmetic expressions;
e. determining successors of the graph node to which data must be propagated;
f. updating symbolic data for elements of the successors;
g. performing anti-unification to generalize similar terms obtained at a loop head; and
h. displaying the program analysis for code review.
2. The method of claim 1 , comprising performing symbolic program analysis through decision procedures with rewriting engines.
3. The method of claim 2 , wherein the decision procedures comprise a Satisfiability Modulo Theories (SMT) solver.
4. The method of claim 1 , comprising determining join if needed.
5. The method of claim 1 , wherein the successors are determined using a Satisfiability Modulo Theories (SMT) solver.
6. The method of claim 1 , comprising simplifying choose-terms to if-then-else (ite)-terms.
7. The method of claim 1 , comprising simplifying ite-terms by using equational axioms, semantic rules and rules for presburger arithmetic.
8. The method of claim 1 , comprising simplifying terms at loop nodes using anti-unification.
9. The method of claim 7 , comprising constructing a bounded parameterized term.
10. The method of claim 7 , comprising computing a bounded parameterized term by generalizing from individual terms obtained during symbolic analysis at loop head.
11. The method of claim 7 , comprising generalizing similar terms obtained at a loop head.
12. The method of claim 1 , comprising representing analysis results during symbolic program analysis using choose and ite function operators.
13. The method of claim 1 , comprising using rewriting rules in a rewrite logic to uniformly simplify terms over a combination of theories.
14. The method of claim 1 , comprising representing data as condition-value pairs and computing joins using choose functions over such pairs.
15. The method of claim 1 , comprising simplifying symbolic terms during program analysis using a rewrite engine.
16. The method of claim 1 , comprising simplifying ite expressions using equational axioms and semantic methods.
17. The method of claim 1 , comprising rewrite system comprises Presburger arithmetic rules in a rewrite logic theory.
18. The method of claim 1 , comprising simplifying, approximating and generalizing terms obtained from symbolic program analysis at loop heads using anti-unification.
19. The method of claim 1 , comprising computing loop invariants given a parameterized term representation.
20. The method of claim 1 , comprising computing an under-approximation based on a parameterized term representation.