Extraction to OCaml + OCaml wrapper code

src/AsyncDisk.v

@@ -4,12 +4,14 @@ Require Import List.
 Require Import Mem.
 Require Import Eqdep_dec.
 Require Import FunctionalExtensionality.
+Require Import String.
+Require HexString.
 
 Set Implicit Arguments.
 
 (* Disk value and address types  *)
 
-Notation "'valubytes_real'" := (4 * 1024)%nat. (* 4KB *)
+Notation "'valubytes_real'" := (HexString.to_nat "0x1000"). (* 4KB *)
 Notation "'valulen_real'" := (valubytes_real * 8)%nat.
 
 Module Type VALULEN.

src/Dir.v

@@ -25,14 +25,15 @@ Require Import AsyncDisk.
 Require Import Errno.
 Require Import DestructVarname.
 Import ListNotations.
+Require HexString.
 
 Set Implicit Arguments.
 
 
 
 Module DIR.
 
-  Definition filename_len := (1024 - addrlen - addrlen).
+  Definition filename_len := (HexString.to_nat "0x400" (* 1024 *) - addrlen - addrlen).
   Definition filename := word filename_len.
 
 

src/ExtractOcaml.v

@@ -2,18 +2,26 @@ Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlString.
 Require Import ExtrOcamlNatBigInt.
 Require Import ExtrOcamlZBigInt.
-Require Import FS.
-Require Import Testprog.
+Require Import AsyncFS.
+Require DirName.
 
-Extraction Language Ocaml.
+Extraction Language OCaml.
 
 (* Avoid conflicts with existing Ocaml module names. *)
-Extraction Blacklist String List Nat Array Bytes.
+Extraction Blacklist String List Nat Array Bytes Int.
 
 (* Optimize away some noop-like wrappers. *)
-Extraction Inline Prog.progseq.
 Extraction Inline Prog.pair_args_helper.
 
+(* Variables are just integers in the interpreter. *)
+Extract Inlined Constant Prog.vartype => "int".
+Extract Inlined Constant Prog.vartype_eq_dec => "(=)".
+
+(* Help eliminate the axiom (not used in executable code) *)
+Extract Constant AsyncDisk.hash_fwd => "(fun _ _ -> assert false)".
+Extract Constant AsyncDisk.default_hash => "(fun _ -> assert false)".
+Extract Constant AsyncDisk.hashmap_get => "(fun _ _ -> assert false)".
+
 (* Optimize away control flow constructs. *)
 Extraction Inline BasicProg.If_.
 
@@ -31,13 +39,22 @@ Extract Constant Nat.min => "Big.min".
 Extract Constant Nat.div => "fun n m -> if Big.eq m Big.zero then Big.zero else Big.div n m".
 Extract Constant Nat.modulo => "fun n m -> if Big.eq m Big.zero then Big.zero else Big.modulo n m".
 
+(* Integer parsing *)
+Require HexString.
+Extract Inlined Constant HexString.to_nat => "(fun l -> Z.of_string (String.of_seq (List.to_seq l)))".
+
+(* tail recursive list functions *)
+Extract Inlined Constant Datatypes.app => "List_extra.append".
+Extract Inlined Constant List.repeat => "List_extra.repeat".
+
 (* Hook up our untrusted replacement policy. *)
-Extract Inlined Constant Cache.eviction_state  => "unit".
-Extract Inlined Constant Cache.eviction_init   => "()".
-Extract Inlined Constant Cache.eviction_update => "(fun state addr -> state)".
-Extract Inlined Constant Cache.eviction_choose => "(fun state -> (Word.wzero Prog.addrlen, state))".
-Extract Constant FS.cachesize => "(Big.of_int 10000)".
+Extract Inlined Constant Cache.eviction_state  => "Evict.eviction_state".
+Extract Inlined Constant Cache.eviction_init   => "Evict.eviction_init".
+Extract Inlined Constant Cache.eviction_update => "Evict.eviction_update".
+Extract Inlined Constant Cache.eviction_choose => "Evict.eviction_choose".
+
+Extract Inlined Constant Log.should_flushall => "false".
 
 Cd "../codegen".
-Recursive Extraction Library FS.
-Recursive Extraction Library Testprog.
+Recursive Extraction Library DirName.
+Recursive Extraction Library AsyncFS.

src/Inode.v

@@ -105,14 +105,15 @@ Module INODE.
     Definition IRBlocks  (x : irec) := Eval compute_rec in ( x :-> "blocks").
     Definition IRAttrs   (x : irec) := Eval compute_rec in ( x :-> "attrs").
 
-    Definition upd_len (x : irec) v  := Eval compute_rec in (x :=> "len" := $ v).
-
-    Definition upd_irec (x : irec) len ibptr dibptr tibptr dbns := Eval compute_rec in
-      (x :=> "len" := $ len
-         :=> "indptr" := $ ibptr
-         :=> "dindptr" := $ dibptr
-         :=> "tindptr" := $ tibptr
-         :=> "blocks" := dbns).
+    Definition upd_len (x : irec) v : irec := Eval compute_rec in (x :=> "len" := $ v).
+
+    Definition upd_irec (x : irec) len ibptr dibptr tibptr dbns : irec :=
+      Eval compute_rec in
+        (x :=> "len" := $ len
+           :=> "indptr" := $ ibptr
+           :=> "dindptr" := $ dibptr
+           :=> "tindptr" := $ tibptr
+           :=> "blocks" := dbns).
 
     (* getter/setter lemmas *)
     Fact upd_len_get_len : forall ir n,

src/Makefile

@@ -1,8 +1,3 @@
-OCAMLBUILD := env OCAMLPATH=$(shell pwd) ocamlbuild \
-	      -tag thread -tag debug -use-ocamlfind \
-	      -lib str -lib nums \
-	      -I codegen -I mllib -X ocamlfuse \
-	      -package extunix -package zarith -package ocamlfuse
 MODULES    := Lock Nomega Word WordAuto WordZ Bytes Rounding \
 				Mem AsyncDisk Pred Prog ProgMonad PredCrash Hoare \
 				OperationalSemantics \
@@ -46,55 +41,15 @@ HSLIB_FUSE := hscgen/Fuse.hs hslib/libopfuse.a
 HSLIB_PRE  := hslib/Word.hs hslib/Evict.hs hslib/Profile.hs
 HSLIB_POST := hslib/Disk.hs hslib/Interpreter.hs
 
-OCAMLFUSE_ML	:= ocamlfuse/Result.ml \
-		   ocamlfuse/Unix_util.ml \
-		   ocamlfuse/Fuse_bindings.ml \
-		   ocamlfuse/Fuse_lib.ml \
-		   ocamlfuse/Fuse.ml
-OCAMLFUSE_MLI	:= ocamlfuse/Fuse.mli \
-		   ocamlfuse/Fuse_bindings.mli
-
-OCAMLFUSE_CMX	:= $(patsubst %.ml,%.cmx,$(OCAMLFUSE_ML))
-OCAMLFUSE_DEP	:= $(patsubst %.ml,%.d,$(OCAMLFUSE_ML)) \
-		   $(patsubst %.mli,%.di,$(OCAMLFUSE_MLI))
-OCAMLFUSE	:= ocamlfuse/Fuse.a ocamlfuse/Fuse.cmxa
-
 .PHONY: coq proof clean
 
 all: fscq mkfs
 
--include $(OCAMLFUSE_DEP)
-
-%.mli %.ml %_stubs.c: %.idl
-	camlidl -header $<
-
-%.d: %.ml
-	ocamldep $< > $@
-
-%.di: %.mli
-	ocamldep $< > $@
-
-ocamlfuse/%.o: ocamlfuse/%.c
-	ocamlc -c -ccopt '-fPIC -D_FILE_OFFSET_BITS=64 -I. -pthread -DPIC -DNATIVE_CODE -o $@' $<
-
-ocamlfuse/libFuse_stubs.a: ocamlfuse/Fuse_bindings_stubs.o ocamlfuse/Unix_util_stubs.o ocamlfuse/Fuse_util.o
-	ar rcs $@ $^
-
-%.cmx: %.ml
-	ocamlopt -I ocamlfuse -c -thread $<
-
-%.cmi: %.mli
-	ocamlopt -I ocamlfuse -c -thread $<
-
-ocamlfuse/Fuse.cmxa ocamlfuse/Fuse.a: $(OCAMLFUSE_CMX) ocamlfuse/libFuse_stubs.a
-	ocamlopt -a -thread -linkall -cclib -lFuse_stubs -cclib -lfuse -cclib -lcamlidl -o $@ $(OCAMLFUSE_CMX)
+mlbin/mkfs.exe: mlbin/mkfs.ml $(VS_ML) $(wildcard mllib/*.ml)
+	dune build $@
 
-%: %.ml $(VS_ML) $(wildcard */*.ml) $(OCAMLFUSE)
-	rm -f $@
-	-mv codegen/Word.ml codegen/WordCoq.ml
-	-mv codegen/Word.mli codegen/WordCoq.mli
-	$(OCAMLBUILD) -no-links $@.native
-	ln -s $(CURDIR)/_build/$@.native $@
+mlbin/fscqfuse.exe: mlbin/fscqfuse.ml $(VS_ML) $(wildcard mllib/*.ml)
+	dune build $@
 
 hscgen/%.hs: hslib/%.hsc
 	@mkdir -p $(@D)
@@ -113,13 +68,14 @@ $(VS_HS): $(VS_VIO) coqbuild/ExtractHaskell.v
 
 $(VS_ML): $(VS_VIO) coqbuild/ExtractOcaml.v
 	( cd coqbuild && coqc -q -R . Fscq ExtractOcaml.v )
+	mv codegen/Word.ml codegen/.WordCoq.ml
+	mv codegen/Word.mli codegen/.WordCoq.mli
 
 $(VS_JSON): $(VS_VIO) coqbuild/ExtractJSON.v
 	( cd coqbuild && coqc -q -R . Fscq ExtractJSON.v )
 
 $(VS_VIO): coqbuild/Makefile.coq
-	( cd coqbuild && $(MAKE) -j $(J) -f Makefile.coq quick )
-	@touch coqbuild/*.vio
+	( cd coqbuild && $(MAKE) -j $(J) -f Makefile.coq vio )
 
 checkproofs: coqbuild/Makefile.coq
 	( cd coqbuild && $(MAKE) -f Makefile.coq checkproofs J=$(J) )
@@ -157,10 +113,8 @@ hslib/libopfuse.a: hslib/opqueue.o hslib/opfuse.o
 
 clean:
 	rm -rf codegen coqbuild _build fstest hstest gotest disk.img \
-	       fscq mkfs *.o *.hi ocamlfuse/*.d ocamlfuse/*.di \
-	       ocamlfuse/*.cmi ocamlfuse/*.cmx ocamlfuse/*.cmo \
-	       ocamlfuse/*.o ocamlfuse/Fuse_bindings_stubs.c \
-	       ocamlfuse/Fuse_bindings.h ocamlfuse/Fuse_bindings.ml \
-	       ocamlfuse/libFuse_stubs.a hslib/*.o hscgen
+	       fscq mkfs *.o *.hi \
+	       hslib/*.o hscgen \
+	       mlbin/*.exe
 
 .PRECIOUS: hscgen/%.hs %_stubs.c

src/MemLog.v

@@ -1,3 +1,4 @@
+Require Import String.
 Require Import Hashmap.
 Require Import Arith.
 Require Import Bool.

src/SuperBlock.v

@@ -12,6 +12,7 @@ Require Import Cache.
 Require Import AsyncDisk.
 Require Import Omega.
 Require Import FSLayout.
+Require HexString.
 
 Import ListNotations.
 Set Implicit Arguments.
@@ -20,7 +21,8 @@ Module SB.
 
   Local Hint Resolve goodSize_add_l goodSize_add_r.
 
-  Definition magic_number := # (natToWord addrlen 3932).  (* 0xF5C = FSC in C *)
+  Definition magic_number :=
+    # (natToWord addrlen (HexString.to_nat "0xF5C")).  (* 0xF5C = FSC in C *)
 
   Definition superblock_type : Rec.type := Rec.RecF ([
       ("data_start",  Rec.WordF addrlen);

src/dune-project

@@ -0,0 +1 @@
+(lang dune 2.0)

src/mlbin/dune

@@ -0,0 +1,13 @@
+(executable
+ (name mkfs)
+ (libraries fscq zarith)
+ (modules mkfs)
+ (promote (until-clean))
+)
+
+(executable
+ (name fscqfuse)
+ (libraries fscq fuse fpath)
+ (modules fscqfuse)
+ (promote (until-clean))
+)