diff --git a/src/AsyncDisk.v b/src/AsyncDisk.v index 593304e1..86e87fb6 100644 --- a/src/AsyncDisk.v +++ b/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. diff --git a/src/Dir.v b/src/Dir.v index f56eec01..70ae15d5 100644 --- a/src/Dir.v +++ b/src/Dir.v @@ -25,6 +25,7 @@ Require Import AsyncDisk. Require Import Errno. Require Import DestructVarname. Import ListNotations. +Require HexString. Set Implicit Arguments. @@ -32,7 +33,7 @@ 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. diff --git a/src/ExtractOcaml.v b/src/ExtractOcaml.v index 34b5aa58..ce5d9fd1 100644 --- a/src/ExtractOcaml.v +++ b/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. diff --git a/src/Inode.v b/src/Inode.v index 19756ca2..4209846e 100644 --- a/src/Inode.v +++ b/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, diff --git a/src/Makefile b/src/Makefile index 52ffa558..5d67c41b 100644 --- a/src/Makefile +++ b/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 diff --git a/src/MemLog.v b/src/MemLog.v index 0848f359..f3a966e4 100644 --- a/src/MemLog.v +++ b/src/MemLog.v @@ -1,3 +1,4 @@ +Require Import String. Require Import Hashmap. Require Import Arith. Require Import Bool. diff --git a/src/SuperBlock.v b/src/SuperBlock.v index e13ee048..6f32e913 100644 --- a/src/SuperBlock.v +++ b/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); diff --git a/src/dune-project b/src/dune-project new file mode 100644 index 00000000..929c696e --- /dev/null +++ b/src/dune-project @@ -0,0 +1 @@ +(lang dune 2.0) diff --git a/src/mlbin/dune b/src/mlbin/dune new file mode 100644 index 00000000..ebfcc248 --- /dev/null +++ b/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)) +) diff --git a/src/mlbin/fscqfuse.ml b/src/mlbin/fscqfuse.ml new file mode 100644 index 00000000..c9d771a1 --- /dev/null +++ b/src/mlbin/fscqfuse.ml @@ -0,0 +1,154 @@ +module Errno = Fscq.Errno +module FSLayout = Fscq.FSLayout +module AsyncFS = Fscq.AsyncFS.AFS +module Ops = Fscq.Operations + +let cachesize = Z.of_int 100_000 +(* there also are many hardcoded "4096" in the rest of the code.. *) +let blocksize = (Z.to_int Fscq.AsyncDisk.Valulen.valulen) / 8 + +type mscs = Fscq.BFile.BFILE.memstate +type fsxp = FSLayout.fs_xparams + +type state = { + ops : Fscq.Operations.state; + lock : Mutex.t; +} + +let mk_state (ops: Ops.state) : state = + { ops; lock = Mutex.create () } + +external reraise : exn -> 'a = "%reraise" +let[@inline never] with_lock (st: state) f = + Mutex.lock st.lock; + match f () with + | x -> + Mutex.unlock st.lock; + x + | exception e -> + Mutex.unlock st.lock; + reraise e + +let fscq_getattr st path = + with_lock st @@ fun () -> + let ctx = Fuse.get_context () in + let stat = Fscq.Operations.getattr st.ops path in + { stat with st_uid = ctx.uid; st_gid = ctx.gid } + +let fscq_fopen st path flags = + with_lock st @@ fun () -> + Ops.fopen st.ops path flags + +let fscq_mknod st path kind _perm _rdev = + with_lock st @@ fun () -> + Ops.mknod st.ops path kind + +let fscq_mkdir st path _ = + with_lock st @@ fun () -> + Ops.mkdir st.ops path + +let fscq_unlink st path = + with_lock st @@ fun () -> + Ops.unlink st.ops path + +let fscq_read st path buffer offset inum = + with_lock st @@ fun () -> + Ops.read st.ops path buffer offset inum + +let fscq_write st path buffer offset inum = + with_lock st @@ fun () -> + let buflen = Bigarray.Array1.size_in_bytes buffer in + Ops.write st.ops path buffer offset buflen inum + +let fscq_truncate st path size = + with_lock st @@ fun () -> + Ops.truncate st.ops path size + +let fscq_opendir st path x = + with_lock st @@ fun () -> + Ops.opendir st.ops path x + +let fscq_readdir st path dnum = + with_lock st @@ fun () -> + Ops.readdir st.ops path dnum + +let fscq_rename st src dst = + with_lock st @@ fun () -> + Ops.rename st.ops src dst + +let fscq_sync_file st path isdatasync inum = + with_lock st @@ fun () -> + Ops.sync_file st.ops path isdatasync inum + +let fscq_sync_dir st x y z = + with_lock st @@ fun () -> + Ops.sync_dir st.ops x y z + +let fscq_statfs (st: state) x = + with_lock st @@ fun () -> + let stats = Ops.statfs st.ops x in + Fuse.Unix_util.{ + f_bsize = stats.blocksize; + f_frsize = stats.blocksize; (* ??? "Fragment size, smallest addressable data size" *) + f_blocks = stats.blocks; + f_bfree = stats.free_blocks; + f_bavail = stats.free_blocks; + f_files = stats.files; + f_ffree = stats.free_files; + f_favail = stats.free_files; (* fuse.h says: ignored? *) + f_fsid = 0L; (* fuse.h says: ignored? *) + f_flag = 0L; (* fuse.h says: ignored? *) + f_namemax = stats.namemax; + } + +let fscq_utime _path _ _ = + () + +let fscq_chmod (_path: string) (_mode: int) = + () + +let fscq_destroy (st: state) () = + with_lock st @@ fun () -> + Ops.destroy st.ops + +let fscq_fuse_ops st = + { Fuse.default_operations with + getattr = fscq_getattr st; + fopen = fscq_fopen st; + (* create file : missing *) + mknod = fscq_mknod st; + mkdir = fscq_mkdir st; + unlink = fscq_unlink st; + rmdir = fscq_unlink st; + read = fscq_read st; + write = fscq_write st; + truncate = fscq_truncate st; + opendir = fscq_opendir st; + readdir = fscq_readdir st; + statfs = fscq_statfs st; + destroy = fscq_destroy st; + utime = fscq_utime; + rename = fscq_rename st; + chmod = fscq_chmod; + fsync = fscq_sync_file st; + fsyncdir = fscq_sync_dir st; + } + +(* main *) + +let () = + match Sys.argv |> Array.to_list with + | argv0 :: disk :: _ -> + let fuseargv = Array.append [| argv0 |] (Array.sub Sys.argv 2 ((Array.length Sys.argv) - 2)) in + Printf.printf "Recovering file system\n%!"; + begin match Ops.load_fs disk with + | Errno.Err _ -> + Printf.eprintf "recovery failed; is this an FSCQ fs?\n"; exit 1 + | Errno.OK ops_st -> + let st = mk_state ops_st in + Printf.printf "Starting file system\n%!"; + Fuse.main fuseargv (fscq_fuse_ops st) + end + | _ -> + Printf.eprintf "Usage: %s -f [other fuse options...]\n" + Sys.argv.(0); exit 1 diff --git a/src/mlbin/mkfs.ml b/src/mlbin/mkfs.ml new file mode 100644 index 00000000..c7372d71 --- /dev/null +++ b/src/mlbin/mkfs.ml @@ -0,0 +1,33 @@ +module Errno = Fscq.Errno +module AsyncFS = Fscq.AsyncFS +module FSLayout = Fscq.FSLayout + +let cachesize = Z.of_int 100_000 + +let do_mkfs fn = + let ds = Fscq.Disk.init fn in + Printf.printf "Initializing filesystem in %s\n" fn; + let mkfs_prog = AsyncFS.AFS.mkfs cachesize (Z.of_int 4) (Z.of_int 1) (Z.of_int 256) in + begin match Fscq.Interp.run ds mkfs_prog with + | Errno.Err _ -> Printf.printf "mkfs failed" + | Errno.OK (_, fsxp) -> + Printf.printf "Initialization OK, %s blocks\n" + (Z.to_string fsxp.FSLayout.coq_FSXPMaxBlock); + Printf.printf " === disk layout addresses ===\n"; + Printf.printf " superblock: 0\n"; + Printf.printf " data blocks start: 1\n"; + Printf.printf " inode blocks start: %s\n" + (Z.to_string (Z.succ FSLayout.(coq_IXStart fsxp.coq_FSXPInode))); + Printf.printf " log header: %s\n" + (Z.format "%x" FSLayout.(coq_LogHeader fsxp.coq_FSXPLog)); + Printf.printf " log data start: %s\n" + (Z.format "%x" FSLayout.(coq_LogData fsxp.coq_FSXPLog)) + end; + Fscq.Disk.close ds + +let _ = + match Sys.argv with + | [| _ ; fn |] -> + do_mkfs fn + | _ -> + Printf.printf "Usage: %s \n" Sys.argv.(0) diff --git a/src/mlfuse.ml b/src/mlfuse.ml deleted file mode 100644 index 013c69cf..00000000 --- a/src/mlfuse.ml +++ /dev/null @@ -1,261 +0,0 @@ -open Log -open Printf -open Sys -open Word -open Interp -open Unix -open Bigarray - -let mem_state = ref (Log.ms_empty, (Cache.cache_empty, ())) -let fuselock = Mutex.create () - -let run_fs ds prog = - try - let (ms', r) = run_prog ds (prog !mem_state) in - mem_state := ms'; - r - with - e -> Printf.printf "run_fs exception: %s\n%!" (Printexc.to_string e); raise e - -let string_explode s = - let rec exp i l = - if i < 0 then l else exp (i - 1) (s.[i] :: l) in - exp (String.length s - 1) [] - -let string_implode l = - let res = String.create (List.length l) in - let rec imp i = function - | [] -> res - | c :: l -> res.[i] <- c; imp (i + 1) l in - imp 0 l - -let split_path s = Str.split (Str.regexp "/+") s - -let split_path_coq s = List.map string_explode (split_path s) - -let lookup ds fsxp path = - let nameparts = split_path_coq path in - let (r, ()) = run_fs ds (FS.lookup fsxp (FSLayout.coq_FSXPRootInum fsxp) nameparts) in - r - -let stat_dir (W ino) = - { - Unix.LargeFile.st_nlink = 2; - st_kind = S_DIR; - st_perm = 0o755; - st_size = Int64.of_int 4096; - st_dev = 0; - st_ino = Z.to_int ino; - st_uid = 0; - st_gid = 0; - st_rdev = 0; - st_atime = 0.0; - st_mtime = 0.0; - st_ctime = 0.0; - } - -let attr_to_kind ftype = - match ftype with - | 0 -> S_REG - | 1 -> S_SOCK - | 2 -> S_FIFO - | 3 -> S_BLK - | 4 -> S_CHR - | _ -> S_REG - -let stat_file (W ino) (W len) { ByteFile.BYTEFILE.coq_FMTime = wmtime; coq_FType = wtype; coq_FDev = wdev } = - let (W fmtime) = wmtime in - let (W ftype) = wtype in - let (W fdev) = wdev in - { - Unix.LargeFile.st_nlink = 1; - st_kind = attr_to_kind (Z.to_int ftype); - st_perm = 0o755; - st_size = Z.to_int64 len; - st_dev = 0; - st_ino = Z.to_int ino; - st_uid = 0; - st_gid = 0; - st_rdev = Z.to_int fdev; - st_atime = 0.0; - st_mtime = Z.to_float fmtime; - st_ctime = 0.0; - } - -let fscq_getattr ds fsxp path = - Mutex.lock fuselock; - let r = lookup ds fsxp path in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (ENOENT, "stat", path)) - | Some (ino, true) -> Mutex.unlock fuselock; stat_dir ino - | Some (ino, false) -> - let (attr, ()) = run_fs ds (FS.file_get_attr fsxp ino) in - let (len, ()) = run_fs ds (FS.file_get_sz fsxp ino) in - Mutex.unlock fuselock; - stat_file ino len attr - -let fscq_readdir ds fsxp path _ = - Mutex.lock fuselock; - let r = lookup ds fsxp path in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (ENOENT, "readdir", path)) - | Some (ino, true) -> - let (files, ()) = run_fs ds (FS.readdir fsxp ino) in - Mutex.unlock fuselock; - List.append ["."; ".."] (List.map (fun (name, (ino, isdir)) -> string_implode name) files) - | Some (_, false) -> Mutex.unlock fuselock; raise (Unix_error (ENOTDIR, "readdir", path)) - -let fscq_fopen ds fsxp path flags = - Mutex.lock fuselock; - let r = lookup ds fsxp path in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (ENOENT, "fopen", path)) - | Some (_, true) -> Mutex.unlock fuselock; raise (Unix_error (EISDIR, "fopen", path)) - | Some (W ino, false) -> Mutex.unlock fuselock; Some (Z.to_int ino) - -let fscq_mknod ds fsxp path kind perm rdev = - Mutex.lock fuselock; - let fn = string_explode (Filename.basename path) in - let r = lookup ds fsxp (Filename.dirname path) in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (ENOENT, "mknod", path)) - | Some (_, false) -> Mutex.unlock fuselock; raise (Unix_error (ENOTDIR, "mknod", path)) - | Some (dnum, true) -> - let (r, ()) = ( match kind with - | S_REG -> run_fs ds (FS.create fsxp dnum fn) - | S_SOCK -> run_fs ds (FS.mkdev fsxp dnum fn (W (Z.of_int 1)) (W (Z.of_int 0))) - | S_FIFO -> run_fs ds (FS.mkdev fsxp dnum fn (W (Z.of_int 2)) (W (Z.of_int 0))) - | S_BLK -> run_fs ds (FS.mkdev fsxp dnum fn (W (Z.of_int 3)) (W (Z.of_int rdev))) - | S_CHR -> run_fs ds (FS.mkdev fsxp dnum fn (W (Z.of_int 4)) (W (Z.of_int rdev))) - | _ -> Mutex.unlock fuselock; raise (Unix_error (EIO, "mknod", path)) - ) in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (EIO, "mknod", path)) - | Some _ -> Mutex.unlock fuselock; () - -let fscq_mkdir ds fsxp path mode = - Mutex.lock fuselock; - let fn = string_explode (Filename.basename path) in - let r = lookup ds fsxp (Filename.dirname path) in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (ENOENT, "mkdir", path)) - | Some (_, false) -> Mutex.unlock fuselock; raise (Unix_error (ENOTDIR, "mkdir", path)) - | Some (dnum, true) -> - let (r, ()) = run_fs ds (FS.mkdir fsxp dnum fn) in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (EIO, "mkdir", path)) - | Some _ -> Mutex.unlock fuselock; () - -let fscq_read ds fsxp path buf ofs ino = - Mutex.lock fuselock; - let inum = W (Z.of_int ino) in - let zoff = Z.of_int64 ofs in - let zlen = Z.of_int (Array1.dim buf) in - let (res, ()) = run_fs ds (FS.read_bytes fsxp inum zoff zlen) in - match res with - | ByteFile.BYTEFILE.Coq_len_bytes (cc, (W bytes)) -> - let strbytes = Z.to_bits bytes in - String.iteri (fun i c -> Array1.set buf i c) strbytes; - Mutex.unlock fuselock; - Z.to_int cc - -let fscq_write ds fsxp path buf ofs ino = - Mutex.lock fuselock; - let inum = W (Z.of_int ino) in - let zoff = Z.of_int64 ofs in - let len = Array1.dim buf in - let strbytes = String.create len in - for i = 0 to len-1 do - String.set strbytes i (Array1.get buf i) - done; - let zbytes = Z.of_bits strbytes in - let (res, ()) = run_fs ds (FS.append fsxp inum zoff (Z.of_int len) (W zbytes)) in - Mutex.unlock fuselock; - if res then len else raise (Unix_error (EIO, "write", path)) - -let fscq_rename ds fsxp src dst = - Mutex.lock fuselock; - let src_fn = string_explode (Filename.basename src) in - let src_dn = split_path_coq (Filename.dirname src) in - let dst_fn = string_explode (Filename.basename dst) in - let dst_dn = split_path_coq (Filename.dirname dst) in - let (r, ()) = run_fs ds (FS.rename fsxp (FSLayout.coq_FSXPRootInum fsxp) - src_dn src_fn dst_dn dst_fn) in - Mutex.unlock fuselock; - if r then () else raise (Unix_error (EIO, "rename", src)) - -let fscq_unlink ds fsxp path = - Mutex.lock fuselock; - let fn = string_explode (Filename.basename path) in - let r = lookup ds fsxp (Filename.dirname path) in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (ENOENT, "unlink", path)) - | Some (_, false) -> Mutex.unlock fuselock; raise (Unix_error (ENOTDIR, "unlink", path)) - | Some (dnum, true) -> - let (r, ()) = run_fs ds (FS.delete fsxp dnum fn) in - Mutex.unlock fuselock; - if r then () else raise (Unix_error (EIO, "unlink", path)) - -let fscq_truncate ds fsxp path len = - Mutex.lock fuselock; - let r = lookup ds fsxp path in - match r with - | None -> Mutex.unlock fuselock; raise (Unix_error (ENOENT, "unlink", path)) - | Some (_, true) -> Mutex.unlock fuselock; raise (Unix_error (EISDIR, "unlink", path)) - | Some (inum, false) -> - let (r, ()) = run_fs ds (FS.file_resize fsxp inum (Z.of_int64 len)) in - Mutex.unlock fuselock; - if r then () else raise (Unix_error (EIO, "truncate", path)) - -let fscq_chmod ds fsxp path mode = - () - -let fscq_chown ds fsxp path uid gid = - () - -let fscq_statfs ds fsxp path = - Mutex.lock fuselock; - let ((W freeblocks), ((W freeinodes), ())) = run_fs ds (FS.statfs fsxp) in - Mutex.unlock fuselock; - let (W block_bitmaps) = FSLayout.coq_BmapNBlocks (FSLayout.coq_FSXPBlockAlloc fsxp) in - let (W inode_bitmaps) = FSLayout.coq_BmapNBlocks (FSLayout.coq_FSXPInodeAlloc fsxp) in - { - Unix_util.f_bsize = Int64.of_int Interp.blockbytes; - f_frsize = Int64.of_int Interp.blockbytes; - f_blocks = Int64.of_int (8 * Interp.blockbytes * (Z.to_int block_bitmaps)); - f_bfree = Z.to_int64 freeblocks; - f_bavail = Z.to_int64 freeblocks; - f_files = Int64.of_int (8 * Interp.blockbytes * (Z.to_int inode_bitmaps)); - f_ffree = Z.to_int64 freeblocks; - f_favail = Z.to_int64 freeblocks; - f_fsid = Int64.of_int 0; - f_flag = Int64.of_int 0; - f_namemax = Z.to_int64 DirName.SDIR.namelen; - } - -let _ = - if (Array.length Sys.argv < 2) then Printf.printf "Usage: %s disk -f /mnt/fscq\n" Sys.argv.(0); - let diskfn = Sys.argv.(1) in - let ds = init_disk diskfn in - let (mscs, (fsxp, ())) = run_prog ds FS.recover in - Printf.printf "Recovery OK\n%!"; - mem_state := mscs; - let fuseargv = Array.append [| Sys.argv.(0) |] (Array.sub Sys.argv 2 ((Array.length Sys.argv) - 2)) in - Fuse.main fuseargv - { - Fuse.default_operations with - getattr = fscq_getattr ds fsxp; - readdir = fscq_readdir ds fsxp; - fopen = fscq_fopen ds fsxp; - mknod = fscq_mknod ds fsxp; - mkdir = fscq_mkdir ds fsxp; - read = fscq_read ds fsxp; - write = fscq_write ds fsxp; - rename = fscq_rename ds fsxp; - unlink = fscq_unlink ds fsxp; - rmdir = fscq_unlink ds fsxp; - truncate = fscq_truncate ds fsxp; - chmod = fscq_chmod ds fsxp; - chown = fscq_chown ds fsxp; - statfs = fscq_statfs ds fsxp; - } diff --git a/src/big.ml b/src/mllib/big.ml similarity index 99% rename from src/big.ml rename to src/mllib/big.ml index 0ad5d57b..a696106e 100644 --- a/src/big.ml +++ b/src/mllib/big.ml @@ -16,8 +16,10 @@ type big_int = Big_int_Z.big_int let zero = zero_big_int (** The big integer [0]. *) + let one = unit_big_int (** The big integer [1]. *) + let two = big_int_of_int 2 (** The big integer [2]. *) @@ -25,28 +27,39 @@ let two = big_int_of_int 2 let opp = minus_big_int (** Unary negation. *) + let abs = abs_big_int (** Absolute value. *) + let add = add_big_int (** Addition. *) + let succ = succ_big_int (** Successor (add 1). *) + let add_int = add_int_big_int (** Addition of a small integer to a big integer. *) + let sub = sub_big_int (** Subtraction. *) + let pred = pred_big_int (** Predecessor (subtract 1). *) + let mult = mult_big_int (** Multiplication of two big integers. *) + let mult_int = mult_int_big_int (** Multiplication of a big integer by a small integer *) + let square = square_big_int (** Return the square of the given big integer *) + let sqrt = sqrt_big_int (** [sqrt_big_int a] returns the integer square root of [a], that is, the largest big integer [r] such that [r * r <= a]. Raise [Invalid_argument] if [a] is negative. *) + let quomod = quomod_big_int (** Euclidean division of two big integers. The first part of the result is the quotient, @@ -54,14 +67,18 @@ let quomod = quomod_big_int Writing [(q,r) = quomod_big_int a b], we have [a = q * b + r] and [0 <= r < |b|]. Raise [Division_by_zero] if the divisor is zero. *) + let div = div_big_int (** Euclidean quotient of two big integers. This is the first result [q] of [quomod_big_int] (see above). *) + let modulo = mod_big_int (** Euclidean modulus of two big integers. This is the second result [r] of [quomod_big_int] (see above). *) + let gcd = gcd_big_int (** Greatest common divisor of two big integers. *) + let power = power_big_int_positive_big_int (** Exponentiation functions. Return the big integer representing the first argument [a] raised to the power [b] @@ -74,18 +91,22 @@ let power = power_big_int_positive_big_int let sign = sign_big_int (** Return [0] if the given big integer is zero, [1] if it is positive, and [-1] if it is negative. *) + let compare = compare_big_int (** [compare_big_int a b] returns [0] if [a] and [b] are equal, [1] if [a] is greater than [b], and [-1] if [a] is smaller than [b]. *) + let eq = eq_big_int let le = le_big_int let ge = ge_big_int let lt = lt_big_int let gt = gt_big_int (** Usual boolean comparisons between two big integers. *) + let max = max_big_int (** Return the greater of its two arguments. *) + let min = min_big_int (** Return the smaller of its two arguments. *) @@ -94,6 +115,7 @@ let min = min_big_int let to_string = string_of_big_int (** Return the string representation of the given big integer, in decimal (base 10). *) + let of_string = big_int_of_string (** Convert a string to a big integer, in decimal. The string consists of an optional [-] or [+] sign, @@ -103,6 +125,7 @@ let of_string = big_int_of_string let of_int = big_int_of_int (** Convert a small integer to a big integer. *) + let is_int = is_int_big_int (** Test whether the given big integer is small enough to be representable as a small integer (type [int]) @@ -111,6 +134,7 @@ let is_int = is_int_big_int [a] is between 2{^30} and 2{^30}-1. On a 64-bit platform, [is_int_big_int a] returns [true] if and only if [a] is between -2{^62} and 2{^62}-1. *) + let to_int = int_of_big_int (** Convert a big integer to a small integer (type [int]). Raises [Failure "int_of_big_int"] if the big integer diff --git a/src/mllib/disk.ml b/src/mllib/disk.ml new file mode 100644 index 00000000..e5b0cd39 --- /dev/null +++ b/src/mllib/disk.ml @@ -0,0 +1,93 @@ +let block_bytes = 4096 + +(* counts the number of reads, writes and syncs *) +type stats = { + mutable reads : int; + mutable writes : int; + mutable syncs : int; +} + +module IntMap = Map.Make(Int) + +type var_store = { + mutable store : Obj.t IntMap.t; + mutable nextvar : int; +} + +type state = { + fd : Unix.file_descr; + stats : stats; + vars : var_store; +} + +let block_to_word b = + Word.natToWord (Z.of_int (block_bytes * 8)) (Z.of_bits b) + +let word_to_string_nbytes nb_bytes (Word.W w) = + let buf = Bytes.make nb_bytes (Char.chr 0) in + let bits = Z.to_bits w in + Bytes.blit_string bits 0 buf 0 (min (String.length bits) nb_bytes); + Bytes.unsafe_to_string buf + +let word_to_string_nbits nb_bits w = + let nb_bytes = (nb_bits + 7) / 8 in + word_to_string_nbytes nb_bytes w + +let word_to_block w = + word_to_string_nbytes block_bytes w + +let init (filename: string): state = + let fd = Unix.openfile filename [ Unix.O_RDWR ; Unix.O_CREAT ] 0o666 in + { fd ; + stats = { reads = 0; writes = 0; syncs = 0 }; + vars = { store = IntMap.empty; nextvar = 0 } } + +let close (st: state) = + Unix.close st.fd + +let print_stats (st: state) = + Printf.printf "Disk I/O stats:\n"; + Printf.printf "Reads: %d\n" st.stats.reads; + Printf.printf "Writes: %d\n" st.stats.writes; + Printf.printf "Syncs: %d\n" st.stats.syncs + +let read (st: state) (a: int): Word.word = + st.stats.reads <- st.stats.reads + 1; + let buf = Bytes.create block_bytes in + let cc = ExtUnix.All.pread st.fd (a * block_bytes) buf 0 block_bytes in + if cc <> block_bytes then ( + Printf.eprintf "attempted read off:%d nbytes:%d\n%!" (a * block_bytes) block_bytes; + Printf.eprintf "read %d bytes\n%!" cc; + raise (Failure "Disk.read") + ); + block_to_word (Bytes.unsafe_to_string buf) + +let write (st: state) (a: int) (w: Word.word) = + st.stats.writes <- st.stats.writes + 1; + let block = word_to_block w in + let cc = ExtUnix.All.pwrite st.fd (a * block_bytes) block 0 block_bytes in + if cc <> block_bytes then raise (Failure "Disk.write") + +let sync (st: state) = + st.stats.syncs <- st.stats.syncs + 1; + ExtUnix.All.fsync st.fd + +let trim (_: state) _ = + () + +let var_alloc (st: state) (x: Obj.t): int = + let v = st.vars.nextvar in + st.vars.nextvar <- st.vars.nextvar + 1; + st.vars.store <- IntMap.add v x st.vars.store; + v + +let var_get (st: state) (v: int): Obj.t = + match IntMap.find_opt v st.vars.store with + | Some x -> x + | None -> failwith "var_get of unset variable" + +let var_set (st: state) (v: int) (x: Obj.t) = + st.vars.store <- IntMap.add v x st.vars.store + +let var_delete (st: state) (v: int) = + st.vars.store <- IntMap.remove v st.vars.store diff --git a/src/mllib/dune b/src/mllib/dune new file mode 100644 index 00000000..5af964c8 --- /dev/null +++ b/src/mllib/dune @@ -0,0 +1,7 @@ +(library + (name fscq) + (flags :standard -w -32-33-34-39) + (libraries zarith unix extunix checkseum)) + +(copy_files ../codegen/*.ml) +(copy_files ../codegen/{AsyncFS,Inode}.mli) diff --git a/src/mllib/evict.ml b/src/mllib/evict.ml new file mode 100644 index 00000000..5e02ad84 --- /dev/null +++ b/src/mllib/evict.ml @@ -0,0 +1,7 @@ +type eviction_state = unit + +let eviction_init = () + +let eviction_update s _ = s + +let eviction_choose s = (Z.zero, s) diff --git a/src/mllib/interp.ml b/src/mllib/interp.ml index 7b790705..8e6f7ae0 100644 --- a/src/mllib/interp.ml +++ b/src/mllib/interp.ml @@ -1,69 +1,69 @@ -let addrlen = Big.of_int 64 -let blockbytes = 4096 -let blockbits = Big.of_int (blockbytes*8) -let debug = false -let really_sync = false +module Crc32 = Checkseum.Crc32 -type disk_state = { disk_fd : Unix.file_descr ref } +let verbose = false +let output = false -let addr_to_int a = Big.to_int (Word.wordToNat addrlen a) +let debugmsg msgf = + if verbose then msgf (Printf.kprintf print_endline) -let word_to_block (Word.W w) = - let s = Z.to_bits w in - let nbytes = String.length s in - let res = String.concat "" [ s ; String.make (blockbytes-nbytes) (Char.chr 0) ] in - res +let crc32_word_update c sz w = + let bits = Disk.word_to_string_nbits sz w in + Crc32.digest_string bits 0 (String.length bits) c -let block_to_word b = - let z = Z.of_bits b in - Word.W z +let rec run : type a. Disk.state -> a Prog.prog -> Obj.t = + fun ds p -> + match p with + | Ret x -> + debugmsg (fun m -> m "Done"); + Obj.repr x + | Read a -> + debugmsg (fun m -> m "Read %s" (Z.to_string a)); + Obj.repr @@ Disk.read ds (Z.to_int a) + | Write (a, v) -> + debugmsg (fun m -> m "Write %s" (Z.to_string a)); + Obj.repr @@ Disk.write ds (Z.to_int a) v + | Sync -> + debugmsg (fun m -> m "Sync"); + Obj.repr @@ Disk.sync ds + | Trim a -> + debugmsg (fun m -> m "Trim %s" (Z.to_string a)); + Obj.repr @@ Disk.trim ds a + | VarAlloc v -> + debugmsg (fun m -> m "VarAlloc"); + Obj.repr @@ Disk.var_alloc ds v + | VarDelete i -> + debugmsg (fun m -> m "VarDelete %d" i); + Obj.repr @@ Disk.var_delete ds i + | VarGet i -> + debugmsg (fun m -> m "VarGet %d" i); + Obj.repr @@ Disk.var_get ds i + | VarSet (i, v) -> + debugmsg (fun m -> m "VarSet %d" i); + Obj.repr @@ Disk.var_set ds i v + | AlertModified -> + debugmsg (fun m -> m "AlertModified"); + Obj.repr () + | Debug (s, n) -> + if output then + Printf.printf "%s %s\n%!" + (String.of_seq (List.to_seq s)) (Z.to_string n); + Obj.repr () + | Rdtsc -> + (* TODO *) + Obj.repr Z.zero + | Hash (sz, w) -> + debugmsg (fun m -> m "Hash %s" (Z.to_string sz)); + let c = crc32_word_update Crc32.default (Z.to_int sz) w in + Obj.repr @@ Z.of_int64 (Optint.to_int64 c) + | Hash2 (sz1, sz2, w1, w2) -> + debugmsg (fun m -> m "Hash2 %s %s" (Z.to_string sz1) (Z.to_string sz2)); + let c1 = crc32_word_update Crc32.default (Z.to_int sz1) w1 in + let c2 = crc32_word_update c1 (Z.to_int sz2) w2 in + Obj.repr @@ Z.of_int64 (Optint.to_int64 c2) + | Bind (p1, p2) -> + debugmsg (fun m -> m "Bind"); + let r1 = run ds p1 in + run ds (p2 r1) -let init_disk fn = - let fd = Unix.openfile fn [ Unix.O_RDWR ; Unix.O_CREAT ] 0o666 in - { disk_fd = ref fd } - -let close_disk { disk_fd = fd } = - Unix.close !fd - -let read_disk { disk_fd = fd } b = - let s = String.create blockbytes in - let cc = ExtUnix.All.pread !fd (b * blockbytes) s 0 blockbytes in - if cc != blockbytes then raise (Failure "read_disk"); - block_to_word s - -let write_disk { disk_fd = fd } b v = - let s = word_to_block v in - let cc = ExtUnix.All.pwrite !fd (b * blockbytes) s 0 blockbytes in - if cc != blockbytes then raise (Failure "write_disk") - -let sync_disk { disk_fd = fd } b = - if really_sync then ExtUnix.All.fsync !fd - -let set_size_disk { disk_fd = fd } b = - Unix.ftruncate !fd (b*blockbytes) - -let rec run_dcode ds = function - | Prog.Done t -> - if debug then Printf.printf "done()\n%!"; - t - | Prog.Trim (a, rx) -> - if debug then Printf.printf "trim(%d)\n%!" (addr_to_int a); - run_dcode ds (rx ()) - | Prog.Sync (a, rx) -> - if debug then Printf.printf "sync(%d)\n%!" (addr_to_int a); - sync_disk ds (addr_to_int a); - run_dcode ds (rx ()) - | Prog.Read (a, rx) -> - if debug then Printf.printf "read(%d)\n%!" (addr_to_int a); - let v = read_disk ds (addr_to_int a) in - run_dcode ds (rx v) - | Prog.Write (a, v, rx) -> - if debug then Printf.printf "write(%d)\n%!" (addr_to_int a); - write_disk ds (addr_to_int a) v; - run_dcode ds (rx ()) - -let run_prog ds p = - try - run_dcode ds (p (fun x -> Prog.Done x)) - with - e -> Printf.printf "Exception: %s\n%!" (Printexc.to_string e); raise e +let run (ds: Disk.state) (p: 'a Prog.prog): 'a = + Obj.magic (run ds p) diff --git a/src/mllib/list_extra.ml b/src/mllib/list_extra.ml new file mode 100644 index 00000000..de0e2d40 --- /dev/null +++ b/src/mllib/list_extra.ml @@ -0,0 +1,28 @@ +(* from containers *) + +let direct_depth_append_ = 10_000 + +let append l1 l2 = + let rec direct i l1 l2 = match l1 with + | [] -> l2 + | _ when i=0 -> safe l1 l2 + | x::l1' -> x :: direct (i-1) l1' l2 + and safe l1 l2 = + List.rev_append (List.rev l1) l2 + in + match l1 with + | [] -> l2 + | [x] -> x::l2 + | [x;y] -> x::y::l2 + | _ -> direct direct_depth_append_ l1 l2 + +let repeat i x = + let rec aux acc i = + if i = 0 then + acc + else + aux (x :: acc) (i - 1) + in + aux [] i + +let repeat x i = repeat (Z.to_int i) x diff --git a/src/mllib/operations.ml b/src/mllib/operations.ml new file mode 100644 index 00000000..227caca2 --- /dev/null +++ b/src/mllib/operations.ml @@ -0,0 +1,445 @@ +open Unix +module AsyncFS = AsyncFS.AFS + +let cachesize = Z.of_int 100_000 +(* there also are some hardcoded "4096" in the code below... *) +let blocksize = (Z.to_int AsyncDisk.Valulen.valulen) / 8 + +type mscs = BFile.BFILE.memstate +type fsxp = FSLayout.fs_xparams + +type state = { + ds : Disk.state; + mutable mscs : mscs; + fsxp : fsxp; +} + +type fs_stats = { + blocksize : int64; + blocks : int64; + free_blocks : int64; + files : int64; + free_files : int64; + namemax : int64; +} + +let run (p: mscs -> (mscs * 'a) Prog.prog) (st: state) = + let mscs', ret = Interp.run st.ds (p st.mscs) in + st.mscs <- mscs'; + ret + +(* Error conversion to Unix *) + +let unix_of_errno (e: Errno.coq_Errno): Unix.error = + match e with + | Errno.ELOGOVERFLOW -> EIO + | Errno.ENOTDIR -> ENOTDIR + | Errno.EISDIR -> EISDIR + | Errno.ENOENT -> ENOENT + | Errno.EFBIG -> EFBIG + | Errno.ENAMETOOLONG -> ENAMETOOLONG + | Errno.EEXIST -> EEXIST + | Errno.ENOSPCBLOCK -> ENOSPC + | Errno.ENOSPCINODE -> ENOSPC + | Errno.ENOTEMPTY -> ENOTEMPTY + | Errno.EINVAL -> EINVAL + +let check_errno fname arg = function + | Errno.OK () -> () + | Errno.Err e -> raise (Unix_error (unix_of_errno e, fname, arg)) + +(* path helpers *) + +(* TODO less ad-hoc path handling? + what kind of paths can we get from fuse? *) + +let split_directories (path: string) = + if path = "/" then [] + else List.tl @@ String.split_on_char '/' path + +let rec take_drop_last = function + | [] -> raise (Invalid_argument "take_drop_last") + | [x] -> ([], x) + | x :: xs -> + let (xs', last) = take_drop_last xs in + x :: xs', last + +let split_dirs_file (path: string) = + take_drop_last (split_directories path) + +let explode s = + String.to_seq s |> List.of_seq + +let implode l = + String.of_seq @@ List.to_seq l + +(* Int64 helpers *) + +module Int64 = struct + include Int64 + let ( * ) = mul + let ( - ) = sub + let ( + ) = add + let ( / ) = div +end + +(* stat helpers *) + +let stat_dir (inum: Z.t): Unix.LargeFile.stats = + Unix.LargeFile.{ + st_dev = 0; (* ignored by fuse *) + st_ino = Z.to_int inum; (* ignored by fuse *) + st_kind = S_DIR; + st_perm = 0o755; + st_nlink = 2; + st_uid = 0; + st_gid = 0; + st_rdev = 0; + st_size = 4096L; + st_atime = 0.; + st_mtime = 0.; + st_ctime = 0.; + } + +let kind_of_attr attr = + let W w = Inode.INODE.coq_AType attr in + if Z.(equal w zero) then S_REG else S_SOCK + +let stat_file (inum: Z.t) (attr: Obj.t) = + Unix.LargeFile.{ + st_dev = 0; (* ignored by fuse *) + st_ino = Z.to_int inum; (* ignored by fuse *) + st_rdev = 0; + st_kind = kind_of_attr attr; + st_perm = 0o777; + st_nlink = 1; + st_uid = 0; + st_gid = 0; + st_size = + Z.to_int64 @@ Word.wordToNat 64 + @@ Inode.INODE.coq_ABytes attr; + st_atime = 0.; + st_mtime = + Z.to_float @@ Word.wordToNat 32 + @@ Inode.INODE.coq_AMTime attr; + st_ctime = 0.; + } + +(* operations *) + +let getattr (st: state) (path: string) = + let nameparts = split_directories path in + let res, () = run ( + AsyncFS.lookup st.fsxp + st.fsxp.FSLayout.coq_FSXPRootInum + (List.map explode nameparts) + ) st in + match res with + | Errno.Err _ -> raise (Unix_error (ENOENT, "stat", path)) + | Errno.OK (inum, true (*isdir*)) -> + stat_dir inum + | Errno.OK (inum, false) -> + let attr, () = run (AsyncFS.file_get_attr st.fsxp inum) st in + stat_file inum attr + +let fopen (st: state) (path: string) (flags: Unix.open_flag list) = + let nameparts = split_directories path in + let res, () = run ( + AsyncFS.lookup st.fsxp + st.fsxp.FSLayout.coq_FSXPRootInum + (List.map explode nameparts) + ) st in + match res with + | Errno.Err _ -> raise (Unix_error (ENOENT, "fopen", path)) + | Errno.OK (_, true (*isdir*)) -> + raise (Unix_error (EISDIR, "fopen", path)) + | Errno.OK (inum, false) -> + if List.mem O_TRUNC flags then begin + let res, () = run (AsyncFS.file_truncate st.fsxp inum Z.zero) st in + check_errno "fopen" path res; + let res, () = run (AsyncFS.file_set_sz st.fsxp inum (Word.W Z.zero)) st in + check_errno "fopen" path res + end; + Some (Z.to_int inum) (* XXX? what about the None case? *) + +let mknod (st: state) (path: string) kind = + let dirparts, filename = split_dirs_file path in + let res, () = run ( + AsyncFS.lookup st.fsxp + st.fsxp.FSLayout.coq_FSXPRootInum + (List.map explode dirparts) + ) st in + match res with + | Errno.Err _ -> raise (Unix_error (ENOENT, "mknod", path)) + | Errno.OK (_, false(*isdir*)) -> + raise (Unix_error (ENOTDIR, "mknod", path)) + | Errno.OK (dnum, true) -> + let res, () = + match kind with + | S_REG -> run (AsyncFS.create st.fsxp dnum (explode filename)) st + | S_SOCK -> run (AsyncFS.mksock st.fsxp dnum (explode filename)) st + | _ -> raise (Unix_error (EINVAL, "mknod", path)) + in + match res with + | Errno.Err _ -> raise (Unix_error (EIO, "mknod", path)) + | Errno.OK _ -> () + +let mkdir (st: state) path = + let dirparts, filename = split_dirs_file path in + let res, () = run ( + AsyncFS.lookup st.fsxp + st.fsxp.FSLayout.coq_FSXPRootInum + (List.map explode dirparts) + ) st in + match res with + | Errno.Err _ -> raise (Unix_error (ENOENT, "mkdir", path)) + | Errno.OK (_, false(*isdir*)) -> + raise (Unix_error (ENOTDIR, "mkdir", path)) + | Errno.OK (dnum, true) -> + let res, () = run (AsyncFS.mkdir st.fsxp dnum (explode filename)) st in + match res with + | Errno.Err _ -> raise (Unix_error (EIO, "mkdir", path)) + | Errno.OK _ -> () + +let unlink (st: state) path = + let dirparts, filename = split_dirs_file path in + let res, () = run ( + AsyncFS.lookup st.fsxp + st.fsxp.FSLayout.coq_FSXPRootInum + (List.map explode dirparts) + ) st in + match res with + | Errno.Err _ -> raise (Unix_error (ENOENT, "mkdir", path)) + | Errno.OK (_, false(*isdir*)) -> + raise (Unix_error (ENOTDIR, "unlink", path)) + | Errno.OK (dnum, true) -> + let res, () = run (AsyncFS.delete st.fsxp dnum (explode filename)) st in + match res with + | Errno.Err _ -> raise (Unix_error (EIO, "unlink", path)) + | Errno.OK () -> () + +(* MISSING IN OCAMLFUSE *) +let destroy (st: state) = + let () = run (AsyncFS.umount st.fsxp) st in + Disk.close st.ds; + Disk.print_stats st.ds + +let iter_ranges off count f = + let startblock = off / blocksize in + let endblock = (off + count - 1) / blocksize in + for blk = startblock to endblock do + let startoff = + if blk = startblock then off mod blocksize + else 0 + in + let endoff = + if blk = endblock then (off + count - 1) mod blocksize + 1 + else blocksize + in + f ~blknum:blk ~off_in_blk:startoff ~count_from_off:(endoff - startoff) + done + +let read_range st inum buffer off bytecount = + let pos = ref 0 in + iter_ranges off bytecount + (fun ~blknum ~off_in_blk ~count_from_off -> + let Word.W wbuf, () = + run (AsyncFS.read_fblock st.fsxp inum (Z.of_int blknum)) st in + let bits = Z.to_bits wbuf in + for i = 0 to count_from_off - 1 do + buffer.{!pos + i} <- bits.[off_in_blk + i] + done; + pos := !pos + count_from_off + ) + +let read (st: state) _path buffer (offset: int64) inum = + let bytecount = Bigarray.Array1.size_in_bytes buffer in + let inum = Z.of_int inum in + let Word.W len, () = run (AsyncFS.file_get_sz st.fsxp inum) st in + let offset = Int64.to_int offset in (* XXX is this dangerous? *) + let len = Z.to_int len in + let offset' = min offset len in + let bytecount' = min bytecount (len - offset') in + read_range st inum buffer offset' bytecount'; + bytecount' + +let bytes_of_bigarray_range ba pos len = + let buf = Bytes.create len in + for i = 0 to len - 1 do + Bytes.set buf i ba.{pos + i} + done; + Bytes.unsafe_to_string buf + +let write_piece st ~inum ~do_log ~init_len ~buffer ~offset ~blknum ~off_in_blk ~count_from_off = + let bufoff = (blknum * blocksize) + off_in_blk - offset in + (* data in buffer is in range [bufoff;bufoff+count_from_off) *) + let piece_bytes = + if count_from_off = blocksize then + (* whole block writes don't need read-modify-write *) + bytes_of_bigarray_range buffer bufoff count_from_off + else begin + let old_block = + if (init_len <= blknum * blocksize) + || (offset = 0 && init_len <= blknum * blocksize + count_from_off) + then + (* If we are doing a partial block write, we don't need RMW in two cases: + (1.) The file was smaller than the start of this block. + (2.) The partial write of this block starts immediately at offset 0 + in this block and writes all the way up to (and maybe past) + the original end of the file. *) + String.make blocksize (Char.chr 0) + else begin + let Word.W block, () = run (AsyncFS.read_fblock st.fsxp inum (Z.of_int blknum)) st in + Z.to_bits block + end + in + let buf = Bytes.of_string old_block in + for i = 0 to count_from_off - 1 do + Bytes.set buf (off_in_blk + i) buffer.{bufoff + i} + done; + Bytes.unsafe_to_string buf + end + in + let piece_word = Word.W (Z.of_bits piece_bytes) in + if do_log then ( + let (_:bool), () = run (AsyncFS.update_fblock st.fsxp inum (Z.of_int blknum) piece_word) st in + () + ) else ( + let () = run (AsyncFS.update_fblock_d st.fsxp inum (Z.of_int blknum) piece_word) st in + () + ); + count_from_off (* number of bytes written *) + +let write (st: state) path buffer (offset: int64) datalen inum = + let Word.W len, () = run (AsyncFS.file_get_sz st.fsxp (Z.of_int inum)) st in + let len = Z.to_int len in + let offset = Int64.to_int offset in (* XXX dangerous? *) + let inum = Z.of_int inum in + let endpos = offset + datalen in + let okspc, do_log = + if len < endpos then ( + let res, () = + run (AsyncFS.file_truncate st.fsxp inum (Z.of_int ((endpos + 4095) / 4096))) st in + (* Appends to a file need to be logged so that the truncate and write + happen in the log. Technically these are different transactions but + FSCQ never breaks up the log. *) + (res, true) + ) else ( + if offset mod 4096 = 0 && datalen mod 4096 = 0 && datalen > 4096 * 5 then + (* block is large and aligned -> bypass write *) + (Errno.OK (), false) + else + (* NOTE: logged overwrites to the middle of the file are disabled since + they are currently not synced by fdatasync, which is unexpected from + a user looking at the Linux API. Thus, regardless of the offset and + length of the write, we always do a direct write. *) + (Errno.OK (), false) + ) + in + match okspc with + | Errno.Err _ -> raise (Unix_error (EIO(*?*), "write", path)) + | Errno.OK () -> + let bytes_written = ref 0 in + iter_ranges offset datalen (fun ~blknum ~off_in_blk ~count_from_off -> + let nwritten = + write_piece st ~inum ~do_log ~init_len:len ~buffer ~offset + ~blknum ~off_in_blk ~count_from_off in + bytes_written := !bytes_written + nwritten + ); + let okspc = + if len < endpos then ( + let ok, () = run (AsyncFS.file_set_sz st.fsxp inum (Word.W (Z.of_int endpos))) st in + ok + ) else Errno.OK () + in + match okspc with + | Errno.OK () -> !bytes_written + | Errno.Err _ -> raise (Unix_error (ENOSPC, "write", path)) + +let truncate (st: state) (path: string) (size: int64) = + let nameparts = split_directories path in + let res, () = run ( + AsyncFS.lookup st.fsxp st.fsxp.FSLayout.coq_FSXPRootInum + (List.map explode nameparts) + ) st + in + match res with + | Errno.Err _ -> raise (Unix_error (ENOENT, "unlink", path)) + | Errno.OK (_, true (*isdir*)) -> raise (Unix_error (EISDIR, "unlink", path)) + | Errno.OK (inum, false (*isdir*)) -> + (* Note that this function is unverified *) + let res, () = run (AsyncFS.ftruncate st.fsxp inum (Z.of_int64 size)) st in + match res with + | Errno.OK () -> () + | Errno.Err _ -> raise (Unix_error (EIO, "truncate", path)) + +let opendir (st: state) path _ = + let nameparts = split_directories path in + let res, () = run ( + AsyncFS.lookup st.fsxp st.fsxp.FSLayout.coq_FSXPRootInum + (List.map explode nameparts) + ) st + in + match res with + | Errno.Err _ -> raise (Unix_error (ENOENT, "opendir", path)) + | Errno.OK (_, false (*isdir*)) -> + raise (Unix_error (ENOTDIR, "opendir", path)) + | Errno.OK (dnum, true) -> + Some (Z.to_int dnum) (* What about the None case? *) + +let readdir (st: state) _path dnum = + (* XXX ocamlfuse does not require file stats? *) + (* let mkstat ctx (fn, (inum, isdir)) = *) + (* if isdir then (fn, stat_dir ctx inum) *) + (* else ( *) + (* let attr, () = run (AsyncFS.file_get_attr st.fsxp inum) st in *) + (* (fn, stat_file ctx inum attr) *) + (* ) *) + (* in *) + (* let ctx = Fuse.get_context () in *) + let dnum = Z.of_int dnum in + let files, () = run (AsyncFS.readdir st.fsxp dnum) st in + (* let files_stat = List.map (mkstat ctx) files in *) + let files = List.map (fun (fn, _) -> implode fn) files in + ["."; ".."] @ files + +let rename (st: state) path_src path_dst = + let srcparts, srcname = split_dirs_file path_src in + let dstparts, dstname = split_dirs_file path_dst in + let res, () = run ( + AsyncFS.rename st.fsxp + st.fsxp.FSLayout.coq_FSXPRootInum + (List.map explode srcparts) (explode srcname) + (List.map explode dstparts) (explode dstname) + ) st in + match res with + | Errno.OK () -> () + | Errno.Err _ -> raise (Unix_error (EIO, "rename", path_src)) + +let sync_file (st: state) _path isdatasync inum = + run (AsyncFS.file_sync st.fsxp (Z.of_int inum)) st; + if not isdatasync then ( + (* full sync *) + run (AsyncFS.tree_sync st.fsxp) st + ) + +let sync_dir (st: state) _ _ _ : unit = + run (AsyncFS.tree_sync st.fsxp) st + +let statfs (st: state) _ = + let freeblocks, (freeinodes, ()) = run (AsyncFS.statfs st.fsxp) st in + let block_bitmaps = FSLayout.(coq_BmapNBlocks st.fsxp.coq_FSXPBlockAlloc1) in + let inode_bitmaps = FSLayout.(coq_BmapNBlocks st.fsxp.coq_FSXPInodeAlloc) in + { blocksize = 4096L; + blocks = Int64.(8L * 4096L * Z.to_int64 block_bitmaps); + free_blocks = Z.to_int64 freeblocks; + files = Int64.(8L * 4096L * Z.to_int64 inode_bitmaps); + free_files = Z.to_int64 freeinodes; + namemax = Z.to_int64 DirName.SDIR.namelen; } + +let load_fs disk = + let ds = Disk.init disk in + match Interp.run ds (AsyncFS.recover cachesize) with + | Errno.Err e -> Errno.Err e + | Errno.OK (mscs, fsxp) -> + Errno.OK { ds; mscs; fsxp } diff --git a/src/mllib/word.ml b/src/mllib/word.ml index 397cd1b9..92ccdc12 100644 --- a/src/mllib/word.ml +++ b/src/mllib/word.ml @@ -1,5 +1,5 @@ type word = - W of Big.big_int + W of Big.big_int [@@unboxed] let wrap sz n = let isz = Z.to_int sz in @@ -8,28 +8,42 @@ let wrap sz n = let two_to_n n = Z.shift_left Z.one (Z.to_int n) let natToWord sz n = W (wrap sz n) -let wordToNat sz (W n) = n -let wzero sz = W Big.zero -let zext sz (W w) sz' = W w +let wordToNat _sz (W n) = n +let wzero _sz = W Big.zero +let wone _sz = W Big.one +let zext _sz (W w) _sz' = W w -let weq sz (W a) (W b) = Big.eq a b -let wlt_dec sz (W a) (W b) = a < b +let weq _sz (W a) (W b) = Big.eq a b +let wlt_dec _sz (W a) (W b) = a < b +let bit_dec (W w) = Z.equal w Z.zero let wplus sz (W a) (W b) = W (wrap sz (Big.add a b)) let wminus sz (W a) (W b) = W (wrap sz (Big.sub (Big.add (two_to_n sz) a) b)) let wmult sz (W a) (W b) = W (wrap sz (Big.mult a b)) -let wdiv sz (W a) (W b) = W (Big.div a b) -let wmod sz (W a) (W b) = W (Big.modulo a b) +let wdiv _sz (W a) (W b) = W (Big.div a b) +let wmod _sz (W a) (W b) = W (Big.modulo a b) let wbit sz _ (W n) = let int_n = Z.to_int n in if int_n >= (Z.to_int sz) then W Z.zero else W (Z.shift_left Z.one int_n) -let wor _ (W a) (W b) = W (Big_int_Z.or_big_int a b) -let wand _ (W a) (W b) = W (Big_int_Z.and_big_int a b) +let wor _sz (W a) (W b) = W (Big_int_Z.or_big_int a b) +let wand _sz (W a) (W b) = W (Big_int_Z.and_big_int a b) +let wlshift _sz (W a) n = + W (Big_int_Z.shift_left_big_int a (Z.to_int n)) +let wrshift _sz (W a) n = W (Big_int_Z.shift_right_big_int a (Z.to_int n)) +let wones n = + W (Z.(pred (one lsl (Z.to_int n)))) +let wnot _n (W a) = W (Z.lognot a) + +let combine sz1 (W a) _sz2 (W b) = + W (Z.logor a (Big_int_Z.shift_left_big_int b (Big.to_int sz1))) +let split1 sz1 _sz2 (W a) = + W (wrap sz1 a) +let split2 sz1 _sz2 (W a) = + W (Big_int_Z.shift_right_big_int a (Big.to_int sz1)) -let combine sz1 (W a) sz2 (W b) = W (Big.add a (Big_int_Z.shift_left_big_int b (Big.to_int sz1))) -let split1 sz1 sz2 (W a) = W (wrap sz1 a) -let split2 sz1 sz2 (W a) = W (Big_int_Z.shift_right_big_int a (Big.to_int sz1)) let splice _ _ _ _ _ _ = raise Not_found + +let pow2 = two_to_n diff --git a/src/mlmkfs.ml b/src/mlmkfs.ml deleted file mode 100644 index 1e4fd5ef..00000000 --- a/src/mlmkfs.ml +++ /dev/null @@ -1,29 +0,0 @@ -open Log -open Printf -open Sys -open Word -open Interp -open Unix - -let do_mkfs fn = - let ds = init_disk fn in - Printf.printf "Initializing filesystem in %s\n" fn; - let res = run_prog ds (FS.mkfs (W (Big.of_int 1)) (W (Big.of_int 1))) in - ( match res with - | Err _ -> Printf.printf "mkfs failed" - | OK (_, (fsxp, ())) -> - let (W nblocks) = FSLayout.coq_FSXPMaxBlock fsxp in - Printf.printf "Initialization OK, %d blocks\n" (Big.to_int nblocks); - try - set_size_disk ds (Big.to_int nblocks) - with - e -> Printf.printf "Error resizing disk image: %s\n" (Printexc.to_string e) - ); - close_disk ds - -let _ = - match Sys.argv with - | [| _ ; fn |] -> - do_mkfs fn - | _ -> - Printf.printf "Usage: %s diskpath\n" Sys.argv.(0) diff --git a/src/ocamlfuse/Fuse.ml b/src/ocamlfuse/Fuse.ml index 683a28b5..49469bb8 100644 --- a/src/ocamlfuse/Fuse.ml +++ b/src/ocamlfuse/Fuse.ml @@ -25,9 +25,13 @@ *) open Fuse_lib -open Unix_util +module Unix_util = Unix_util +module Fuse_bindings = Fuse_bindings +module Fuse_lib = Fuse_lib +module Fuse_result = Fuse_result -type buffer = (char, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t +type buffer = + (char, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t type context = Fuse_bindings.__fuse_context @@ -35,40 +39,54 @@ let get_context : unit -> context = Fuse_bindings.fuse_get_context type xattr_flags = AUTO | CREATE | REPLACE -type operations = - { getattr : string -> Unix.LargeFile.stats; - readlink : string -> string; - mknod : string -> Unix.file_kind -> Unix.file_perm -> int -> unit; - mkdir : string -> int -> unit; - unlink : string -> unit; - rmdir : string -> unit; - symlink : string -> string -> unit; - rename : string -> string -> unit; - link : string -> string -> unit; - chmod : string -> int -> unit; - chown : string -> int -> int -> unit; - truncate : string -> int64 -> unit; - utime : string -> float -> float -> unit; - fopen : string -> Unix.open_flag list -> int option; (* TODO: optional arguments missing *) - read : string -> buffer -> int64 -> int -> int; (* TODO: optional arguments missing *) - write : string -> buffer -> int64 -> int -> int; (* TODO: optional arguments missing *) - statfs : string -> Unix_util.statvfs; - flush : string -> int -> unit; (* TODO: optional arguments missing *) - release : string -> Unix.open_flag list -> int -> unit; (* TODO: optional arguments missing *) - fsync : string -> bool -> int -> unit; (* TODO: optional arguments missing *) - setxattr : string -> string -> string -> xattr_flags -> unit; - getxattr : string -> string -> string; - listxattr : string -> string list; - removexattr : string -> string -> unit; - opendir : string -> Unix.open_flag list -> int option; (* TODO: optional arguments missing *) - readdir : string -> int -> string list; (* TODO: optional arguments missing *) - releasedir : string -> Unix.open_flag list -> int -> unit; (* TODO: optional arguments missing *) - fsyncdir : string -> bool -> int -> unit; (* TODO: optional arguments missing *) - init : unit -> unit; (* TODO: optional arguments missing and return value missing *) - } - +type operations = { + getattr : string -> Unix.LargeFile.stats; + readlink : string -> string; + mknod : string -> Unix.file_kind -> Unix.file_perm -> int -> unit; + mkdir : string -> int -> unit; + unlink : string -> unit; + rmdir : string -> unit; + symlink : string -> string -> unit; + rename : string -> string -> unit; + link : string -> string -> unit; + chmod : string -> int -> unit; + chown : string -> int -> int -> unit; + truncate : string -> int64 -> unit; + utime : string -> float -> float -> unit; + fopen : string -> Unix.open_flag list -> int option; + (* TODO: optional arguments missing *) + read : string -> buffer -> int64 -> int -> int; + (* TODO: optional arguments missing *) + write : string -> buffer -> int64 -> int -> int; + (* TODO: optional arguments missing *) + statfs : string -> Unix_util.statvfs; + flush : string -> int -> unit; + (* TODO: optional arguments missing *) + release : string -> Unix.open_flag list -> int -> unit; + (* TODO: optional arguments missing *) + fsync : string -> bool -> int -> unit; + (* TODO: optional arguments missing *) + setxattr : string -> string -> string -> xattr_flags -> unit; + getxattr : string -> string -> string; + listxattr : string -> string list; + removexattr : string -> string -> unit; + opendir : string -> Unix.open_flag list -> int option; + (* TODO: optional arguments missing *) + readdir : string -> int -> string list; + (* TODO: optional arguments missing *) + releasedir : string -> Unix.open_flag list -> int -> unit; + (* TODO: optional arguments missing *) + fsyncdir : string -> bool -> int -> unit; + (* TODO: optional arguments missing *) + init : unit -> unit; + (* TODO: optional arguments missing and return value missing *) + destroy : unit -> unit; +} + let op_names_of_operations ops = - { Fuse_bindings.init = Fuse_lib.named_op ops.init; + { + Fuse_bindings.init = Fuse_lib.named_op ops.init; + Fuse_bindings.destroy = Fuse_lib.named_op ops.destroy; Fuse_bindings.getattr = Fuse_lib.named_op ops.getattr; Fuse_bindings.readlink = Fuse_lib.named_op ops.readlink; Fuse_bindings.readdir = Fuse_lib.named_op_2 ops.readdir; @@ -93,21 +111,19 @@ let op_names_of_operations ops = Fuse_bindings.flush = Fuse_lib.named_op_2 ops.flush; Fuse_bindings.statfs = Fuse_lib.named_op ops.statfs; Fuse_bindings.fsync = Fuse_lib.named_op_3 ops.fsync; - Fuse_bindings.listxattr = Fuse_lib.named_op - (fun path -> - let s = ops.listxattr path in - (s,List.fold_left - (fun acc s -> - acc + 1 + (String.length s)) - 0 s)); + Fuse_bindings.listxattr = + Fuse_lib.named_op (fun path -> + let s = ops.listxattr path in + (s, List.fold_left (fun acc s -> acc + 1 + String.length s) 0 s)); Fuse_bindings.getxattr = Fuse_lib.named_op_2 ops.getxattr; Fuse_bindings.setxattr = Fuse_lib.named_op_4 ops.setxattr; Fuse_bindings.removexattr = Fuse_lib.named_op_2 ops.removexattr; } -let default_operations = +let default_operations = { init = undefined; + destroy = undefined; getattr = undefined; readdir = undefined; opendir = undefined; @@ -135,7 +151,7 @@ let default_operations = listxattr = undefined; getxattr = undefined; setxattr = undefined; - removexattr = undefined; + removexattr = undefined; } let main argv ops = diff --git a/src/ocamlfuse/Fuse_bindings.idl b/src/ocamlfuse/Fuse_bindings.idl index 7940f2dc..544b95f8 100644 --- a/src/ocamlfuse/Fuse_bindings.idl +++ b/src/ocamlfuse/Fuse_bindings.idl @@ -23,9 +23,10 @@ applejack@users.sf.net vincenzo_ml@yahoo.it */ - +quote(h,"#define FUSE_USE_VERSION 26") quote(h,"#include ") + typedef [abstract] void * fuse; quote(mlmli,"type fuse_operations") quote(mlmli,"type fuse_cmd") @@ -34,6 +35,7 @@ typedef [string] char * str; struct fuse_operation_names { [string,unique] char * init; + [string,unique] char * destroy; [string,unique] char * getattr; [string,unique] char * readlink; [string,unique] char * readdir; @@ -79,11 +81,11 @@ quote(h,"#define __file_info file_info"); [ptr] struct fuse_operations * get_fuse_operations(); void set_fuse_operations([ref] const struct fuse_operation_names * op); -[blocking,ptr] struct fuse_cmd * __fuse_read_cmd([ptr,in] struct fuse *f); -[blocking] void __fuse_process_cmd([ptr] struct fuse *f,[ptr,in] struct fuse_cmd *cmd); +[blocking,ptr] struct fuse_cmd * fuse_read_cmd([ptr,in] struct fuse *f); +[blocking] void fuse_process_cmd([ptr] struct fuse *f,[ptr,in] struct fuse_cmd *cmd); void ml_fuse_init(); void ml_fuse_main(int argc,[size_is(argc)] str argv[],[ptr] const struct fuse_operations *op); -[blocking] boolean __fuse_exited([ptr] struct fuse * f); +[blocking] boolean fuse_exited([ptr] struct fuse * f); diff --git a/src/ocamlfuse/Fuse_lib.ml b/src/ocamlfuse/Fuse_lib.ml index a78941de..696a18b3 100644 --- a/src/ocamlfuse/Fuse_lib.ml +++ b/src/ocamlfuse/Fuse_lib.ml @@ -27,137 +27,114 @@ open Fuse_bindings open String open Thread -open Result +open Fuse_result let _ = Callback.register "ocaml_list_length" List.length external is_null : 'a Com.opaque -> bool = "ocaml_fuse_is_null" -let undefined _ = raise (Unix.Unix_error (Unix.ENOSYS,"undefined","")) - -let worker_thread (q, m, c) = - Mutex.lock m; - while true do - while Queue.length q == 0 do - Condition.wait c m - done; - let (x, y) = Queue.take q in - Mutex.unlock m; - ignore (x y); - Mutex.lock m - done - -let fuse_loop fuse (multithreaded) = - let q = Queue.create () in - let m = Mutex.create () in - let c = Condition.create () in - for i = 0 to 1 do - ignore (Thread.create worker_thread (q, m, c)); - done; +let undefined _ = raise (Unix.Unix_error (Unix.ENOSYS, "undefined", "")) + +let fuse_loop fuse multithreaded = + let thread_pool = Thread_pool.create () in let f = - if multithreaded (* TODO: thread pooling instead of creation? *) - then fun x y -> - Mutex.lock m; - Queue.add (x, y); - Mutex.unlock m; - Condition.signal c - else fun x y -> ignore (x y) + if multithreaded then fun f x -> Thread_pool.add_work f x thread_pool + else fun f x -> ignore (f x) in - while not (__fuse_exited fuse) do - let cmd = __fuse_read_cmd fuse in - if not (is_null cmd) - then f (__fuse_process_cmd fuse) cmd - done + while not (fuse_exited fuse) do + let cmd = fuse_read_cmd fuse in + if not (is_null cmd) then f (fuse_process_cmd fuse) cmd + done; + Thread_pool.shutdown thread_pool let _ = Callback.register "ocaml_fuse_loop" fuse_loop -let default_op_names = { - init = None; - getattr = None; - readlink = None; - readdir = None; - opendir = None; - releasedir = None; - fsyncdir = None; - mknod = None; - mkdir = None; - unlink = None; - rmdir = None; - symlink = None; - rename = None; - link = None; - chmod = None; - chown = None; - truncate = None; - utime = None; - fopen = None; - read = None; - write = None; - statfs = None; - flush = None; - release = None; - fsync = None; - setxattr = None; - getxattr = None; - listxattr = None; - removexattr = None; -} +let default_op_names = + { + init = None; + destroy = None; + getattr = None; + readlink = None; + readdir = None; + opendir = None; + releasedir = None; + fsyncdir = None; + mknod = None; + mkdir = None; + unlink = None; + rmdir = None; + symlink = None; + rename = None; + link = None; + chmod = None; + chown = None; + truncate = None; + utime = None; + fopen = None; + read = None; + write = None; + statfs = None; + flush = None; + release = None; + fsync = None; + setxattr = None; + getxattr = None; + listxattr = None; + removexattr = None; + } let start = ref 0 -let supply () = + +let supply () = let r = !start in - start := !start + 1; - "__caml_cb_" ^ (string_of_int r) + start := !start + 1; + "__caml_cb_" ^ string_of_int r let named_op f = - if f == undefined - then None - else - let cb x = - try Ok (f x) - with - Unix.Unix_error (err,_,_) -> Bad err - | _ -> Bad Unix.ERANGE (* TODO: find a better way to signal the user and log this *) + if f == undefined then None + else + let cb x = + try Ok (f x) with + | Unix.Unix_error (err, _, _) -> Bad err + | _ -> Bad Unix.ERANGE + (* TODO: find a better way to signal the user and log this *) in let name = supply () in - Callback.register name cb; - Some name + Callback.register name cb; + Some name let named_op_2 f = - if f == undefined - then None - else - let cb x y = - try Ok (f x y) - with - Unix.Unix_error (err,_,_) -> Bad err - | _ -> Bad Unix.ERANGE in + if f == undefined then None + else + let cb x y = + try Ok (f x y) with + | Unix.Unix_error (err, _, _) -> Bad err + | _ -> Bad Unix.ERANGE + in let name = supply () in - Callback.register name cb; - Some name + Callback.register name cb; + Some name let named_op_3 f = - if f == undefined - then None - else - let cb x y z = - try Ok (f x y z) - with - Unix.Unix_error (err,_,_) -> Bad err - | _ -> Bad Unix.ERANGE in + if f == undefined then None + else + let cb x y z = + try Ok (f x y z) with + | Unix.Unix_error (err, _, _) -> Bad err + | _ -> Bad Unix.ERANGE + in let name = supply () in - Callback.register name cb; - Some name + Callback.register name cb; + Some name let named_op_4 f = - if f == undefined - then None - else - let cb x y z t = - try Ok (f x y z t) - with - Unix.Unix_error (err,_,_) -> Bad err - | _ -> Bad Unix.ERANGE in + if f == undefined then None + else + let cb x y z t = + try Ok (f x y z t) with + | Unix.Unix_error (err, _, _) -> Bad err + | _ -> Bad Unix.ERANGE + in let name = supply () in - Callback.register name cb; - Some name + Callback.register name cb; + Some name diff --git a/src/ocamlfuse/Result.ml b/src/ocamlfuse/Fuse_result.ml similarity index 100% rename from src/ocamlfuse/Result.ml rename to src/ocamlfuse/Fuse_result.ml diff --git a/src/ocamlfuse/Fuse_util.c b/src/ocamlfuse/Fuse_util.c index 27c1c8dc..61cd1fb6 100644 --- a/src/ocamlfuse/Fuse_util.c +++ b/src/ocamlfuse/Fuse_util.c @@ -56,11 +56,15 @@ #define min(a,b) (adim) dim=src[srcdim]; + if (src[srcdim]+1>dim) dim=src[srcdim]+1; srcdim++; } @@ -275,6 +279,7 @@ int ml2c_unix_file_kind[] = void ml2c_Unix_stats_struct_stat(value v,struct stat * s) { + CAMLparam1(v); memset(s,0,sizeof(*s)); s->st_dev=Int_val(Field(v,0)); s->st_ino=Int_val(Field(v,1)); @@ -289,10 +294,12 @@ void ml2c_Unix_stats_struct_stat(value v,struct stat * s) s->st_atime=Double_val(Field(v,9)); s->st_mtime=Double_val(Field(v,10)); s->st_ctime=Double_val(Field(v,11)); + CAMLreturn0; } void ml2c_Unix_struct_statvfs(value v,struct statvfs * st) { + CAMLparam1(v); memset(st,0,sizeof(*st)); st->f_bsize = Int64_val(Field(v,0)); st->f_frsize = Int64_val(Field(v,1)); @@ -305,7 +312,7 @@ void ml2c_Unix_struct_statvfs(value v,struct statvfs * st) st->f_fsid = Int64_val(Field(v,8)); st->f_flag = Int64_val(Field(v,9)); st->f_namemax = Int64_val(Field(v,10)); - + CAMLreturn0; /* TODO: check the meaning of the following missing field: __f_spare */ @@ -364,20 +371,24 @@ void ml2c_Unix_struct_statvfs(value v,struct statvfs * st) static struct fuse_operations ops = { FOR_ALL_OPS(SET_NULL_OP) + .destroy = NULL, }; -static value * ocaml_list_length=NULL; +static const value * ocaml_list_length=NULL; -#define DECLARE_OP_CLOSURE(OPNAME) static value * OPNAME##_closure=NULL; +#define DECLARE_OP_CLOSURE(OPNAME) static const value * OPNAME##_closure=NULL; FOR_ALL_OPS(DECLARE_OP_CLOSURE) +static const value * destroy_closure = NULL; #define init_ARGS (struct fuse_conn_info *conn) +#define init_CALL_ARGS (conn) #define init_RTYPE void * #define init_CB vres=callback(*init_closure,Val_unit); /* TODO: the result from init is wrong, it should return unit */ #define init_RES #define getattr_ARGS (const char* path, struct stat * buf) +#define getattr_CALL_ARGS (path, buf) #define getattr_RTYPE int #define getattr_CB vpath = copy_string(path); vres=callback(*getattr_closure,vpath); #define getattr_RES \ @@ -385,6 +396,7 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) /* TODO: allow ocaml to use the offset and the stat argument of the filler */ #define readdir_ARGS (const char * path, void * buf, fuse_fill_dir_t filler, off_t offset, struct fuse_file_info * info) +#define readdir_CALL_ARGS (path, buf, filler, offset, info) #define readdir_RTYPE int #define readdir_CB vpath = copy_string(path); vres=callback2(*readdir_closure,vpath,Val_int(info->fh)); #define readdir_RES \ @@ -397,31 +409,37 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) } #define mknod_ARGS (const char *path, mode_t mode, dev_t rdev) +#define mknod_CALL_ARGS (path, mode, rdev) #define mknod_RTYPE int #define mknod_CB vpath = copy_string(path); vres=callback4(*mknod_closure,vpath,c2ml_mode_t_kind(mode),c2ml_mode_t_perm(mode),Val_int(rdev)); #define mknod_RES #define mkdir_ARGS (const char *path, mode_t mode) +#define mkdir_CALL_ARGS (path, mode) #define mkdir_RTYPE int #define mkdir_CB vpath = copy_string(path); vres=callback2(*mkdir_closure,vpath,Val_int(mode)); #define mkdir_RES #define unlink_ARGS (const char *path) +#define unlink_CALL_ARGS (path) #define unlink_RTYPE int #define unlink_CB vpath = copy_string(path); vres=callback(*unlink_closure,vpath); #define unlink_RES #define rmdir_ARGS (const char *path) +#define rmdir_CALL_ARGS (path) #define rmdir_RTYPE int #define rmdir_CB vpath = copy_string(path); vres=callback(*rmdir_closure,vpath); #define rmdir_RES #define readlink_ARGS (const char *path, char *buf, size_t size) +#define readlink_CALL_ARGS (path, buf, size) #define readlink_RTYPE int #define readlink_CB vpath = copy_string(path); vres=callback(*readlink_closure,vpath); #define readlink_RES strncpy(buf,String_val(Field(vres,0)),size-1); #define symlink_ARGS (const char *path, const char *dest) +#define symlink_CALL_ARGS (path, dest) #define symlink_RTYPE int #define symlink_CB \ vpath = copy_string(path); \ @@ -430,6 +448,7 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) #define symlink_RES #define rename_ARGS (const char *path, const char *dest) +#define rename_CALL_ARGS (path, dest) #define rename_RTYPE int #define rename_CB \ vpath = copy_string(path); \ @@ -438,6 +457,7 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) #define rename_RES #define link_ARGS (const char *path, const char *dest) +#define link_CALL_ARGS (path, dest) #define link_RTYPE int #define link_CB \ vpath = copy_string(path); \ @@ -446,36 +466,43 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) #define link_RES #define chmod_ARGS (const char *path, mode_t mode) +#define chmod_CALL_ARGS (path, mode) #define chmod_RTYPE int #define chmod_CB vpath = copy_string(path); vres=callback2(*chmod_closure,vpath,Val_int(mode)); #define chmod_RES #define chown_ARGS (const char *path, uid_t uid, gid_t gid) +#define chown_CALL_ARGS (path, uid, gid) #define chown_RTYPE int #define chown_CB vpath = copy_string(path); vres=callback3(*chown_closure,vpath,Val_int(uid),Val_int(gid)); #define chown_RES #define truncate_ARGS (const char *path, off_t size) +#define truncate_CALL_ARGS (path, size) #define truncate_RTYPE int #define truncate_CB vpath = copy_string(path); vres=callback2(*truncate_closure,vpath,copy_int64(size)); #define truncate_RES #define utime_ARGS (const char *path, struct utimbuf *buf) +#define utime_CALL_ARGS (path, buf) #define utime_RTYPE int #define utime_CB vpath = copy_string(path); vres=callback3(*utime_closure,vpath,copy_double(buf->actime),copy_double(buf->modtime)); #define utime_RES #define open_ARGS (const char *path, struct fuse_file_info *fi) +#define open_CALL_ARGS (path, fi) #define open_RTYPE int #define open_CB vpath = copy_string(path); vres=callback2(*open_closure,vpath,c_flags_to_open_flag_list(fi->flags)); #define open_RES if (Field(vres,0) != Val_int(0)) fi->fh = Int_val(Field(Field(vres,0),0)); #define opendir_ARGS (const char *path, struct fuse_file_info *fi) +#define opendir_CALL_ARGS (path, fi) #define opendir_RTYPE int #define opendir_CB vpath = copy_string(path); vres=callback2(*opendir_closure,vpath,c_flags_to_open_flag_list(fi->flags)); #define opendir_RES if (Field(vres,0) != Val_int(0)) fi->fh = Int_val(Field(Field(vres,0),0)); #define read_ARGS (const char *path, char *buf, size_t size, off_t offset,struct fuse_file_info * fi) +#define read_CALL_ARGS (path, buf, size, offset,fi) #define read_RTYPE int #define read_CB \ vpath = copy_string(path); \ @@ -483,6 +510,7 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) #define read_RES res=Int_val(Field(vres,0)); #define write_ARGS (const char *path, const char *buf, size_t size,off_t offset,struct fuse_file_info * fi) /* TODO: check usage of the writepages field of fi */ +#define write_CALL_ARGS (path, buf, size,offset,fi) #define write_RTYPE int #define write_CB \ vpath = copy_string(path); \ @@ -490,45 +518,53 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) #define write_RES res=Int_val(Field(vres,0)); #define release_ARGS (const char *path, struct fuse_file_info * fi) +#define release_CALL_ARGS (path, fi) #define release_RTYPE int #define release_CB vpath = copy_string(path); vres=callback3(*release_closure,vpath,c_flags_to_open_flag_list(fi->flags),Val_int(fi->fh)); #define release_RES #define releasedir_ARGS (const char *path, struct fuse_file_info * fi) +#define releasedir_CALL_ARGS (path, fi) #define releasedir_RTYPE int #define releasedir_CB vpath = copy_string(path); vres=callback3(*releasedir_closure,vpath,c_flags_to_open_flag_list(fi->flags),Val_int(fi->fh)); #define releasedir_RES #define flush_ARGS (const char *path,struct fuse_file_info * fi) +#define flush_CALL_ARGS (path, fi) #define flush_RTYPE int #define flush_CB vpath = copy_string(path); vres=callback2(*flush_closure,vpath,Val_int(fi->fh)); #define flush_RES #define statfs_ARGS (const char *path, struct statvfs *stbuf) +#define statfs_CALL_ARGS (path, stbuf) #define statfs_RTYPE int #define statfs_CB vpath = copy_string(path); vres=callback(*statfs_closure,vpath); #define statfs_RES ml2c_Unix_struct_statvfs(Field(vres,0),stbuf); #define fsync_ARGS (const char *path, int isdatasync,struct fuse_file_info * fi) +#define fsync_CALL_ARGS (path, isdatasync, fi) #define fsync_RTYPE int #define fsync_CB vpath = copy_string(path); vres=callback3(*fsync_closure,vpath,Val_bool(isdatasync),Val_int(fi->fh)); #define fsync_RES #define fsyncdir_ARGS (const char *path, int isdatasync,struct fuse_file_info * fi) +#define fsyncdir_CALL_ARGS (path, isdatasync, fi) #define fsyncdir_RTYPE int #define fsyncdir_CB vpath = copy_string(path); vres=callback3(*fsync_closure,vpath,Val_bool(isdatasync),Val_int(fi->fh)); #define fsyncdir_RES #define setxattr_ARGS (const char *path, const char *name, const char *val,size_t size,int flags) +#define setxattr_CALL_ARGS (path, name, val, size, flags) #define setxattr_RTYPE int #define setxattr_CB \ vpath = copy_string(path); \ vstring = alloc_string(size); \ - memcpy(String_val(vstring),val,size); \ + memcpy(&Byte(String_val(vstring),0),val,size); \ vres=callback4(*setxattr_closure,vpath,copy_string(name),vstring,c2ml_setxattr_flags(flags)); #define setxattr_RES #define getxattr_ARGS (const char *path, const char *name, char *val,size_t size) +#define getxattr_CALL_ARGS (path, name, val, size) #define getxattr_RTYPE int #define getxattr_CB \ vpath = copy_string(path); \ @@ -546,6 +582,7 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) } #define listxattr_ARGS (const char *path, char *list, size_t size) +#define listxattr_CALL_ARGS (path, list, size) #define listxattr_RTYPE int #define listxattr_CB vpath = copy_string(path); vres=callback(*listxattr_closure,vpath); #define listxattr_RES \ @@ -579,37 +616,57 @@ FOR_ALL_OPS(DECLARE_OP_CLOSURE) } #define removexattr_ARGS (const char *path, const char *name) +#define removexattr_CALL_ARGS (path, name) #define removexattr_RTYPE int #define removexattr_CB vpath = copy_string(path); vres=callback2(*removexattr_closure,vpath,copy_string(name)); #define removexattr_RES #define CALLBACK(OPNAME) \ -static OPNAME##_RTYPE ops_##OPNAME OPNAME##_ARGS \ -{ \ - leave_blocking_section(); \ - value vstring; \ - value vpath; \ - value vres; \ - value vtmp; \ - int res=-1; \ +static OPNAME##_RTYPE gm281_ops_##OPNAME OPNAME##_ARGS \ +{\ + CAMLparam0(); \ + CAMLlocal4(vstring, vpath, vres, vtmp); \ + OPNAME##_RTYPE res=(typeof (res))-1L; \ OPNAME##_CB \ if (Tag_val(vres)==1) /* Result is not Bad */ \ { \ - res=0; \ + res=(typeof (res))0L; \ OPNAME##_RES /* res can be changed here */ \ } \ else \ { \ if (Is_block(Field(vres,0))) /* This is EUNKNOWNERR of int in ocaml */ \ - res=-Int_val(Field(Field(vres,0),0)); \ - else res=-ml2c_unix_error(Int_val(Field(vres,0))); \ + res=(typeof (res))(long)-Int_val(Field(Field(vres,0),0)); \ + else res=(typeof (res))(long)-ml2c_unix_error(Int_val(Field(vres,0))); \ } \ + CAMLreturnT(OPNAME##_RTYPE, res); \ +}\ +\ +static OPNAME##_RTYPE ops_##OPNAME OPNAME##_ARGS \ +{ \ + leave_blocking_section(); \ + OPNAME##_RTYPE ret = gm281_ops_##OPNAME OPNAME##_CALL_ARGS; \ enter_blocking_section(); \ - return res; \ + return ret; \ } FOR_ALL_OPS(CALLBACK) +static void gm281_ops_destroy (void *private_data) +{ + CAMLparam0(); + callback(*destroy_closure,Val_unit); + CAMLreturn0; +} + +static void ops_destroy (void *private_data) +{ + leave_blocking_section(); + gm281_ops_destroy (private_data); + enter_blocking_section(); +} + + #define SET_OPERATION(OPNAME) \ if (op->OPNAME==NULL) ops.OPNAME=NULL; \ else \ @@ -621,6 +678,12 @@ FOR_ALL_OPS(CALLBACK) void set_fuse_operations(struct fuse_operation_names const *op) { FOR_ALL_OPS(SET_OPERATION) + + if (op->destroy==NULL) ops.destroy=NULL; + else { + destroy_closure=caml_named_value(op->destroy); + ops.destroy=ops_destroy; + } } struct fuse_operations * get_fuse_operations() @@ -628,17 +691,19 @@ struct fuse_operations * get_fuse_operations() return &ops; } -value * ocaml_fuse_loop_closure; +const value * ocaml_fuse_loop_closure; int mainloop(struct fuse * f,int multithreaded) { + CAMLparam0(); if (f == NULL) return(-1); - value _fuse=alloc_small(1, Abstract_tag); - Field(_fuse, 0) = (value) f; + CAMLlocal1(_fuse); + _fuse=caml_alloc(1, Abstract_tag); + Store_field(_fuse, 0, (value) f); - return callback2(*ocaml_fuse_loop_closure,_fuse,Val_bool(multithreaded)); + CAMLreturnT(int, callback2(*ocaml_fuse_loop_closure,_fuse,Val_bool(multithreaded))); } void ml_fuse_init() @@ -660,12 +725,17 @@ void ml_fuse_main(int argc,str * argv,struct fuse_operations const * op) if (fuse!=NULL) { mainloop(fuse,multithreaded); + enter_blocking_section(); + // fuse_teardown will run the destroy() callback which will try to take + // the runtime lock, so we need to release it before fuse_teardown(fuse,mountpoint); + leave_blocking_section(); } } value ocaml_fuse_is_null(value v) /* For Com.opaque values */ { - return Val_bool(0==Field(v,0)); // Is this the right way to check for null? + CAMLparam1(v); + CAMLreturn(Val_bool(0==Field(v,0))); // Is this the right way to check for null? } diff --git a/src/ocamlfuse/META b/src/ocamlfuse/META deleted file mode 100644 index 1d60a7df..00000000 --- a/src/ocamlfuse/META +++ /dev/null @@ -1,5 +0,0 @@ -description = "ocaml fuse bindings" -requires = "" -version = "2.7.1" -archive(byte) = "Fuse.cma" -archive(native) = "Fuse.cmxa" diff --git a/src/ocamlfuse/Thread_pool.ml b/src/ocamlfuse/Thread_pool.ml new file mode 100644 index 00000000..3b1fdb6a --- /dev/null +++ b/src/ocamlfuse/Thread_pool.ml @@ -0,0 +1,67 @@ +(* + This file is part of the "OCamlFuse" library. + + OCamlFuse is free software; you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation (version 2 of the License). + + OCamlFuse is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with OCamlFuse. See the file LICENSE. If you haven't received + a copy of the GNU General Public License, write to: + + Free Software Foundation, Inc., + 59 Temple Place, Suite 330, Boston, MA + 02111-1307 USA + + Alessandro Strada + + alessandro.strada@gmail.com +*) + +type t = { + max_threads : int; + lock : Mutex.t; + condition : Condition.t; + table : (int, Thread.t) Hashtbl.t; +} + +let create ?(max_threads = 128) () = + { + max_threads; + lock = Mutex.create (); + condition = Condition.create (); + table = Hashtbl.create max_threads; + } + +let signal_work_done thread_id pool = + Mutex.lock pool.lock; + try + Hashtbl.remove pool.table thread_id; + Condition.signal pool.condition; + Mutex.unlock pool.lock + with _ -> Mutex.unlock pool.lock + +let add_work f x pool = + Mutex.lock pool.lock; + try + while Hashtbl.length pool.table >= pool.max_threads do + Condition.wait pool.condition pool.lock + done; + let f' x = + let thread = Thread.self () in + let thread_id = Thread.id thread in + let _ = f x in + signal_work_done thread_id pool + in + let thread = Thread.create f' x in + let thread_id = Thread.id thread in + Hashtbl.add pool.table thread_id thread; + Mutex.unlock pool.lock + with _ -> Mutex.unlock pool.lock + +let shutdown pool = Hashtbl.iter (fun _ thread -> Thread.join thread) pool.table diff --git a/src/ocamlfuse/Unix_util.ml b/src/ocamlfuse/Unix_util.ml index 9fbdf2e4..47f64637 100644 --- a/src/ocamlfuse/Unix_util.ml +++ b/src/ocamlfuse/Unix_util.ml @@ -24,13 +24,23 @@ vincenzo_ml@yahoo.it *) -open Result +open Fuse_result -external read_noexn : Unix.file_descr -> (char, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t -> int result = "unix_util_read" -external write_noexn : Unix.file_descr -> (char, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t -> int result = "unix_util_write" +external read_noexn : + Unix.file_descr -> + (char, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t -> + int result = "unix_util_read" -external int_of_file_descr : Unix.file_descr -> int = "unix_util_int_of_file_descr" -external file_descr_of_int : int -> Unix.file_descr = "unix_util_file_descr_of_int" +external write_noexn : + Unix.file_descr -> + (char, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t -> + int result = "unix_util_write" + +external int_of_file_descr : Unix.file_descr -> int + = "unix_util_int_of_file_descr" + +external file_descr_of_int : int -> Unix.file_descr + = "unix_util_file_descr_of_int" (* Statvfs code inspired by statfs code by Richard Jones and Damien Doligez, see: @@ -57,19 +67,19 @@ type statvfs = { external statvfs_noexn : string -> statvfs result = "unix_util_statvfs" -let statvfs path = +let statvfs path = match statvfs_noexn path with - Ok res -> res - | Bad err -> raise (Unix.Unix_error (err,"statvfs","")) + | Ok res -> res + | Bad err -> raise (Unix.Unix_error (err, "statvfs", "")) external fchdir : Unix.file_descr -> unit = "unix_util_fchdir" let read fd buf = match read_noexn fd buf with - Ok res -> res - | Bad err -> raise (Unix.Unix_error (err,"read","")) + | Ok res -> res + | Bad err -> raise (Unix.Unix_error (err, "read", "")) let write fd buf = match write_noexn fd buf with - Ok res -> res - | Bad err -> raise (Unix.Unix_error (err,"read","")) + | Ok res -> res + | Bad err -> raise (Unix.Unix_error (err, "read", "")) diff --git a/src/ocamlfuse/Unix_util_stubs.c b/src/ocamlfuse/Unix_util_stubs.c index c308e095..5c015871 100644 --- a/src/ocamlfuse/Unix_util_stubs.c +++ b/src/ocamlfuse/Unix_util_stubs.c @@ -24,10 +24,15 @@ vincenzo_ml@yahoo.it */ +#include #include #include #include +#if defined(__APPLE__) +#include +#else #include +#endif #include #include @@ -47,17 +52,23 @@ CAMLprim value unix_util_read(value fd,value buf) { CAMLparam2(fd,buf); CAMLlocal1(vres); - vres=alloc(1,1); /* Ok result */ int res; + int c_fd = Int_val(fd); /* TODO: unsafe coercion */ + void * c_data = Data_bigarray_val(buf); + int c_dim = Bigarray_val(buf)->dim[0]; + enter_blocking_section(); - res = read(Int_val(fd), /* TODO: unsafe coercion */ - Bigarray_val(buf)->data,Bigarray_val(buf)->dim[0]); + res = read(c_fd, c_data, c_dim); leave_blocking_section(); - if (res >=0) Field(vres,0)=Val_int(res); + if (res >=0) + { + vres=alloc(1,1); /* Ok result */ + Store_field(vres,0,Val_int(res)); + } else { - Tag_val(vres)=0; /* Bad result */ - Field(vres,0)=Val_int(c2ml_unix_error(res)); /* TODO: EUNKNOWN x is a block */ + vres=alloc(1,0); /* Bad result */ + Store_field(vres,0,Val_int(c2ml_unix_error(res))); /* TODO: EUNKNOWN x is a block */ } CAMLreturn (vres); } @@ -66,17 +77,23 @@ CAMLprim value unix_util_write(value fd,value buf) { CAMLparam2(fd,buf); CAMLlocal1(vres); - vres=alloc(1,1); /* Ok result */ int res; + int c_fd = Int_val(fd); /* TODO: unsafe coercion */ + void * c_data = Data_bigarray_val(buf); + int c_dim = Bigarray_val(buf)->dim[0]; + enter_blocking_section(); - res = write(Int_val(fd), /* TODO: unsafe coercion */ - Bigarray_val(buf)->data,Bigarray_val(buf)->dim[0]); + res = write(c_fd, c_data, c_dim); leave_blocking_section(); - if (res >=0) Field(vres,0)=Val_int(res); + if (res >=0) + { + vres=alloc(1,1); /* Ok result */ + Store_field(vres,0,Val_int(res)); + } else { - Tag_val(vres)=0; /* Bad result */ - Field(vres,0)=Val_int(c2ml_unix_error(res)); /* TODO: EUNKNOWN x is a block */ + vres=alloc(1,0); /* Bad result */ + Store_field(vres,0,Val_int(c2ml_unix_error(res))); /* TODO: EUNKNOWN x is a block */ } CAMLreturn (vres); } @@ -134,12 +151,12 @@ CAMLprim value unix_util_statvfs (value pathv) if (res >=0) { bufv = copy_statvfs (&buf); - Field(vres,0)=bufv; + Store_field(vres,0,bufv); } else { Tag_val(vres)=0; /* Bad result */ - Field(vres,0)=Val_int(c2ml_unix_error(res)); /* TODO: EUNKNOWN x is a block */ + Store_field(vres,0,Val_int(c2ml_unix_error(res))); /* TODO: EUNKNOWN x is a block */ } CAMLreturn (vres); } diff --git a/src/ocamlfuse/config/discover.ml b/src/ocamlfuse/config/discover.ml new file mode 100644 index 00000000..a675aa99 --- /dev/null +++ b/src/ocamlfuse/config/discover.ml @@ -0,0 +1,52 @@ +module C = Configurator.V1 + +let read_file path = + let in_ch = open_in path in + let rec loop acc = + try + let line = input_line in_ch in + loop (acc ^ line) + with End_of_file -> acc + in + try + let result = loop "" in + close_in in_ch; + result + with exc -> + close_in in_ch; + Printf.eprintf "read_file: could not read file: '%s'" path; + raise exc + +let () = + C.main ~name:"foo" (fun c -> + let default : C.Pkg_config.package_conf = + { libs = [ "-lfuse" ]; cflags = [] } + in + let conf = + match C.Pkg_config.get c with + | Some pkgc -> ( + match C.Pkg_config.query pkgc ~package:"fuse" with + | Some flags -> flags + | None -> default ) + | None -> default + in + let calmidl_fname = "camlidl.libs.sexp" in + let camlidl_lib_path = + match + Sys.command + (Printf.sprintf "opam var camlidl:lib > %s" calmidl_fname) + with + | 0 -> String.trim (read_file calmidl_fname) + | _ -> ( + match + Sys.command + (Printf.sprintf "ocamlfind query camlidl > %s" calmidl_fname) + with + | 0 -> String.trim (read_file calmidl_fname) + | _ -> C.die "Could not query camlidl lib path" ) + in + let camlidl_libs = [ "-L" ^ camlidl_lib_path; "-lcamlidl" ] in + C.Flags.( + write_sexp calmidl_fname camlidl_libs; + write_sexp "fuse.cflags.sexp" conf.cflags; + write_sexp "fuse.libs.sexp" conf.libs)) diff --git a/src/ocamlfuse/config/dune b/src/ocamlfuse/config/dune new file mode 100644 index 00000000..21a5f9a5 --- /dev/null +++ b/src/ocamlfuse/config/dune @@ -0,0 +1,3 @@ +(executable + (name discover) + (libraries dune.configurator)) diff --git a/src/ocamlfuse/dune b/src/ocamlfuse/dune new file mode 100644 index 00000000..eab562f6 --- /dev/null +++ b/src/ocamlfuse/dune @@ -0,0 +1,19 @@ +(library + (name fuse) + (libraries unix threads bigarray camlidl) + (flags -thread) + (foreign_stubs + (language c) + (names Fuse_bindings_stubs Fuse_util Unix_util_stubs) + (flags (:include fuse.cflags.sexp))) + (c_library_flags ((:include fuse.libs.sexp) (:include camlidl.libs.sexp)))) + +(rule + (targets fuse.libs.sexp fuse.cflags.sexp camlidl.libs.sexp) + (deps (:discover config/discover.exe)) + (action (run %{discover}))) + +(rule + (targets Fuse_bindings.h Fuse_bindings_stubs.c Fuse_bindings.ml Fuse_bindings.mli) + (deps Fuse_bindings.idl) + (action (run camlidl -header Fuse_bindings.idl)))