Definition
The all-local-paths coverage criterion is one of two structural coverage criteria considered within the guided Test Case Generation (TCG) framework for Constraint Logic Programming. A coverage criterion is defined as a pair ⟨TC, SC⟩ consisting of:
- TC (termination criterion): ensures finiteness of symbolic execution. The framework adheres to
loop-k, which limits to a thresholdkthe number of allowed loop iterations and/or recursive calls of each concrete loop or recursive method. - SC (selection criterion): steers TCG to determine which paths of the symbolic execution tree will be explored.
The all-local-paths criterion requires that all local execution paths within the method under test are exercised up to a loop-k limit. This has potential interest in the context of unit testing, where each method must be tested in isolation. [1]
Context in the Guided TCG Framework
In the guided TCG framework for CLP, the trace-abstraction of a program (Definition 6) is the starting point for building trace generators for structural coverage criteria. Given a CLP-translated program with traces P, its trace-abstraction is obtained by:
- Removing all atoms in the body of each rule except those corresponding to rule calls.
- Removing all arguments from the head and from the surviving atoms except the last one (i.e., the trace term).
The trace-abstraction essentially corresponds to the control-flow graph of the program. [2]
The trace generator is characterized as:
- Sound if every trace it generates satisfies the coverage criterion.
- Complete if it produces an over-approximation of the set of traces satisfying the criterion.
- Effective based on the number of unfeasible traces it generates — the larger the number, the less effective the trace generator. [2]
Slicing for All-Local-Paths
Starting from the trace-abstraction program, a syntactic program slicing is applied that removes the rules which do not belong to the considered method (Definition 7 — slicing for the all-local-paths coverage criterion). Given a trace-abstraction program P and an entry method M:
- Remove from P all the rules that do not belong to method M.
- For all remaining rules in P, remove from their bodies all the calls to rules which are not in P.
The obtained sliced trace-abstraction, together with the termination criterion, can be used as a trace generator for the all-local-paths criterion for a method. The generated traces will have free variables in those trace arguments that correspond to the execution of other methods, if any. [d8349853-89c6-45f1-8960-1ab703454e90, 6907992d-d5ed-4f80-8377-ffae01b67513]
For method lcm, the sliced trace-abstraction yields six finite traces (shown in Figure 3 of the source) for any loop-K termination criterion. Free variables G and A correspond to the sliced-away calls to methods gcd and abs. [3]
Prolog Implementation
The guided TCG scheme instantiated for the all-local-paths criterion is implemented in Prolog using three key predicates:
computeSlicedProgram(M)— computes the sliced trace-abstraction for method M as in Definition 7.generateTrace(M, TC, Trace)— returns on backtracking all partial traces computed using such sliced trace-abstraction, limited by termination criterion TC.traceGuidedTCG(M, Trace, TC, TestCase)— computes on backtracking the settgTCG(M, Trace, TC)(Def. 4), failing if empty and instantiating on success TestCase and Trace (in case it was partial).
The full Prolog implementation:
prolog (1) guidedTCG(M,TC) :- (2) computeSlicedProgram(M), (3) generateTrace(M,TC,Trace), (4) once(traceGuidedTCG(M,Trace,TC,TestCase)), (5) assert(testCase(M,TestCase,Trace)), (6) fail. (7) guidedTCG(_, _).
Given a (possibly partial) trace generated in line (3), if the call in line (4) fails, the next trace is tried. Otherwise, the generated test case is asserted with its corresponding trace which is now fully instantiated (in case it was partial). The process finishes when generateTrace/3 has computed all traces, in which case it fails, making the program exit through line (7). [3]
Example: Method lcm
For the all-local-paths criterion applied to method lcm, three test cases are obtained, achieving full code and path coverage:
| Constraint store | Trace |
|---|---|
| {A>=B} | lcm(1,[cont(1,[gcd(1,[loop(1,[abs(1,[])])]),check(1,[abs(1,[]),div(1,[])])])]) |
| {A=B=0, Out=-1} | lcm(1,[cont(1,[gcd(1,[loop(1,[abs(1,[])])]),check(1,[abs(1,[]),div(2,[])])])]) |
| {B>A} | lcm(2,[cont(1,[gcd(1,[loop(1,[abs(1,[])])]),check(1,[abs(1,[]),div(1,[])])])]) |
This set of three test cases achieves full code and path coverage on method lcm and is thus a perfect choice in the context of unit-testing. In contrast, the original, non-guided TCG scheme with loop-2 as termination criterion produces nine test cases. [3]
Experimental Evaluation
The guided TCG scheme for the all-local-paths coverage criterion was implemented and integrated within PET, an automatic TCG tool for Java bytecode. The experimental comparison against standard TCG (with post-filtering) demonstrates significant reductions in the number of generated test cases while maintaining 100% code coverage on most benchmark methods from the net.datastructures library (methods from NodeSequence, SortedListPriorityQueue, BinarySearchTree, and HeapPriorityQueue). [4]
For example, guided TCG produced 5 test cases for Seq.elemAt versus 24 for standard TCG; 18 test cases for BST.addAll versus 379; and 9 test cases for BST.insert versus 970 — all achieving 100% code coverage. [4]