Commit 38d59aeb authored by charguer's avatar charguer
Browse files
parents 0207232e ee37c5b6
open Mytools
(*#########################################################################*)
(* ** Helper function to decompose Coq paths *)
let rec split_at_dots s pos =
try
let dot = String.index_from s pos '.' in
String.sub s pos (dot - pos) :: split_at_dots s (dot + 1)
with Not_found ->
[String.sub s pos (String.length s - pos)]
let name_of_mlpath s =
List.hd (List.rev (split_at_dots s 0))
(*#########################################################################*)
(* ** List of inlined primitives *)
(** Fully-applied "inlined primitive" are translated directly as a
Coq application, and does not involve the "AppReturns" predicate. *)
let primitive_special = -1
let inlined_primitives_table =
["Pervasives.+", (2, "Coq.ZArith.BinInt.Zplus");
"Pervasives.-", (2, "Coq.ZArith.BinInt.Zminus");
"Pervasives.*", (2, "Coq.ZArith.BinInt.Zmult");
"Pervasives.~-", (1, "Coq.ZArith.BinInt.Zopp");
"Pervasives.&&", (2, "LibBool.and");
"Pervasives.||", (2, "LibBool.or");
(*
"Pervasives./", (primitive_special, "Coq.ZArith.Zdiv.Zdiv");
"Pervasives.mod", (primitive_special, "Coq.ZArith.Zdiv.Zmod");
*)
(* TEMPORARY the following 8 primitives should be limited to certain types! *)
"Pervasives.=", (2, "(fun _y _z => isTrue (_y = _z))");
"Pervasives.<>", (2, "(fun _y _z => isTrue (_y <> _z))");
"Pervasives.<", (2, "(fun _y _z => isTrue (_y < _z))");
"Pervasives.<=", (2, "(fun _y _z => isTrue (_y <= _z))");
"Pervasives.>", (2, "(fun _y _z => isTrue (_y > _z))");
"Pervasives.>=", (2, "(fun _y _z => isTrue (_y >= _z))");
"Pervasives.max", (2, "Zmax");
"Pervasives.min", (2, "Zmin");
"Pervasives.not", (1, "LibBool.neg");
"Pervasives.fst", (1, "(@fst _ _)");
"Pervasives.snd", (1, "(@snd _ _)");
"Pervasives.@", (2, "LibList.append");
"List.rev", (1, "LibList.rev");
"List.length", (1, "LibList.length");
"List.append", (2, "LibList.append");
"OkaStream.++", (2, "LibList.append");
"OkaStream.reverse", (1, "LibList.rev");
"Lazy.force", (1, ""); (* i.e., @LibLogic.id _*)
"Okasaki.!$", (1, ""); (* i.e., @LibLogic.id _*)
"StrongPointers.cast", (1, "")
]
(* --todo: add asr, etc.. *)
(*#########################################################################*)
(* ** List of all primitives *)
(** Primitive functions from the following list are mapped to special
Coq constants whose specification is axiomatized. *)
let all_primitives_table =
[ "Pervasives.=", "ml_eqb";
"Pervasives.<>", "ml_neq";
"Pervasives.==", "ml_phy_eq";
"Pervasives.!=", "ml_phy_neq";
"Pervasives.+", "ml_plus";
"Pervasives.-", "ml_minus";
"Pervasives.~-", "ml_opp";
"Pervasives.*", "ml_mul";
"Pervasives./", "ml_div";
"Pervasives.mod", "ml_mod";
"Pervasives.<=", "ml_leq";
"Pervasives.<", "ml_lt";
"Pervasives.>", "ml_gt";
"Pervasives.>=", "ml_geq";
"Pervasives.&&", "ml_and";
"Pervasives.||", "ml_or";
"Pervasives.@", "ml_append";
"Pervasives.raise", "ml_raise";
"Pervasives.land", "ml_land";
"Pervasives.lor", "ml_lor";
"Pervasives.lxor", "ml_lxor";
"Pervasives.lnot", "ml_lnot";
"Pervasives.lsl", "ml_lsl";
"Pervasives.lsr", "ml_lsr";
"Pervasives.asr", "ml_asr";
"Pervasives.ref", "ml_ref";
"Pervasives.!", "ml_get";
"Pervasives.:=", "ml_set";
"Pervasives.incr", "ml_incr";
"Pervasives.decr", "ml_decr";
"Pervasives.fst", "ml_fst";
"Pervasives.snd", "ml_snd";
"Pervasives.max_int", "ml_max_int";
"Pervasives.min_int", "ml_min_int";
"Pervasives.read_int", "ml_read_int";
"Pervasives.print_int", "ml_print_int";
"Sys.max_array_length", "ml_max_array_length";
"Random.int", "ml_rand_int";
"List.nth", "ml_list_nth";
"List.hd", "ml_list_hd";
"List.tl", "ml_list_tl";
"List.iter", "ml_list_iter";
"List.fold_left", "ml_list_fold_left";
"List.fold_right", "ml_list_fold_right";
"List.rev", "ml_rev";
"List.append", "ml_append";
"Stack.create", "ml_stack_create";
"Stack.is_empty", "ml_stack_is_empty";
"Stack.push", "ml_stack_push";
"Stack.pop", "ml_stack_pop";
"OkaStream.append", "ml_append";
"OkaStream.take", "ml_take";
"OkaStream.drop", "ml_drop";
"NullPointers.null", "null";
"NullPointers.is_null", "ml_is_null";
"NullPointers.free", "ml_free";
"StrongPointers.sref", "ml_ref";
"StrongPointers.sget", "ml_get";
"StrongPointers.sset", "ml_sset"; ]
(* ---todo: add not, fst, snd *)
(*#########################################################################*)
(* ** List of primitive data constructors *)
(** Data constructors from the following lists are mapped to particular
inductive data constructors in Coq. *)
let builtin_constructors_table =
[ "[]", ("Coq.Lists.List.nil", 1);
"::", ("Coq.Lists.List.cons", 1);
"()", ("Coq.Init.Datatypes.tt", 0);
"true", ("Coq.Init.Datatypes.true", 0);
"false", ("Coq.Init.Datatypes.false", 0);
]
(* --todo: add [Pervasives] as prefix *)
(*#########################################################################*)
(* ** Accessor functions *)
(** Find the inlined primitive associated with [p] of arity [arity] *)
let find_inlined_primitive p arity =
match list_assoc_option p inlined_primitives_table with
| None -> None
| Some (n,y) -> if n = arity then Some y else None
(** Test whether [p] is an inlined primitive of arity [arity] *)
let is_inlined_primitive p arity =
find_inlined_primitive p arity <> None
(** Temporary: test only base on the last part of the name *)
let is_inlined_primitive_hack p arity =
let t = List.map (fun (x,(n,y)) -> name_of_mlpath x, (n,y)) inlined_primitives_table in
match list_assoc_option p t with
| None -> false
| Some (n,y) -> (arity = n)
(** Find the primitive associated with [p]. This partial function
returns an option. *)
let find_primitive p =
list_assoc_option p all_primitives_table
(** Find the primitive data-constructor associated with [p].
This partial function returns an option. *)
let find_builtin_constructor p =
list_assoc_option p builtin_constructors_table
(** List of special top-level definitions that should not lead
to the generation of a characteristic formula. The definition
of [!$] as a keyword for forcing lazy expressions is one such
exception. *)
let hack_recognize_okasaki_lazy = function
| "!$" -> true
| _ -> false
(** List of special modules whose [open] should not lead to the
generation of an [Require Import] statement. *)
let is_primitive_module n =
List.mem n [ "NullPointers"; "StrongPointers" ]
(* ; "Okasaki"; "OkaStream" *)
(* Special construction for [|v1; .. ; vN|], encoded as
Array.make_from_list [v1; .. ; vN]. *)
external make_from_list : 'a list -> 'a array = "%array_make_from_list"
(* Special case for [||], needed to implement this file. *)
let make_empty () = make_from_list []
(* Alternative:
external make_empty : unit -> 'a array = "%array_make_empty"
(* This file is a copy of [array.ml], with different [external] declarations,
because:
- we must axiomatize the functions that cannot be implemented in OCaml;
- and only those.
*)
external make : int -> 'a -> 'a array = "%array_make"
(* A literal array [|v1; .. ; vN|] is encoded by CFML as
[of_list [v1; .. ; vN]].
This requires us to make [of_list] a primitive function. *)
external of_list : 'a list -> 'a array = "%array_of_list"
external length : 'a array -> int = "%array_length"
(* [unsafe_get] and [unsafe_set] intentionally omitted, at least for now. *)
external length : 'a array -> int = "%array_length"
external get : 'a array -> int -> 'a = "%array_get"
external set : 'a array -> int -> 'a -> unit = "%array_set"
external make : int -> 'a -> 'a array = "%array_make"
(* [make_float] omitted. *)
let init n f =
assert (n >= 0);
if n = 0 then make_empty() else begin
if n = 0 then of_list [] else begin
let res = make n (f 0) in
for i = 1 to pred n do
set res i (f i)
......@@ -32,22 +29,11 @@ let init n f =
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
let fill a start nb v =
assert (not (start < 0 || nb < 0 || start > length a - nb));
for i = start to pred (start + nb) do
set a i v;
done
let blit a1 start1 a2 start2 nb =
assert (not (nb < 0 || start1 < 0 || start1 > length a1 - nb
|| start2 < 0 || start2 > length a2 - nb));
for i = 0 to pred nb do
set a2 (start2 + i) (get a1 (start1 + i));
done
(* [make_matrix] omitted. *)
let copy a =
let n = length a in
if n = 0 then make_empty() else begin
if n = 0 then of_list [] else begin
let r = make (length a) (get a 0) in
for i = 0 to pred n do
set r i (get a i);
......@@ -55,10 +41,11 @@ let copy a =
r
end
(* Re-implementation of [append]. *)
let append a1 a2 =
let n1 = length a1 in
let n2 = length a2 in
if n1 = 0 && n2 = 0 then make_empty() else begin
if n1 = 0 && n2 = 0 then of_list [] else begin
let d = (if n1 <> 0 then get a1 0 else get a2 0) in
let a = make (n1+n2) d in
for i = 0 to pred n1 do
......@@ -69,48 +56,65 @@ let append a1 a2 =
done;
a
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
external sub : 'a array -> int -> int -> 'a array = "caml_array_sub"
(*
(* NOTE: Improved original code below *)
(* TODO: Do we want to expose unsafe_sub ? *)
(* Re-implementation of [concat]. *)
let concat ts =
List.fold_left append (of_list []) ts
(* Re-implementation of [sub]. *)
let sub a ofs len =
assert (not (ofs < 0 || len < 0 || ofs > length a - len));
unsafe_sub a ofs len
*)
init len (fun i -> get a (ofs + i))
let iter f a =
for i = 0 to pred (length a) do
f (get a i)
let fill a start nb v =
assert (not (start < 0 || nb < 0 || start > length a - nb));
for i = start to pred (start + nb) do
set a i v;
done
let iteri f a =
for i = 0 to pred (length a) do
f i (get a i)
(* Re-implementation of [blit]. *)
(* TEMPORARY incorrect: should work also when [a1] and [a2] are the same array! *)
let blit a1 start1 a2 start2 nb =
assert (not (nb < 0 || start1 < 0 || start1 > length a1 - nb
|| start2 < 0 || start2 > length a2 - nb));
for i = 0 to pred nb do
set a2 (start2 + i) (get a1 (start1 + i));
done
let iter f a =
for i = 0 to pred (length a) do
f (get a i)
done
let map f a =
let n = length a in
if n = 0 then make_empty() else begin
if n = 0 then of_list [] else begin
let r = make n (f (get a 0)) in
for i = 1 to pred n do
set r i (f (get a i));
done;
r
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
let iteri f a =
for i = 0 to pred (length a) do
f i (get a i)
done
let mapi f a =
let n = length a in
if n = 0 then make_empty() else begin
if n = 0 then of_list [] else begin
let r = make n (f 0 (get a 0)) in
for i = 1 to pred n do
set r i (f i (get a i));
done;
r
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
let to_list a =
let rec tolist i res =
if i < 0 then res else tolist (i - 1) (get a i :: res) in
tolist (length a - 1) []
let fold_left f x a =
let r = ref x in
......@@ -119,14 +123,11 @@ let fold_left f x a =
done;
!r
(* TODO: add support for downto in CFML
let fold_right f a x =
let r = ref x in
for i = pred (length a) downto 0 do
r := f (get a i) !r
done;
!r
*)
(* [sort], [stable_sort], [fast_sort] omitted, for now. *)
Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml Pervasives_proof.
Require Export LibListZ.
Require Import Array_ml.
Generalizable Variables A.
(************************************************************)
(** Builtin *)
Parameter Array : forall A (L:list A) (l:loc), hprop.
Parameter make_from_list_spec : curried 2%nat make_from_list /\
forall A (L:list A),
app make_from_list [L] \[] (fun t => t ~> Array L).
Hint Extern 1 (RegisterSpec make_from_list) => Provide make_from_list_spec.
Lemma make_empty_spec : forall A,
app make_empty [tt] \[] (fun l => l ~> Array (@nil A)).
Proof using.
xcf. xgo.
Qed.
Hint Extern 1 (RegisterSpec make_empty) => Provide make_empty_spec.
Parameter make_spec : curried 2%nat make /\
forall A (n:int) (v:A),
n >= 0 ->
app make [n v] \[] (fun t =>
Hexists L, t ~> Array L \* \[L = LibListZ.make n v]).
Hint Extern 1 (RegisterSpec make) => Provide make_spec.
Lemma make_spec_direct : forall A (n:int) (v:A),
n >= 0 ->
app make [n v] \[] (fun l => l ~> Array (LibListZ.make n v)).
Proof using.
intros. xapp~.
Qed.
Parameter length_spec : curried 1%nat length /\
forall A (L:list A) (t:loc),
app_keep length [t] (t ~> Array L) (fun n => \[n = LibListZ.length L]).
Hint Extern 1 (RegisterSpec length) => Provide length_spec.
Parameter get_spec : curried 2%nat get /\
forall `{Inhab A} (L:list A) (t:loc) (i:int),
index L i ->
app_keep get [t i] (t ~> Array L) \[= L[i] ].
Hint Extern 1 (RegisterSpec get) => Provide get_spec.
Parameter set_spec : curried 2%nat set /\
forall A (L:list A) (t:loc) (i:int) (v:A),
index L i ->
app set [t i v] (t ~> Array L) (# t ~> Array (L[i:=v])).
Hint Extern 1 (RegisterSpec set) => Provide set_spec.
(* NOTE: Check if correct *)
Parameter sub_spec : curried 3%nat sub /\
forall `{Inhab A} (L : list A) (a : loc) (ofs len : int),
0 <= ofs ->
ofs <= len ->
len <= LibListZ.length L ->
app_keep sub [a ofs len]
(a ~> Array L)
(fun a' => Hexists L',
a' ~> Array L' \*
\[LibListZ.length L' = len - ofs] \*
\[forall i, ofs <= i < len -> L'[i] = L[i]]).
Hint Extern 1 (RegisterSpec sub) => Provide sub_spec.
Notation "'App'' r `[ i ]" := (App get r i;)
(at level 69, r at level 0, no associativity,
format "'App'' r `[ i ]") : charac.
Notation "'App'' r `[ i ] `<- v" := (App set r i v;)
(at level 69, r at level 0, no associativity,
format "'App'' r `[ i ] `<- v") : charac.
(************************************************************)
(************************************************************)
(************************************************************)
(** FUTURE
(** The model of an imperative array is a sequence, represented as a list *)
Definition array (A:Type) := list A.
Parameter ArrayOf : forall a A (T:htype A a) (M:array A) (l:loc), hprop.
Notation "'Array'" := (ArrayOf Id).
Require Import LibBag.
(* -- with credits ---*)
Set Implicit Arguments.
Require Export LibInt LibListZ CFSpec CFPrint CFPrimSpec.
Generalizable Variables a A.
Parameter array_make_cst : nat.
Parameter ml_array_make_spec_direct : forall a,
Spec ml_array_make (n:int) (v:a) |R>>
R (\$ (abs n * array_make_cst))
(fun l => l ~> Array (make n v)).
Parameter ml_array_make_spec : forall a,
Spec ml_array_make (n:int) (v:a) |R>>
n >= 0 ->
R (\$ (abs n * array_make_cst))
(fun l => Hexists M, l ~> Array M \* \[M = make n v]).
Hint Extern 1 (RegisterSpecCredits ml_array_make) => Provide ml_array_make_spec.
*)
Require Import LibListZ.
Require Sys_ml.
Require Array_ml.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* TODO: merge *)
(*
Set Implicit Arguments.
Require Import LibListZ LibMap LibInt.
Require Import CFSpec CFPrint CFPrim.
Require Array_ml.
Section Array.
(* Conventions. *)
Variable A : Type.
Implicit Types t : loc. (* array *)
Implicit Types i ofs len : int. (* index *)
(* -------------------------------------------------------------------------- *)
(* The model of an imperative array is a sequence, represented as a list. *)
(* An ad hoc notation for array accesses in OCaml code. For display only. *)
Parameter Array : list A -> loc -> hprop.
Notation "'App'' t `[ i ]" := (App Array_ml.get t i;)
(at level 69, t at level 0, no associativity,
format "'App'' t `[ i ]") : charac.
(* -------------------------------------------------------------------------- *)
Notation "'App'' t `[ i ] `<- x" := (App Array_ml.set t i x;)
(at level 69, t at level 0, no associativity,
format "'App'' t `[ i ] `<- x") : charac.
(* [Sys.max_array_length] is nonnegative. We do not guarantee anything more.
In reality, [Sys.max_array_length] is [2^22 - 1] on a 32-bit machine, and
[2^54 - 1] on a 64-bit machine. (10 bits are reserved in an array header,
the rest encodes the array length.) *)
(* -------------------------------------------------------------------------- *)
(* Ideally, we should guarantee that [Sys.max_array_length] is less than or
equal to [max_int]. This could be useful someday if we need to prove that
certain integer calculations cannot overflow. *)
(* The model of an imperative array is a sequence, represented as a list. *)
Parameter max_array_length_property:
0 <= ml_max_array_length.
Parameter Array : forall A, list A -> loc -> hprop.
(* -------------------------------------------------------------------------- *)
......@@ -170,111 +36,165 @@ Parameter max_array_length_property:
cannot overflow. *)
Parameter bounded_length:
forall l xs,
l ~> Array xs ==>
l ~> Array xs \* \[ length xs <= ml_max_array_length ].
forall A t (xs : list A),
t ~> Array xs ==>
t ~> Array xs \* \[ length xs <= Sys_ml.max_array_length ].
(* -------------------------------------------------------------------------- *)
(* [Array.make]. *)
(* [Array.length]. *)
(* In practice, the parameter [n] of [Array.make] must not exceed the constant
[Sys.max_array_length]. In the specification, we ignore this aspect, as it
would pollute the client quite severely, without a clear benefit. If someday
we decide to make this precondition explicit, then we should guarantee that
[Sys.max_array_length] is at least [2^22 - 1], as this will help prove that
it is safe to allocate arrays of known small size. *)
Parameter length_spec :
curried 1%nat Array_ml.length /\
forall A (xs:list A) t,
app_keep Array_ml.length [t]
(t ~> Array xs)
(fun n => \[n = length xs]).
Parameter make_spec :
Spec Array_ml.make n v |R>>
n >= 0 ->
R \[] (fun l => Hexists xs, l ~> Array xs \* \[ xs = make n v ]).
Hint Extern 1 (RegisterSpec Array_ml.length) => Provide length_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.get]. *)
Parameter get_spec :
Spec Array_ml.get l i |R>>
forall `{Inhab A} xs,
index xs i ->
keep R (l ~> Array xs) (fun x => \[ x = xs[i] ]).
curried 2%nat Array_ml.get /\
forall A `{Inhab A} (xs:list