Commit d6d225e0 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Merge branch 'array_extraction' into 'master'

Extraction of C arrays

See merge request !88
parents 7b4155e8 c24a53f7
......@@ -548,7 +548,12 @@ static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
end
module mach.array.Array32
syntax val ([]) "%1[%2]"
syntax val ([]<-) "%1[%2] = %3"
end
module mach.c.C
......
ptrcursor.[co]
\ No newline at end of file
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../bin/why3.opt
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
endif
clean:
rm -rf build
dir:
mkdir -p build
why3:
make -C ../..
extract: why3 dir
$(WHY3) extract -D cursor.drv -D c -L . -o build/ptrcursor.c ccursor.PtrCursor
cfiles: extract
gcc -Wall -g -pedantic -Wno-unused-function -std=c11 build/ptrcursor.c -Ibuild -o build/tests
tests: cfiles
./build/tests
module PtrCursor
use int.Int
use map.MapEq
use mach.int.Int32
use mach.c.C
use array.Array
(* we assume that a non-null pointer exists *)
val ghost dummy_nonnull () : ptr int32
ensures { is_not_null result /\ plength result = 1 /\ offset result = 0 }
ensures { min result = 0 /\ max result = plength result }
ensures { (data result)[0] = 0 }
type cursor = {
current : ptr int32;
mutable new : bool;
len : int32;
ghost mutable freed : bool;
bound : int32
}
invariant { 0 < len }
invariant { not freed ->
(plength current = len /\
offset current = 0 /\
valid current len /\
min current = 0 /\
max current = len /\
is_not_null current /\
forall i. 0 <= i < len -> (data current)[i] < bound) }
by { current = dummy_nonnull (); new = true;
len = 1; freed = false; bound = 42 }
val ([]) (a: array 'a) (i: int32) : 'a
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { result = ([]) a i }
val ([]<-) (a: array 'a) (i: int32) (v: 'a) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { a.elts = Map.set (old a).elts i v }
ensures { a = ([<-]) (old a) i v }
let partial create_cursor (l:int32) (b: int32) : cursor
requires { 0 < l }
requires { 0 < b }
ensures { result.len = l }
ensures { not result.freed }
ensures { forall i. 0 <= i < l -> (data result.current)[i] = 0 }
ensures { bound result = b }
= let a = malloc (UInt32.of_int32 l) in
c_assert (is_not_null a);
for i = 0 to l-1 do
invariant { forall j. 0 <= j < i -> (data a)[j] = 0 }
set_ofs a i 0;
done;
{ current = a; new = true; len = l; freed = false; bound = b }
let free_cursor (c:cursor) : unit
requires { not c.freed }
ensures { c.freed }
writes { c.freed }
writes { c.current }
writes { c.current.data }
= free c.current;
c.freed <- true
val get_current (c:cursor) : array int32
requires { not c.freed }
ensures { length result = plength c.current }
ensures { map_eq_sub result.elts (pelts c.current) 0 c.len }
alias { c.current.data with result }
let next (c: cursor) : unit
requires { not c.freed }
requires { 0 < c.bound < max_int32 }
= let a = get_current c in
label L in
let n = c.len in
let b = c.bound in
let ref r = (n-1) in
while r >= 0 && a[r] = b - 1 do
invariant { -1 <= r < n }
invariant { forall s. r < s < c.len -> a[s] = b - 1 }
variant { r }
r <- r - 1
done;
if (r < 0) then
c.new <- false
else begin
a[r] <- a[r] + 1;
assert { a[r] < b };
for i = r+1 to n-1 do
invariant { forall j. r+1 <= j < i -> a[j] = 0 }
invariant { forall j. 0 <= j < r -> a[j] = a[j] at L }
invariant { a[r] = a[r] at L + 1 }
a[i] <- 0
done;
c.new <- true;
end
let main () : int32
= let c = create_cursor 4 4 in
for i = 0:int32 to 255 do
invariant { not c.freed }
invariant { forall i. 0 <= i < c.len -> (data c.current)[i] < c.bound }
c_assert c.new;
next c;
done;
c_assert (not c.new);
free_cursor c;
0
end
\ No newline at end of file
This diff is collapsed.
module ccursor.PtrCursor
syntax val ([]) "%1[%2]"
syntax val ([]<-) "%1[%2] = %3"
syntax val get_current "%1->current"
end
\ No newline at end of file
This diff is collapsed.
......@@ -12,7 +12,7 @@ module Array
use int.Int
use map.Map
type array 'a = private {
type array [@ex:array] 'a = private {
mutable ghost elts : int -> 'a;
length : int
} invariant { 0 <= length }
......@@ -49,7 +49,7 @@ module Array
= if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v
val function make (n: int) (v: 'a) : array 'a
val function make [@ex:array_make] (n: int) (v: 'a) : array 'a
requires { [@expl:array creation size] n >= 0 }
ensures { forall i:int. 0 <= i < n -> result[i] = v }
ensures { result.length = n }
......
......@@ -12,7 +12,7 @@ module Array32
use mach.int.Int32
use map.Map as M
type array 'a = private {
type array [@ex:array] 'a = private {
mutable ghost elts : int -> 'a;
length : int32;
} invariant { 0 <= length }
......@@ -45,7 +45,7 @@ module Array32
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
val make (n: int32) (v: 'a) : array 'a
val make [@ex:array_make] (n: int32) (v: 'a) : array 'a
requires { [@expl:array creation size] n >= 0 }
ensures { forall i:int. 0 <= i < n -> result[i] = v }
ensures { result.length = n }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment