Numerical Non-Relational Domains
Pietro Ferrara
Chair of Programming Methodology
ETH
Zurich, Switzerland
Analisi e Verifica di Programmi
Universita’ Ca’ Foscari, Venice, Italy
Chi sono
• Febbraio 05: Laurea specialistica
• Ottobre 05-Maggio 09: Dottorato
> Ecole Polytechnique/ENS (Radhia Cousot)
> Universita’ Ca’ Foscari (Agostino Cortesi)
• Agosto-Ottobre 07: Internship
> Microsoft (Francesco Logozzo)
• Da Aprile 09: Postdoc
> ETH Zurich (Peter Mueller)
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Obiettivo
• Scopo di queste (oggi e 16/12) lezioni
> Applicazione pratica
• Dominio e semantica
> Concreti e astratti
> Di un “toy-language”
• Domini numerici non relazionali
• Domini numerici relazionali
• Astrazioni dello heap
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Outline
1.
2.
3.
4.
Recalls of Abstract Interpretation
Language and Concrete Semantics
Abstract Semantics
Numerical Non-Relational Domains
•
•
•
•
Sign
Parity
Congruences
Intervals
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Galois Connection
• The abstract domain is a sound
approximation of the concrete domain iff
> they form a Galois connection
•
iff
>
is reductive
•
>
is extensive
•
>
and
are monotone
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is monotone
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is monotone
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is monotone
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is monotone
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is reductive
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is reductive
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is reductive
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is extensive
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
>
is extensive
•
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Peter Müller
MALE
Marlies Weissert
Katja Abrahams
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
Soundness of the semantics
• Two main components:
> Abstract and concrete domains
• Soundness proved via Galois connection
• Abstract and concrete semantics
• Intuition:
> The abstract overapproximates the concrete
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
• Semantics
> Next person following the alphabetical order
•
•
•
•
Bossi -> Cortesi
Cortesi -> Ferrara
Ferrara -> Raffaeta’
Raffaeta’ -> Bossi
> In the abstract:
• I do not know! Top!
• Always sound 
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Another example
• Semantics
> Give the other person of the same gender
•
•
•
•
Bossi -> Raffaeta’
Raffaeta’ -> Bossi
Cortesi -> Ferrara
Ferrara -> Cortesi
> In the abstract:
•
•
•
•
MALE -> MALE
FEMALE -> FEMALE
TOP -> TOP
BOTTOM-> BOTTOM
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Agostino Cortesi
`
Annalisa Bossi
MALE
Alessandra Raffaeta’
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
An example
Concrete domain: People
Abstract domain: Gender
Pietro Ferrara
Agostino Cortesi
`
Annalisa Bossi
MALE
Alessandra Raffaeta’
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
FEMALE
Outline
1.
2.
3.
4.
Recalls of Abstract Interpretation
Language and Concrete Semantics
Abstract Semantics
Numerical Non-Relational Domains
•
•
•
•
Sign
Parity
Congruences
Intervals
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Syntax
• Toy language
• Commands:
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Syntax
• Expressions:
where:
> c is an integer value
> x is a variable
> <op> arithmetic operator, i.e. +, -, *, /
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Syntax
• Conditions:
where:
> <comp> is a comparison operator
• >, <, ==, !=
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
i=0;
r=1;
while(i<exp) {
r=r*2;
i=i+1;
}
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
• Which is the semantics of this program?
• Input:
i=0;
r=1;
while(i<exp) {
r=r*2;
i=i+1;
}
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Concrete domain
• For each variable, we trace a value:
• Runtime behaviors:
> Set of environments
> Lattice with set operators:
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Semantics of expressions
• Function that
> given a state and an expression
> returns an integer value
• States = Concrete domain
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Formal definition
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Semantics of conditions
• Function that
> given a state and a condition
> returns true or false
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Formal definition
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Semantics of commands
• Function that
> given a state and a command
> returns the following state and command
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Concatenation
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
If
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
While
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Assignment
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Outline
1.
2.
3.
4.
Recalls of Abstract Interpretation
Language and Concrete Semantics
Abstract Semantics
Numerical Non-Relational Domains
•
•
•
•
Sign
Parity
Congruences
Intervals
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstract non-relational domain
• Pointwise abstraction of concrete domain
•
: abstraction of numerical values
> Sign, intervals, parity, congruences, …
• Abstract set of integers with a value:
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Sign domain
• Which is the semantics of this program?
• Input:
i=0;
r=1;
while(i<exp) {
r=r*2;
Fixpoint!
i=i+1;
}
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Semantics of expressions
• Quite similar to concrete definitions!
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Formal definition
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Evaluation of constants
•
:primitive of numerical domain
• Given an integer constant, returns its
abstraction
• E.g.: sign domain
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Evaluation of arith. expressions
•
:primitive of numerical domain
• Given an arithmetical expression, it returns
the abstract result
• E.g.:
*
0
+
top
0
0
0
0
0
+
0
+
-
top
-
0
-
+
top
top
0
top
top
top
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Semantics of conditions
• Function that
> given a state and a condition
> returns true or false or top
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Formal definition
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstract or operator
Abstract
or
True
False
Top
True
True
True
True
False
True
False
Top
Top
True
Top
Top
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstract and operator
Abstract
and
True
False
Top
True
True
False
Top
False
False
False
False
Top
Top
False
Top
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Evaluation of condition
•
:primitive of numerical domain
• Given a conditional expression, returns
true/false/top
• E.g.:
<
0
+
top
0
false
true
false
top
+
false
top
false
top
-
true
true
top
top
top
top
top
top
top
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Semantics of commands
• Quite similar to the concrete definition
• Need to consider when a condition is
evaluated to top
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Concatenation
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Assignment
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
If
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
If
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
While
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Summary
• A non-relational domain has to provide:
> Operators on lattices
• Partial ordering
• Upper and lower bounds
• Top and bottom elements
> Abstraction and concretization functions
>
>
>
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Implementation
public interface NumericalDomain {
public boolean lessEqual(NumericalDomain val);
public boolean lub(NumericalDomain val1, NumericalDomain val2);
public boolean glb(NumericalDomain val1, NumericalDomain val2);
public boolean widening(NumericalDomain val1, NumericalDomain val2);
public NumericalDomain eval_const(int value);
public NumericalDomain eval_arithm
(NumericalDomain val1, NumericalDomain val2, ArithmeticOperator op);
public BooleanDomain eval_cond
(NumericalDomain val1, NumericalDomain val2, ConditionalOperator op);
}
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Outline
1.
2.
3.
4.
Recalls of Abstract Interpretation
Language and Concrete Semantics
Abstract Semantics
Numerical Non-Relational Domains
•
•
•
•
Sign
Parity
Congruences
Intervals
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Lattice structure
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Implementation
public class SignDomain implements NumericalValue {
private enum Values {top, bottom, plus, minus, zero}
private Values val=Values.bottom;
public SignDomain(Values v) {
val=v;
}
public boolean lessEqual(NumericalValue v) {
if(this.val==SignDomain.Values.bottom) return true;
if(((SignDomain) v).val==SignDomain.Values.top)
return true;
if(this.equals(v)) return true;
return false;
}
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Implementation
public NumericalValue lub(NumericalValue v1, NumericalValue v2) {
SignDomain val1=(SignDomain) v1;
SignDomain val2=(SignDomain) v2;
if(val1.val==Values.bottom) return v2.clone();
if(val2.val==Values.bottom) return v1.clone();
if(val1.val==Values.top || val2.val==Values.top)
return new SignDomain(Values.top);
if(val1.val==val2.val) return new SignDomain(val1.val);
return new SignDomain(Values.top);
}
public NumericalValue widening(NumericalValue v1, NumericalValue v2) {
return this.lub(v1, v2);
}
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstraction and concretization
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstraction and concretization
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
0
-3
-1
-5
-10
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
2
1
0
-5
-1
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
0
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_const
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Implementation
public NumericalValue evalConstant(long value) {
if(value > 0) return new SignDomain(Values.plus);
if(value == 0) return new SignDomain(Values.zero);
if(value < 0) return new SignDomain(Values.minus);
}
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_arithm
+
_|_
0
+
-
T
_|_
_|_
_|_
_|_
_|_
_|_
0
_|_
0
+
-
T
+
_|_
+
+
T
T
-
_|_
-
T
-
T
T
_|_
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
T
eval_arithm
-
_|_
0
+
-
T
_|_
_|_
_|_
_|_
_|_
T
0
_|_
0
-
+
T
+
_|_
+
T
+
T
-
_|_
-
-
T
T
T
_|_
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
T
eval_arithm
*
_|_
0
+
-
T
_|_
_|_
_|_
_|_
_|_
_|_
0
_|_
0
0
0
0
+
_|_
0
+
-
T
-
_|_
0
-
+
T
T
_|_
0
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
T
eval_arithm
/
_|_
0
+
-
T
_|_
_|_
_|_
_|_
_|_
_|_
0
_|_
_|_
0
0
0
+
_|_
_|_
+
-
T
-
_|_
_|_
-
+
T
T
_|_
_|_
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
T
An example
Operation: i+1
4
5
2
3
0
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
Operation: i+4
6
2
-2
2
0
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Implementation (+)
SignDomain val1=(SignDomain) v1;
SignDomain val2=(SignDomain) v2;
if(val1.val==Values.bottom || val2.val==Values.bottom)
return new SignDomain(Values.bottom);
if(val1.val==Values.plus && val2.val==Values.plus)
return new SignDomain(Values.plus);
if(val1.val==Values.zero && val2.val==Values.plus)
return new SignDomain(Values.plus);
if(val1.val==Values.zero && val2.val==Values.minus)
return new SignDomain(Values.minus);
if(val1.val==Values.zero && val2.val==Values.zero)
return new SignDomain(Values.zero);
if(val1.val==Values.minus && val2.val==Values.minus)
return new SignDomain(Values.minus);
return new SignDomain(Values.top);
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_cond
<
_|_
0
+
-
T
_|_
T
T
T
T
T
0
T
false
true
false
T
+
T
false
T
false
T
-
T
true
true
T
T
T
T
T
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_cond
==
_|_
0
+
-
T
_|_
T
T
T
T
T
0
T
true
false
false
T
+
T
false
T
false
T
-
T
false
false
T
T
T
T
T
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
5>0
+>0
Concrete
eval_cond
true
Abstract
eval_cond
=
true
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
5>1
+>+
Concrete
eval_cond
true
Abstract
eval_cond
<=
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Implementation (<)
if(val1.val==Values.top || val2.val==Values.top) return BooleanDomain.Top;
if(val1.val==Values.bottom || val2.val==Values.bottom)
return BooleanDomain.Top;
if(val1.val==Values.minus) {
if(val2.val==Values.zero || val2.val==Values.plus)
return BooleanDomain.True;
else return BooleanDomain.Top;
}
else
if(val1.val==Values.zero) {
if(val2.val==Values.plus) return BooleanDomain.True;
else return BooleanDomain.False;
}
else
if(val2.val==Values.zero || val2.val==Values.minus)
return BooleanDomain.False;
else return BooleanDomain.Top;
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Outline
1.
2.
3.
4.
Recalls of Abstract Interpretation
Language and Concrete Semantics
Abstract Semantics
Numerical Non-Relational Domains
•
•
•
•
Sign
Parity
Congruences
Intervals
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Lattice structure
O
E
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstraction and concretization
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstraction and concretization
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
i%2=0
5
-1
13
O
i%2=1
7
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
E
An example
i%2=0
18
4
5
-1
O
i%2=1
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
E
An example
i%2=0
O
i%2=1
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
E
eval_const
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_arithm
+
_|_
O
E
T
_|_
_|_
_|_
_|_
_|_
O
_|_
E
O
T
E
_|_
O
E
T
T
_|_
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_arithm
-
_|_
O
E
T
_|_
_|_
_|_
_|_
_|_
O
_|_
E
O
T
E
_|_
O
E
T
T
_|_
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_arithm
*
_|_
O
E
T
_|_
_|_
_|_
_|_
_|_
O
_|_
O
E
T
E
_|_
E
E
E
T
_|_
T
E
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_arithm
/
_|_
O
E
T
_|_
_|_
_|_
_|_
_|_
O
_|_
O
O
T
E
_|_
E
T
T
T
_|_
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
i%2=0
Operation: i+1
4
2
5
O
3
i%2=1
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
E
An example
Operation: i+1
i%2=0
2
2
1
3
O
i%2=1
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
E
eval_cond
<
_|_
O
E
T
_|_
T
T
T
T
O
T
T
T
T
E
T
T
T
T
T
T
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_cond
==
_|_
O
E
T
_|_
T
T
T
T
O
T
T
false
T
E
T
false
T
T
T
T
T
T
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
5==2
O == E
Concrete
eval_cond
false
Abstract
eval_cond
=
false
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
5>1
O>O
Concrete
eval_cond
true
Abstract
eval_cond
<=
T
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Outline
1.
2.
3.
4.
Recalls of Abstract Interpretation
Language and Concrete Semantics
Abstract Semantics
Numerical Non-Relational Domains
•
•
•
•
Sign
Parity
Congruences
Intervals
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Lattice structure
1
2
3
5
….
6
10
15
….
….
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Lattice operators
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstraction and concretization
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstraction and concretization
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
10
20
15
5 30
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
5
An example
5
i%5=0
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_const
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_arithm
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
Operation: i+1
1
5
3
6
4
2
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_cond
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Outline
1.
2.
3.
4.
Recalls of Abstract Interpretation
Language and Concrete Semantics
Abstract Semantics
Numerical Non-Relational Domains
•
•
•
•
Sign
Parity
Congruences
Intervals
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Lattice structure
[-inf..+inf]
….
….
….
[-1..1]
….
[-1..0] [0..1]
….
[-1..-1] [0..0]
[1..1]
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
….
Lattice operators
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstraction and concretization
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Abstraction and concretization
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
-1
0
1
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
[-1..1]
An example
5
10
8
7
9
6
[5..10]
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
5
76
8
9
10
[5..10]
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_const
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
eval_arithm
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
Operation: i+1
3
6
[3..8]
8
4
7
9
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
[4..9]
An example
Operation: 5/i
-1
[-3..-1]
-3
-5
-1
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
[-5..-1]
eval_cond
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
{2, 3}<{5, 6}
[2..3]<[5..6]
Abstract
eval_cond
Concrete
eval_cond
true
=
true
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An example
{2, 4}<{3, 5}
[2..4]<[3..5]
Abstract
eval_cond
Concrete
eval_cond
top
=
top
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Reduced Product
• Different domains (may) collect different
information
• Combine them
> In order to obtain a more precise analysis
• First step: Cartesian product
> Collect two abstract values
> No flow of information between domains
• Second step: reduced product
> Flow of information!
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Cartesian Product
• Given two abstract domains
• Cartesian product:
and
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
An Example
i=0;
r=1;
while(i<exp) {
r=r*2;
i=i+1;
}
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Another Example
if(…)
i=2;
else i=4;
if(i%2==1)
throw new Exception();
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Reduced Product
• Flow of information between domains
• Cartesian product…
• … equipped with a reduce function!
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Some examples
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy
Summary
• Impossible to compute all the numerical
values
• Approximation required
• First step: non-relational abstraction
> Many different domains
• Sign, Intervals, Congruence, Parity, …
> Cartesian and reduced products
• Second step: relational abstraction
Pietro Ferrara: “Numerical Non-Relational Domains”
Analisi e Verifica di Programmi, Universita’ Ca’ Foscari, Venice, Italy