Równoważność programów
Wyniki
Podsumowanie
Kontrprzykład
Założenia
Sędzia
dobre (100/100)
int add(int a, int b) {
return a + b;
}
Rozwiązania
void check(int r1, int r2)
{
assert(r1 == r2);
}
Fałszywy alarm
void assumptions(int a, int b)
{
__CPROVER_assume(a > 0);
__CPROVER_assume(b > 0);
}
int add(int a, int b) {
while (--b)
++a;
return a;
}
złe (np. 50/100)
Brak kontrprzykładu
Scalenie
int add1() ...
int add2() ...
int main()
{
int a = nondet_int();
int b = nondet_int();
assumptions(a, b);
int r1 = add1(a, b);
int r2 = add2(a, b);
check(r1, r2);
}
∞
Proste różnice
w semantyce
int equi ( int A[], int n ) {
if(n<=0)
return -1;
int64_t backSum = 0, forSum = 0;
int i;
for(i=0; i<n; i++)
backSum += A[i];
for(i=0; i<n; i++)
{
backSum -= A[i];
if(backSum == forSum)
return i;
forSum += A[i];
}
return -1;
}
int maxRS ( int A[], int n ) {
int best=0, current=0, i, begin=0, ii=0;
for (i=0;i<n;i++){
if (A[i]<A[i+1]){
current = current +1;
}else{
if (current>best){
best=current;
ii=begin;
current=0;
begin=i;
}else{
current=0;
begin=i+1;
}
}
}
return ii;
}
złośliwość
vs
przypadek
[[-2147483648, -2147483648, 4194304]]
Program C
file source.c: Parsing
Converting
Type-checking source
Generating GOTO Program
...
Program
GOTO
...
size of program expression: 414 assignments
simple slicing removed 5 assignments
...
{-213} i@1#20 == (\guard#24 && \guard#25 && \guard#26 &&
\guard#27 && \guard#28 && !\guard#29 ? i@1#12 : i@1#19)
{-214} sum_left@1#11 == (\guard#24 && \guard#25 && \guard#26 &&
\guard#27 && \guard#28 && !\guard#29 ? sum_left@1#3 : sum_left@1#10)
...
CBMC
Formuła logiczna
?
...
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 without simplifier
60281 variables, 220208 clauses
Verified 209725 original clauses.
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.691s
...
State 47 file source.c line 94 function equi thread 0
----------------------------------------------------
source::equi::1::i=1 (00000000000000000000000000000001)
State 49 file source.c line 95 function equi thread 0
----------------------------------------------------
source::equi::1::right=3242196992 (0000000000000000000000000000000011000001010000000000000000000000)
State 50 file source.c line 94 function equi thread 0
----------------------------------------------------
source::equi::1::i=2 (00000000000000000000000000000010)
State 53 file source.c line 95 function equi thread 0
----------------------------------------------------
source::equi::1::right=4261474304 (0000000000000000000000000000000011111110000000001111000000000000)
State 54 file source.c line 94 function equi thread 0
----------------------------------------------------
source::equi::1::i=3 (00000000000000000000000000000011)
State 59 file source.c line 99 function equi thread 0
----------------------------------------------------
source::equi::1::i=1 (00000000000000000000000000000001)
State 61 file source.c line 100 function equi thread 0
----------------------------------------------------
source::equi::1::left=1052770304 (0000000000000000000000000000000000111110110000000000000000000000)
State 62 file source.c line 101 function equi thread 0
----------------------------------------------------
source::equi::1::right=1019277312 (0000000000000000000000000000000000111100110000001111000000000000)
Nieznane
funkcje
int equi( int A[], int n )
{
if( n <= 0 )
return -1;
int total = sum( A, n );
double lhs = 0.0, rhs = total;
unsigned int i;
for( i = 0; i < n; ++i )
{
rhs -= A[i];
if( fabs(rhs - lhs) < 1e-6 )
return i;
lhs += A[i];
}
return -1;
}
Spełnialność ?
int equi ( int A[], int n ) {
if (n <= 0)
return -1;
int i,j,k;
unsigned long long left = 0;
unsigned long long right = 0;
for (i = 1 ; i < n ; ++i) {
right += A[i];
}
if (left == right)
return 0;
for (i = 1; i < n; ++i) {
left += A[i - 1];
right -= A[i];
if (left == right)
return i;
}
return -1;
}
Kontrprzykład
(traceback)
Counterexample:
State 2 file source.c line 11 thread 0
----------------------------------------------------
arr=NULL
State 3 file source.c line 12 thread 0
----------------------------------------------------
n=0 (00000000000000000000000000000000)
State 4 file /usr/include/stdio.h line 165 thread 0
----------------------------------------------------
stdin=NULL
State 5 file /usr/include/stdio.h line 166 thread 0
----------------------------------------------------
stdout=NULL
State 6 file /usr/include/stdio.h line 167 thread 0
----------------------------------------------------
stderr=NULL
State 7 file /usr/include/bits/sys_errlist.h line 27 thread 0
----------------------------------------------------
sys_nerr=0 (00000000000000000000000000000000)
State 8 file line 19 thread 0
----------------------------------------------------
__CPROVER_alloc={ [3]=FALSE }
State 9 file line 20 thread 0
----------------------------------------------------
__CPROVER_alloc_size={ [3]=0 }
State 10 file line 29 thread 0
----------------------------------------------------
__CPROVER_rounding_mode=0 (00000000000000000000000000000000)
State 13 thread 0
----------------------------------------------------
c::argv'=(assignment removed)
State 17 file source.c line 23 function main thread 0
----------------------------------------------------
n=1073741826 (01000000000000000000000000000010)
State 19 file source.c line 25 function main thread 0
----------------------------------------------------
c::main::$tmp::return_value_malloc$1=&dynamic_1_array[0]
State 21 file source.c line 25 function main thread 0
----------------------------------------------------
__CPROVER_alloc_size={ [3]=1073741826 }
State 22 file source.c line 25 function main thread 0
----------------------------------------------------
__CPROVER_alloc={ [3]=TRUE }
State 23 file source.c line 25 function main thread 0
----------------------------------------------------
arr=&dynamic_1_array[0]
State 24 file source.c line 28 function main thread 0
----------------------------------------------------
source::main::1::1::i=0 (00000000000000000000000000000000)
0
State 27 file source.c line 28 function main thread 0
----------------------------------------------------
source::main::1::1::i=1 (00000000000000000000000000000001)
0
State 31 file source.c line 28 function main thread 0
----------------------------------------------------
source::main::1::1::i=2 (00000000000000000000000000000010)
0
State 35 file source.c line 28 function main thread 0
----------------------------------------------------
source::main::1::1::i=3 (00000000000000000000000000000011)
402653444
State 39 file source.c line 28 function main thread 0
----------------------------------------------------
source::main::1::1::i=4 (00000000000000000000000000000100)
Violated property:
file source.c line 28 function main
unwinding assertion loop 0
VERIFICATION FAILED
int equi ( int A[], int n ) {
long long i;
long long j;
long long a, b;
a = 0;
b = 0;
for(i = 0; i < n; i++) {
b = 0;
for(j = i + 1; j < n; j++)
b += A[j];
if(a == b)
return i;
a += A[i];
}
return -1;
}
int equi ( int A[], int n ) {
float sum = 0;
int i = 0;
for (i = 0; i < n; i++)
{
sum += A[i];
}
float left = 0;
float right = sum;
float val = 0;
i = 0;
for (i = 0; i < n; i++)
{
val = A[i];
right = right - val;
if (left == right)
return i;
else
left = left + val;
}
return -1;
}
Słaba
wydajność
Błędy
parsowania
int equi ( int A[], int n ) {
int sumlow(int A[], int k){
int i, sumaL = 0;
for(i = 0; i < k; ++i) sumaL+=A[i];
return sumaL;
}
int sumhi(int A[], int n, int k){
int i, sumaH = 0;
for(i = k; i < n; ++i) sumaH+=A[i];
return sumaH;
}
int j=0;
for(j=0; j < n; j++){
if (sumlow(A, j) == sumhi(A,n,j+1)) return j;
}
return -1;
}
Niepotwierdzony kontrprzykład
[-268435456, 8]
Kontrprzykład
int equi ( int A[], int n ) {
long long int low = 0;
long long int high = 0;
int i;
for(i=0; i<n; ++i){
high+=A[i];
}
for(i=0; i<n; ++i){
if(low + A[i] == high){
return i;
}
low += 2*A[i];
}
return -1;
}
234 (8.1%)
a = 34, b = 2
Niepotwierdzony
kontrprzykład
34 (5.8%)
[2014818472, 275785409, 2014818472]
Brak
kontrprzykładu
Kontrprzykład
int maxRS ( int A[], int n ) {
int count=1, ii=0, pi=0, i, countp=0;
if (n==0)
return -1;
for (i=1;i<n;i++) {
if (A[i]>A[i-1])
count++;
else {
if (countp<count) {
pi=ii;
countp=count;
}
count=0;
ii=i;
}
}
return (count>=countp)?ii:pi;
}
int add(int a, int b) {
return a + b;
}
int add(int a, int b) {
while (--b)
++a;
return a;
}
105 (3.6%)
[20, 16, 1024, 0]
35 (5.9%)
35
36
DOWÓD NIERÓWNOWAŻNOŚCI
Złe rozwiązania
Dobre rozwiązania
522 (88.3%)
2542 (88.2%)
Brak kontrprzykładu
Kontrprzykład
Brak wydajności
Błędy
parsowania
Poprawność
int equi ( int A[], int n ) {
int x;
long long left=0,right=0;
for(x = 0; x < n; right += (long long)A[x++]);
for(x = 0; x < n; x++) {
right -= (long long)A[x];
if(left == right)
return x;
left += (long long)A[x];
}
return left != right ? -1 : (n-1);
}
int equi ( int A[], int n ) {
long long lsum = 0;
long long rsum = 0;
int i;
for ( i=0 ; i<n ; i++)
rsum+= A[i];
for ( i=0 ; i<n ; i++)
{
if (i != 0)
lsum += A[i-1];
rsum -= A[i];
if ( lsum==rsum )
return i;
}
return -1;
}
[-12, 12]