Locating Loop Errors in Programs: A Scalable and Expressive Approach using LocFaults

Locating Loop Errors in Programs: A Scalable and
Expressive Approach using LocFaults
Mohammed BEKKOUCHE
´
Ecole Sup´erieure en Informatique, Sidi Bel Abb`es, Algeria
LabRI-SBA Laboratory
[email protected]
TACC 2023
November 6th - 8th, 2023
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Presentation Outline
1
Introduction
2
Definitions
3
The problem≤k-MCD
4
Error localization in loops
5
Practical experience
6
Conclusion
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Introduction
Introduction
Debugging is
correction. Identifying the precise locations of problematic instructions, is
most costly
→When a program does not conform to its specification (i.e., contains errors) :
A model checker
counterexamples
With
Consequently, the location of errors in loops is
program
Our approach LocFaults is based on
program’s Control Flow Graph (CFG) from the counterexample to calculate
the minimal subsets necessary
postcondition
Ensuring that our method is
software systems is a crucial criterion for its quality
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Introduction
Introduction
Several
as Tarantula, Ochiai, AMPLE, Pinpoint, FLCN-S, FTFL, ConsilientSFL, and
Poster
Tarantula is the most famous and uses different
degree of suspicion
of tests
These approaches have a drawback in that they require
test cases, while our approach only uses one counterexample
Another challenge with statistical approaches is the need for
determine if a test case’s result is correct or not
To address this issue, we utilize
which only requires
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Introduction
Introduction
Our approach simplifies the problem of error localization by
computing a
(
The CSP represents the constraints of the program, counterexample, and the
assertion or postcondition violated
The calculated set can be either a
Minimal Unsatisfiable Subset (MUS)
Explaining the infeasibility in a CSP can be classified as
BugAssist is a BMC-based error localization method that employs a
Max-SAT solver
→to compute
program with the counterexample
Problem :
LocFaults also works
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Introduction
Introduction
We explore
unfolded b times, and a number of deviated conditions ranging from 0 to 3
LocFaults vs. BugAssist
We avoid transforming
Instead, we use the CFG of the program
counterexample path and paths derived from it. We assume that
conditionals
counterexample path and paths that correct the program
We do not convert program instructions into a
numerical constraints
We do not rely on MaxSAT solvers as
algorithm that uses a constraint solver to calculate MCSs.
We
conditions
We can
most efficient one according to the category of the CSP constructed
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Definitions
Definitions
LetP=<X,C,D>an infeasible CSP, we define forP:
IS (Inconsistent Set)
C
′
is an
C
′
⊆C, andSol(<X,C
′
,D>) =∅.
IIS (Irreducible Inconsistent Set) or MUS (Minimal Unsatisfiable Subset)
C
′
is an
C
′
is an IS.
∀C
′′
⊂C
′
.Sol(<X,C
′′
,D>)̸=∅,C
′
is called irreducible.
MCS (Minimal Correction Set)
C
′
is a
C
′
⊆C.
Sol(<X,C\C
′
,D>)̸=∅.
∄C
′′
⊂C
′
such asSol(<X,C\C
′′
,D>) =∅.
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

The problem≤k-MCD
The problem≤k-MCD
Given an erroneous program modeled in a CFGG= (C,A,E), where :
→Cis the set of conditional nodes,
→Ais the set of assignment blocks,
→andEis the set of arcs,
→along with a counterexample
A Minimal Correction Deviation (MCD) D⊆Csuch that
the counterexample on all the instructions ofGfrom the root, while having
negated D, allows the output
A MCD is called) if no element can be removed from
Dwithout losing this property
The.
The problem≤k-MCD
The problem of finding kis denoted as≤
k-MCD.
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

The problem≤k-MCD
The problem≤k-MCD (example)
As an illustration, consider the CFG of the program AbsMinus :
1c l a s s
2 /*
3 @
&&
4 @
;
5 int
6 int
7 int
8 if
9 k = k +2; }
k
10 if
11 r e s u l t = j - i ; }
12 else
13 r e s u l t = i - j ; }
14 r e t u r n
(a)
k
0
= 0i
0
≤
j
0
k
1
=k
0
+ 2Ifk
1
=k
0
k
1
=
1&&
i
0
! =
j
0
Elser
1
=j
0
−i
0
Ifr
1
=i
0
−j
0
ElsePOST:{r
1
=|i
0
−j
0
|}
(b)
AbsMinus
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

The problem≤k-MCD
The problem≤k-MCD (example)
The counterexample{i= 0,j= 1}
k
0
= 0i
0
≤
j
0
k
1
=k
0
+ 2Ifk
1
=k
0
k
1
=
1&&
i
0
! =
j
0
Elser
1
=j
0
−i
0
Ifr
1
=i
0
−j
0
ElsePOST:{r
1
=|i
0
−j
0
|}
(a)
k
0
= 0i
0
≤
j
0
k
1
=k
0
+ 2Ifk
1
=k
0
k
1
=
1&&
i
0
! =
j
0
Elser
1
=j
0
−i
0
Ifr
1
=i
0
−j
0
ElsePOST:{r
1
=
|i
0
−j
0
|}is UNSAT
(b)
the conditioni0≤j0
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

The problem≤k-MCD
The problem≤k-MCD (example)
The counterexample{i= 0,j= 1}
k
0
= 0i
0
≤
j
0
k
1
=k
0
+ 2Ifk
1
=k
0
k
1
=
1&&
i
0
! =
j
0
Elser
1
=j
0
−i
0
Ifr
1
=i
0
−j
0
ElsePOST:{r
1
=
|i
0
−j
0
|}is SAT
(a)
conditionk1= 1∧i0! =j0
k
0
= 0i
0
≤
j
0
k
1
=k
0
+ 2Ifk
1
=k
0
k
1
=
1&&
i
0
! =
j
0
Elser
1
=j
0
−i
0
Ifr
1
=i
0
−j
0
elsePOST:{r
1
=
|i
0
−j
0
|}is SAT
(b)
deviation
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

The problem≤k-MCD
The problem≤k-MCD (example)
Table
Deviated conditions MCD MCS
∅ / {r1=i0−j0: 13}
{i0≤j0: 8} No /
{k1= 1∧i0! =j0: 10}Yes
{k0= 0 : 7},
{k1=k0+ 2 : 9}
{i0≤j0: 8,
No /
k1= 1∧i0! =j0: 10}
When provided with the counterexample{i= 0,j= 1}, this program has
minimal deviation of size 1
→While the deviation{i0≤j0,k1= 1∧i0̸=j0}does correct the program,
it is
→The only minimal correction deviation for this program is
{k1= 1∧i0̸=j0}
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Error localization in loops
Error localization in loops
1c l a s s
2 /*
i n t e g e r s
3 /*
4 @
l e n g t h
5 @
6 int
7 int
8 int
9 w h i l e
,
(
10 if
11 min = tab [ i ];
12 }
13 i = i +1;
14 }
15 r e t u r n
16 }
17}
min=tab[0]
i= 1i<
tab.length−1
tab[i]<minmin=tab[i]i=i+ 1PostconditionIfIfElseElseGoto
Figure
{∀intk; (k≥0∧k<tab.length);tab[k]≥min}
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Error localization in loops
Error localization in loops
LocFaults use bto unfold
conditional b
CE:{tab
0
[0] = 3∧tab
0
[1] = 2
∧tab
0
[2] = 1∧tab
0
[3] = 0}
min
0
=tab
0
[0]
i
0
= 1i
0
<
tab
0
.length−1
tab
0
[i
0
]<
min
0
min
1
=tab
0
[i
0
]min
1
=min
0
min
4
=min
0
i
4
=i
0
i
1
=i
0
+ 1i
1
<
tab
0
.length−1
tab
0
[i
1
]<
min
1
min
2
=tab
0
[i
1
]min
2
=min
1
min
4
=min
1
i
4
=i
1
i
2
=i
1
+ 1i
2
<
tab
0
.length−1
tab
0
[i
2
]<
min
2
min
3
=tab
0
[i
2
]min
3
=min
2
min
4
=min
2
i
4
=i
2
i
3
=i
2
+ 1
min
4
=min
3
i
4
=i
3
POST:{∀intk; (k≥0∧k<tab
0
.length);
tab
0
[k]≥min
4
}IfIfElseElseIfIfElseElseIf(deviation)IfElseElse
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Error localization in loops
Error localization in loops
CE={tab[0] = 3,tab[1] = 2,tab[2] = 1,tab[3] = 0}
The initial The deviation
CE:{tab
0
[0] = 3∧tab
0
[1] = 2
∧tab
0
[2] = 1∧tab
0
[3] = 0}
min
0
=tab
0
[0]
i
0
= 1i
0
<
tab
0
.length−1
tab
0
[i
0
]<
min
0
min
1
=tab
0
[i
0
]min
1
=min
0
min
4
=min
0
i
4
=i
0
i
1
=i
0
+ 1i
1
<
tab
0
.length−1
tab
0
[i
1
]<
min
1
min
2
=tab
0
[i
1
]min
2
=min
1
min
4
=min
1
i
4
=i
1
i
2
=i
1
+ 1i
2
<
tab
0
.length−1
tab
0
[i
2
]<
min
2
min
3
=tab
0
[i
2
]min
3
=min
2
min
4
=min
2
i
4
=i
2
i
3
=i
2
+ 1
min
4
=min
3
i
4
=i
3
POST:{∀intk; (k≥0∧k<tab
0
.length);
tab
0
[k]≥min
4
}IfIfElseElseIfIfElseElseIf(deviation)IfElseElse
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Error localization in loops
Error localization in loops
CE={tab[0] = 3,tab[1] = 2,tab[2] = 1,tab[3] = 0}
The initial The deviation
CE:{tab
0
[0] = 3∧tab
0
[1] = 2
∧tab
0
[2] = 1∧tab
0
[3] = 0}
CE:{tab
0
[0] = 3∧tab
0
[1] = 2
∧tab
0
[2] = 1∧tab
0
[3] = 0}
min
0
=tab
0
[0]
i
0
= 1
min
0
=tab
0
[0]
i
0
= 1i
0
<
tab
0
.length−1
i
0
<
tab
0
.length−1
tab
0
[i
0
]<
min
0
tab
0
[i
0
]<
min
0
min
1
=tab
0
[i
0
]min
1
=tab
0
[i
0
]min
1
=min
0
min
4
=min
0
i
4
=i
0
i
1
=i
0
+ 1i
1
=i
0
+ 1i
1
<
tab
0
.length−1
i
1
<
tab
0
.length−1
tab
0
[i
1
]<
min
1
tab
0
[i
1
]<
min
1
min
2
=tab
0
[i
1
]min
2
=tab
0
[i
1
]min
2
=min
1
min
4
=min
1
i
4
=i
1
i
2
=i
1
+ 1i
2
=i
1
+ 1i
2
<
tab
0
.length−1
i
2
<
tab
0
.length−1
tab
0
[i
2
]<
min
2
min
3
=tab
0
[i
2
]min
3
=min
2
min
4
=min
2
i
4
=i
2
min
4
=min
2
i
4
=i
2
i
3
=i
2
+ 1
min
4
=min
3
i
4
=i
3
POST:{∀intk; (k≥0∧k<tab
0
.length);
tab
0
[k]≥min
4
}
POST:{∀intk; (k≥0∧k<tab
0
.length);
tab
0
[k]≥min
4
}IfIfIfIfElseElseIfIfIfIfElseElseIf(deviation)IfElseElseElse
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Error localization in loops
Error localization in loops
CE={tab[0] = 3,tab[1] = 2,tab[2] = 1,tab[3] = 0}
The initial The deviation
CE:{tab
0
[0] = 3∧tab
0
[1] = 2
∧tab
0
[2] = 1∧tab
0
[3] = 0}
CE:{tab
0
[0] = 3∧tab
0
[1] = 2
∧tab
0
[2] = 1∧tab
0
[3] = 0}
min
0
=tab
0
[0]
i
0
= 1
min
0
=tab
0
[0]
i
0
= 1i
0
<
tab
0
.length−1
i
0
<
tab
0
.length−1
tab
0
[i
0
]<
min
0
tab
0
[i
0
]<
min
0
min
1
=tab
0
[i
0
]min
1
=tab
0
[i
0
]min
1
=min
0
min
4
=min
0
i
4
=i
0
i
1
=i
0
+ 1i
1
=i
0
+ 1i
1
<
tab
0
.length−1
i
1
<
tab
0
.length−1
tab
0
[i
1
]<
min
1
tab
0
[i
1
]<
min
1
min
2
=tab
0
[i
1
]min
2
=tab
0
[i
1
]min
2
=min
1
min
4
=min
1
i
4
=i
1
i
2
=i
1
+ 1i
2
=i
1
+ 1i
2
<
tab
0
.length−1
i
2
<
tab
0
.length−1
i
2
<
tab
0
.length−1
tab
0
[i
2
]<
min
2
tab
0
[i
2
]<
min
2
min
3
=tab
0
[i
2
]min
3
=tab
0
[i
2
]min
3
=min
2
min
4
=min
2
i
4
=i
2
min
4
=min
2
i
4
=i
2
i
3
=i
2
+ 1i
3
=i
2
+ 1
min
4
=min
3
i
4
=i
3
min
4
=min
3
i
4
=i
3
POST:{∀intk; (k≥0∧k<tab
0
.length);
tab
0
[k]≥min
4
}
POST:{∀intk; (k≥0∧k<tab
0
.length);
tab
0
[k]≥min
4
}IfIfIfIfElseElseIfIfIfIfElseElseIf(deviation)If(deviation)IfIfElseElseElse
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Error localization in loops
Error localization in loops
Table
PATH MCSs
{CE: [tab0[0] = 3∧tab0[1] = 2∧tab0[2] = 1∧tab0[3] = 0],
{min2=tab0[i1]}
min0=tab0[0],i0= 1,min1=tab0[i0],i1=i0+ 1,min2=tab0[i1],
i2=i1+ 1,min4=min2,i4=i2,POST: [(tab0[0]≥min4)
∧(tab0[1]≥min4)∧(tab0[2]≥min4)∧(tab0[3]≥min4)]
{CE: [tab0[0] = 3∧tab0[1] = 2∧tab0[2] = 1∧tab0[3] = 0], {i0= 1},
min0=tab0[0],i0= 1,min1=tab0[i0],i1=i0+ 1, {i1=i0+ 1},
min2=tab0[i1],i2=i1+ 1,[¬(i2≤tab0.length−1)] {i2=i1+ 1}
LocFaults identifies a single MCS on
includes the constraintmin2=tab0[i1]
→This constraint arises from the instruction on
iteration
When
the unfolded loop, i.e.,i2<tab0.length−1
→This deviation implies that we need to execute
the postcondition.
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Practical experience
Practical experience
Tools Used and Experimental Protocol
LocFaults: Our Implementation
→The
→The
→Benchmarks:
→LocFaults will limit itself to deviating
→To calculate
Sakallah
BugAssist: The Error Localization Tool Implementing the BugAssist
Approach
→The MaxSAT solver
→The
erroneous trace
→Benchmarks:
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Practical experience
Practical experience
Creation of Benchmark Dataset
The benchmark set comprises various implementations of,
and,, and
respectively
These programs, enabling us to
study
To increase the program’s
iterations in the execution of each tool
Both LocFaults and BugAssist were subjected to
unfolding loops
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Practical experience
Practical experience
Results (execution time): BubbleSort Benchmark
510152002,0004,0006,000Unfoldings (b)Times (in seconds)LocFaults (= 0)LocFaults (≤1)LocFaults (≤2)LocFaults (≤3)BugAssist
The runtime of LocFaults and
BugAssist shows
with the number of unfoldings
BugAssist consistently having
highest computation times
The different versions of LocFaults
remain usable
unfolding
The number of unfoldings at which
the computation time of BugAssist
becomes
compared to LocFaults
→that of LocFaults with up to 3
conditions deviated is
of LocFaults with up to 2 conditions
deviated
→which is also
LocFaults with up to 1 condition
deviated
→The computation times of
LocFaults with up to 1 and 0
conditions deviated are
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Practical experience
Practical experience
Results: Sum and SquareRoot Benchmarks
2040608010020406080Unfoldings (b)Times (in seconds)LocFaults (≤3)BugAssist20406080100200400600800Unfoldings (b)Times (in seconds)LocFaults (≤3)BugAssist
The execution time of BugAssist
The times of LocFaults remain
The times of LocFaults with at most 0, 1, and 2 conditions deviated are
comparable
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Conclusion
Conclusions & Perspectives
Conclusions
The LocFaults method detects suspicious subsets by analyzing
the CFG to identify the
constraint solvers
The BugAssist method calculates
entire
Both methods start from
We have presented
handling loops with
The initial results indicate that LocFaults is
programs with loops
→The execution times of BugAssist tend
loop unfoldings
→while LocFaults shows
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Conclusion
Conclusions & Perspectives
Perspectives
To validate our results on programs with
To compare the performance of LocFaults with existing
To develop
leveraging the user’s knowledge to select the conditions that should be
deviated
To extend our method to handle numerical instructions involving calculations
on
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Conclusion
Thank you for your attention.Questions ?
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Conclusion
Practical experience
Results (suspicious instructions): SquareRootV40 program
1p u b l i c
2 /*
+1)
3 p u b l i c
4 {
5 int
6 int
7 int
8 int
9 w h i l e
10 v = v + 2* i + 1;
11 i = i + 1;
12 }
13 res = i ;
res
14 r e t u r n
15 }
16}
Figure
The SquareRootV40 program is
designed to find
the square root of the integer
An error is injected at line 13,
resulting in the incorrect return
value of, whereas the correct
value should be
The program contains :
→a
its loop,
→and
postcondition.
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Conclusion
Practical experience
Results (suspicious instructions): SquareRootV40 program
With an unwinding limit of50:
→BugAssist identifies :{9,10,11,13}
→LocFaults identifies suspicious instructions by providing their
the program (instruction line), as well as
iteration number
Table
∅
{5},{6},{9 : 1.11},{9 : 2.11},{9 : 3.11},
{9 : 4.11},{9 : 5.11},{9 : 6.11},{9 : 7.11},{13}
{9 : 7}
{5},{6},{7},{9 : 1.10},{9 : 2.10},{9 : 3.10},
{9 : 4.10},{9 : 5.10},{9 : 6.10},{9 : 1.11},
{9 : 2.11},{9 : 3.11},{9 : 4.11},{9 : 5.11},{9 : 6.11}
Mohammed BEKKOUCHE (ESI-SBA) Locating Loop Errors in Programs November 6th - 8th, 2023

Locating Loop Errors in Programs: A Scalable and Expressive Approach using LocFaults

About This Presentation

Slide Content

Tags

Categories

Download

Quick Actions

Statistics

Related Slideshows

Locating Loop Errors in Programs: A Scalable and Expressive Approach using LocFaults

About This Presentation

Slide Content

Slide 1

Slide 2

Slide 3

Slide 4

Slide 5

Slide 6

Slide 7

Slide 8

Slide 9

Slide 10

Slide 11

Slide 12

Slide 13

Slide 14

Slide 15

Slide 16

Slide 17

Slide 18

Slide 19

Slide 20

Slide 21

Slide 22

Slide 23

Slide 24

Slide 25

Slide 26

Slide 27

Slide 28

Slide 29

Slide 30

Tags

Categories

Download

Quick Actions

Statistics

Related Slideshows

Pray For The Peace Of Jerusalem and You Will Prosper

Don_t_Waste_Your_Life_God.....powerpoint

VILLASUR_FACTORS_TO_CONSIDER_IN_PLATING_SALAD_10-13.pdf

Fertility awareness methods for women in the society

Chapter 5 Arithmetic Functions Computer Organisation and Architecture

syakira bhasa inggris (1) (1).pptx.......