(*
In order to showing that the test coverage is 100%, we mark with
special comments the lines that are irrelevant and unreachable.
Legend:
coverage:unused
lines that are meant to not be tested for now;
coverage:linux:irrelevant
coverage:mac_os_x:irrelevant
lines that become irrelevant when the spec is
initialised with a different architecture;
coverage:impossible
lines that we know cannot be reached (e.g. impossible cases of the spec);
coverage:fixme
lines that should be reached, but there are not test cases for them yet.
*)
open import Bool Maybe Maybe_extra Basic_classes Tuple Num Set List List_extra Word Either Assert_extra String Function
open import T_list_array T_fs_prelude
open import {ocaml} `Lem_support`
open import {ocaml} `Sexplib.Std`
open import {ocaml} `Sexplib.Conv`
(******************************************************************************)
(* Fs_types *)
(* *)
(* Types common to all implementations of the basic operations *)
(******************************************************************************)
module Fs_types = struct
open T_fs_prelude
(*-------------------------------*)
(* miscellaneous types *)
(*-------------------------------*)
type ty_bytes = T_list_array.t (*o with sexp o*) (* FIXME may want to change this to string? or parameterize? FIXME also want option of null pointer; FIXME also there are bytes passed in by user and bytes used to store file data, and these are probably not the same *)
type file_contents = ty_bytes (*o with sexp_of o*) (* really a map from index to ... *)
type name = string (*o with sexp o*) (* shortest component of a filename - doesn't include /; may be empty; may be . or .. *)
(* type ty_dirname = list string
type ty_filename = list string (* non-empty *) *)
type size_t = nat (*o with sexp o*) (* unsigned integer of at least 16 bits http://stackoverflow.com/questions/2550774/what-is-size-t-in-c *) (* FIXME note that these parameters are never added to, or subtracted, or otherwise operated on in this spec, they are only supplied by user, or returned e.g. as result of a read; thus we don't need to worry about the fact that they may use a finite number of bits *)
type off_t = int (*o with sexp o*) (* singed integer type; FIXME cross reference this with posix *)
type float_t = Float of nat (*o with sexp o*) (* FIXME *)
(*-------------------------------*)
(* cstring *)
(*-------------------------------*)
type cstring = CS_Null | CS_Some of string (*o with sexp o*)
val string_of_cstring : cstring -> string
let string_of_cstring cs = match cs with
| CS_Null -> "" (* coverage:unused *)
| CS_Some s -> s (* coverage:unused *)
end
val bytes_of_cstring : cstring -> ty_bytes
let bytes_of_cstring cs = (match cs with
| CS_Null -> (T_list_array.of_string "")
| CS_Some s -> (T_list_array.of_string s)
end)
val cstring_of_bytes : ty_bytes -> cstring
let cstring_of_bytes bs = (CS_Some (T_list_array.to_string bs))
(*-------------------------------*)
(* File descriptors, per process *)
(*-------------------------------*)
type ty_fd = FD of nat (*o with sexp o*)
let ty_fd_compare (FD n0) (FD n1) = compare n0 n1
instance ( SetType ty_fd )
let setElemCompare = ty_fd_compare
end
val dest_FD : ty_fd -> nat
let dest_FD x = (match x with FD n -> n end)
(*-------------------------------*)
(* directory handles, per process*)
(*-------------------------------*)
type ty_dh = DH of nat (*o with sexp o*)
let ty_dh_compare (DH n0) (DH n1) = compare n0 n1
instance ( SetType ty_dh )
let setElemCompare = ty_dh_compare
end
val dest_DH : ty_dh -> nat
let dest_DH x = (match x with DH n -> n end)
(*-------------------------------*)
(* Inodes *)
(*-------------------------------*)
type inode = Inode of nat (*o with sexp o*)
let inode_compare (Inode n0) (Inode n1) = compare n0 n1
instance ( SetType inode )
let setElemCompare = inode_compare
end
val dest_Inode : inode -> nat
let dest_Inode x = (match x with Inode n -> n end)
(*-------------------------------*)
(* Errors *)
(*-------------------------------*)
(* the following note discusses modeling of errors: posix/base_definitions/errno.h.txt *)
type error =
E2BIG
| EACCES
| EAGAIN
| EBADF
| EBUSY
| ECHILD
| EDEADLK
| EDOM
| EEXIST
| EFAULT
| EFBIG
| EINTR
| EINVAL
| EIO
| EISDIR
| EMFILE
| EMLINK
| ENAMETOOLONG
| ENFILE
| ENODEV
| ENOENT
| ENOEXEC
| ENOLCK
| ENOMEM
| ENOSPC
| ENOSYS
| ENOTDIR
| ENOTEMPTY
| ENOTTY
| ENXIO
| EPERM
| EPIPE
| ERANGE
| EROFS
| ESPIPE
| ESRCH
| EXDEV
| EWOULDBLOCK
| EINPROGRESS
| EALREADY
| ENOTSOCK
| EDESTADDRREQ
| EMSGSIZE
| EPROTOTYPE
| ENOPROTOOPT
| EPROTONOSUPPORT
| ESOCKTNOSUPPORT
| EOPNOTSUPP
| EPFNOSUPPORT
| EAFNOSUPPORT
| EADDRINUSE
| EADDRNOTAVAIL
| ENETDOWN
| ENETUNREACH
| ENETRESET
| ECONNABORTED
| ECONNRESET
| ENOBUFS
| EISCONN
| ENOTCONN
| ESHUTDOWN
| ETOOMANYREFS
| ETIMEDOUT
| ECONNREFUSED
| EHOSTDOWN
| EHOSTUNREACH
| ELOOP
| EOVERFLOW
| EUNKNOWNERR of int (*o with sexp o*)
instance (Eq error)
let (=) = unsafe_structural_equality
let (<>) = unsafe_structural_inequality
end
(*-------------------------------*)
(* Errors or Values *)
(*-------------------------------*)
type error_or_value 'a = Error of error | Value of 'a (*o with sexp o*)
val error_or_valueEqual : forall 'a. Eq 'a => error_or_value 'a -> error_or_value 'a -> bool
let error_or_valueEqual eov1 eov2 = (match (eov1, eov2) with
| (Error e1, Error e2) -> (e1 = e2)
| (Value v1, Value v2) -> (v1 = v2)
| (_, _) -> false (* coverage:fixme -this case is covered only if the checker finds discrepancies with the posix results *)
end)
let inline {hol;isabelle} error_or_valueEqual = unsafe_structural_equality
instance forall 'a. Eq 'a => (Eq (error_or_value 'a))
let (=) = error_or_valueEqual
let (<>) x y = not (error_or_valueEqual x y)
end
val is_Error : forall 'a. error_or_value 'a -> bool
let is_Error x = (match x with | Error _ -> true | _ -> false end)
val is_Value : forall 'a. error_or_value 'a -> bool
let is_Value x = (match x with | Value _ -> true | _ -> false end)
(*-------------------------------*)
(* Open flags *)
(*-------------------------------*)
type int_open_flags = int32 (*o with sexp o*)
(* from unix.mli *)
(* FIXME extend these to use open flags listed here http://pubs.opengroup.org/onlinepubs/9699919799/ *)
type open_flag =
| O_EXEC
| O_RDONLY (** Open for reading *)
| O_RDWR (** Open for reading and writing *)
| O_SEARCH
| O_WRONLY (** Open for writing *)
| O_APPEND (** Open for append *)
| O_CLOEXEC
| O_CREAT (** Create if nonexistent *)
| O_DIRECTORY
| O_DSYNC (** Writes complete as Synchronised I/O data integrity completion *)
| O_EXCL (** Fail if existing *)
| O_NOCTTY (** Don't make this dev a controlling tty *)
| O_NOFOLLOW
| O_NONBLOCK (** Open in non-blocking mode *)
| O_RSYNC (** Reads complete as writes (depending on
O_SYNC/O_DSYNC) *)
| O_SYNC (** Writes complete as Synchronised I/O file
integrity completion *)
| O_TRUNC (** Truncate to 0 length if existing *)
| O_TTY_INIT (*o with sexp_of o*)
instance (Eq open_flag)
let (=) = unsafe_structural_equality
let (<>) = unsafe_structural_inequality
end
(* N.B. this should be the complete set of flags *)
val open_flags : finset open_flag
let open_flags = (finset_from_list [
O_EXEC;
O_RDONLY;
O_RDWR;
O_SEARCH;
O_WRONLY;
O_APPEND;
O_CLOEXEC;
O_CREAT;
O_DIRECTORY;
O_DSYNC;
O_EXCL;
O_NOCTTY;
O_NOFOLLOW;
O_NONBLOCK;
O_RSYNC;
O_SYNC;
O_TRUNC;
O_TTY_INIT;
])
(* a subset of the flags; exactly one must be provided for an open call *)
val access_mode_flags : finset open_flag
let access_mode_flags = (finset_from_list [O_EXEC;O_RDONLY;O_RDWR;O_SEARCH;O_WRONLY])
(* [open_flag_set_access_mode_ok] checks that a finite set of
open-flags contains exactly one access-mode flag *)
val open_flag_set_access_mode_ok : finset open_flag -> bool
let open_flag_set_access_mode_ok oflags = (* coverage:linux:irrelevant *)
let acc_flgs = finset_filter (fun flag -> finset_mem flag access_mode_flags) oflags in (* coverage:linux:irrelevant *)
finset_size acc_flgs = 1 (* coverage:linux:irrelevant *)
(*-------------------------------*)
(* File permissions *)
(*-------------------------------*)
type file_perm = File_perm of int32 (*o with sexp o*) (* TODO: actually only 12 bit, perhaps change *)
val dest_file_perm : file_perm -> int32
let dest_file_perm (File_perm p) = p
(*-------------------------------*)
(* Seek commands for lseek *)
(*-------------------------------*)
type int_seek_command = int (*o with sexp o*)
(* from unix.mli *)
type seek_command =
SEEK_SET (** indicates positions relative to the beginning of the file *)
| SEEK_CUR (** indicates positions relative to the current position *)
| SEEK_END (** indicates positions relative to the end of the file *)
| SEEK_DATA (** indicates positions relative to the current position that contain data *)
| SEEK_HOLE (*o with sexp_of o*) (** indicates positions relative to the current positions that do not contain data *)
instance (Eq seek_command)
let (=) = unsafe_structural_equality
let (<>) = unsafe_structural_inequality
end
(*-------------------------------*)
(* Kinds of files *)
(*-------------------------------*)
type file_kind =
S_IFBLK (* block special *) (* not handled in this spec *)
| S_IFCHR (* character special *) (* not handled in this spec *)
| S_IFIFO (* FIFO special *) (* not handled in this spec *)
| S_IFREG (* regular *)
| S_IFDIR (* directory *)
| S_IFLNK (* symbolic link *)
| S_IFSOCK (*o with sexp o*) (* socket *) (* not handled in this spec *)
instance (Eq file_kind)
let (=) = unsafe_structural_equality
let (<>) = unsafe_structural_inequality
end
(*-------------------------------*)
(* User and group ids *)
(*-------------------------------*)
type uid = User_id of nat (*o with sexp o*)
let uid_compare (User_id n0) (User_id n1) = compare n0 n1 (* coverage:unused *)
instance ( SetType uid )
let setElemCompare = uid_compare
end
instance (Eq uid)
let (=) = unsafe_structural_equality
let (<>) = unsafe_structural_inequality
end
let root_uid : uid = User_id 0
type gid = Group_id of nat (*o with sexp o*)
let gid_compare (Group_id n0) (Group_id n1) = compare n0 n1
instance ( SetType gid )
let setElemCompare = gid_compare
end
let root_gid : gid = Group_id 0
(*-------------------------------*)
(* result record for stat *)
(*-------------------------------*)
(* from ocaml source unix.mli *)
type ty_stats =
<| st_dev : int; (** Device number *)
st_ino : inode; (** Inode number *)
st_kind : file_kind; (** Kind of the file *)
st_perm : file_perm; (** Access rights *)
st_nlink : int; (** Number of links *)
st_uid : uid; (** User id of the owner *)
st_gid : gid; (** Group ID of the file's group *)
st_rdev : int; (** Device minor number *)
st_size : int64; (** Size in bytes; no sensible meaning for directories *)
st_atime : float_t; (** Last access time *)
st_mtime : float_t; (** Last modification time *)
st_ctime : float_t; (** Last status change time *)
|> (*o with sexp o*)
(*-------------------------------*)
(* Return values *)
(*-------------------------------*)
type ret_value =
RV_none
| RV_num of nat (* FIXME int? or change constructor name*)
| RV_bytes of ty_bytes (* FIXME add init return type *)
| RV_names of list name
| RV_stats of ty_stats
| RV_file_perm of file_perm (*o with sexp o*)
instance (Eq ret_value)
let (=) = unsafe_structural_equality
let (<>) = unsafe_structural_inequality
end
val dest_RV_bytes : ret_value -> ty_bytes
let dest_RV_bytes (RV_bytes bs) = bs
(* a dummy value, that is expected to never matter *)
val dummy_return_value : ret_value
let dummy_return_value = RV_none
(*-------------------------------*)
(* Entries *)
(*-------------------------------*)
(* We want to distinguish explicitly between directories and other files. Posix uses inodes
to point to these. Here we use abstract dir_ref for directories and file_refs for all
other files. Notice, that the Posix standard considers a directory to be a special file.
In the following we differ from that notation. *)
type entry 'dir_ref 'file_ref = Dir_ref_entry of 'dir_ref | File_ref_entry of 'file_ref (*o with sexp_of o*)
val is_dir_ref_entry : forall 'dir_ref 'file_ref. entry 'dir_ref 'file_ref -> bool
let is_dir_ref_entry e =
match e with
| Dir_ref_entry _ -> true (* coverage:impossible -is_dir_ref_entry is only used in pwrite, and the case in which this is called on a directory is impossoble *)
| File_ref_entry _ -> false end
val is_file_ref_entry : forall 'dir_ref 'file_ref. entry 'dir_ref 'file_ref -> bool
let is_file_ref_entry e =
match e with
| Dir_ref_entry _ -> false (* coverage:unused *)
| File_ref_entry _ -> true end (* coverage:unused *)
val dest_dir_ref_entry : forall 'dir_ref 'file_ref. entry 'dir_ref 'file_ref -> 'dir_ref
let dest_dir_ref_entry (Dir_ref_entry dr) = dr (* coverage:unused *)
val dest_file_ref_entry : forall 'dir_ref 'file_ref. entry 'dir_ref 'file_ref -> 'file_ref
let dest_file_ref_entry (File_ref_entry ir) = ir (* coverage:unused *)
(*-------------------------------*)
(* Non empty lists of names *)
(*-------------------------------*)
(* A non-empty list of names.
From split_path_string, the following appears to hold:
"/" ~ Name_list("",[""]);
"" ~ Name_list("",[])
*)
type ty_name_list = Name_list of (name * list name) (*o with sexp_of o*)
val ty_name_list_to_list : ty_name_list -> list name
let ty_name_list_to_list (tnl : ty_name_list) : list name =
match tnl with
| Name_list (n, nl) -> n :: nl
end
(* invariant nl not empty *)
val make_ty_name_list : list name -> ty_name_list
let make_ty_name_list (nl : list name) : ty_name_list =
match nl with
| [] -> failwith "invariant name<> [] broken" (* coverage:impossible *)
| (n :: nl') -> Name_list (n, nl')
end
(* let nl_ends_with_slash nl = (last nl = "") *)
val nl_starts_with_slash : ty_name_list -> bool
let nl_starts_with_slash nl = (match nl with
| Name_list ("",[]) -> false
| Name_list (x, _) -> (x = "")
end)
val nl_only_slash : ty_name_list -> bool
let nl_only_slash nl = (match nl with
| Name_list ("", [""]) -> (true) (* coverage:unused *)
| _ -> false (* coverage:unused *)
end)
val name_list_ends_with_slash : list name -> bool
let name_list_ends_with_slash (nl : list name) : bool = (nl <> [""] && last nl = "")
(*-------------------------------*)
(* Predicates for paths seen as *)
(* lists of names *)
(*-------------------------------*)
(* check whether a path is an absolute one by counting the number of slashes stripped *)
let rec is_absolute_path_aux (c : nat) p =
match p with
| ("" :: ns) -> is_absolute_path_aux (c+1) ns (* coverage:unused *)
| _ -> (c > 0) && not (c = 2) (* coverage:unused *)
end
declare termination_argument is_absolute_path_aux = automatic
val is_absolute_path : list name -> bool
let is_absolute_path p = is_absolute_path_aux 0 p (* coverage:unused *)
val is_root_path : list name -> bool
let is_root_path p = ((List.all (fun n -> (n = "")) p) && (List.length p > 0) && (not (List.length p = 2))) (* coverage:unused *)
val is_simple_path : list name -> bool
let is_simple_path p = List.all (fun n -> not ((n = "") || (n = ".") || (n = ".."))) p (* coverage:unused *)
(* check that a path is a simple, absolute path. It is so, if it starts with a _single_ slash and containing no
".", ".." or "//". *)
val is_simple_absolute_path : list name -> bool
let is_simple_absolute_path p =
(match p with
| ("" :: ns) -> is_simple_path ns (* coverage:unused *)
| _ -> false (* coverage:unused *)
end)
(*-------------------------------*)
(* Results of path resolution *)
(* (real paths) *)
(*-------------------------------*)
(* store the result of processing a path in a record, we then have a type encoding either
successful name resolution or an error *)
type ty_realpath_rec 'dir_ref = <|
rp_cwd: 'dir_ref; (* cwd for process *)
rp_nl: ty_name_list; (* the original input for resolution *)
rp_ns: list name; (* the realpath of the entry, this is a simple, absolute path, i.e.
not []; not [""]; ["";""] ~ "/"; first entry is empty; no . and .. entries; no further empty entries (absolute paths) *)
|> (*o with sexp_of o*)
type ty_realpath 'dir_ref 'file_ref = RP_ok of ty_realpath_rec 'dir_ref | RP_err of (error * ty_name_list) (*o with sexp_of o*)
val wf_ty_realpath_rec : forall 'dir_ref. ty_realpath_rec 'dir_ref -> bool
let wf_ty_realpath_rec rp = is_simple_absolute_path rp.rp_ns (* coverage:unused *)
(* check wellformedness of ty_realpath *)
val wf_ty_realpath : forall 'dir_ref 'file_ref. ty_realpath 'dir_ref 'file_ref -> bool
let wf_ty_realpath rp = match rp with
| RP_ok rp' -> wf_ty_realpath_rec rp' (* coverage:unused *)
| RP_err _ -> true (* coverage:unused *)
end
val realpath_proper_subdir : forall 'dir_ref. ty_realpath_rec 'dir_ref -> ty_realpath_rec 'dir_ref -> bool
let realpath_proper_subdir s d =
s.rp_ns <> d.rp_ns
&& (match s.rp_ns with
| ["";""] -> true (* special case for root *)
| _ -> isPrefixOf s.rp_ns d.rp_ns end)
(*-------------------------------*)
(* Resolved names *)
(*-------------------------------*)
type rn_error_extra 'dir_ref 'file_ref = <|
re_cwd: 'dir_ref;
re_nl: maybe ty_name_list; (* the name list that was being resolved, needed for raising errors with respect to trailing slashes *)
re_rn: maybe (res_name 'dir_ref 'file_ref) (* the resolved name (an RN_file) if we ignore trailing slashes *)
|>
and res_name 'dir_ref 'file_ref =
RN_dir of ('dir_ref * ty_realpath_rec 'dir_ref ) (* rp used for subdir check *)
| RN_file of ('dir_ref * name * 'file_ref * ty_realpath_rec 'dir_ref)
| RN_none of ('dir_ref * name * ty_realpath_rec 'dir_ref)
| RN_error of (error * rn_error_extra 'dir_ref 'file_ref)
(*o with sexp_of o*)
(* invariant: if RN_file ns, then not (ns.ends_with_slash2) *)
(* invariant: if RN_error then ns.ends_with_slash2 TT: I don't understand this invariant. Does it really hold?*)
(* invariant: iff RN_error (_, {re_nl=Just nl, re_rn=Just X}) then X = RN_file and nl ends in slash *)
val is_RN_dir : forall 'dir_ref 'file_ref. res_name 'dir_ref 'file_ref -> bool
val is_RN_file : forall 'dir_ref 'file_ref. res_name 'dir_ref 'file_ref -> bool
val is_RN_none : forall 'dir_ref 'file_ref. res_name 'dir_ref 'file_ref -> bool
val is_RN_error : forall 'dir_ref 'file_ref. res_name 'dir_ref 'file_ref -> bool
let is_RN_dir x = (match x with | RN_dir _ -> true | _ -> false end)
let is_RN_file x = (match x with | RN_file _ -> true | _ -> false end)
let is_RN_none x = (match x with | RN_none _ -> true | _ -> false end)
let is_RN_error x = (match x with | RN_error _ -> true | _ -> false end)
(* check wellformedness of res_name *)
val wf_res_name : forall 'dir_ref 'file_ref. res_name 'dir_ref 'file_ref -> bool
let wf_res_name rn = match rn with
RN_dir (_, rp) -> wf_ty_realpath_rec rp (* coverage:unused *)
| RN_file (_, _, _, rp) -> wf_ty_realpath_rec rp && (not (name_list_ends_with_slash rp.rp_ns)) (* coverage:unused *)
| RN_none (_, _, rp) -> wf_ty_realpath_rec rp (* coverage:unused *)
| RN_error (_, <| re_nl=Just nl|>) -> (name_list_ends_with_slash (ty_name_list_to_list nl)) (* TT: and not the root directory ? *) (* coverage:unused *)
| RN_error (_, <| re_nl=Nothing |>) -> true (* coverage:unused *)
end
val name_list_of_res_name : forall 'dir_ref 'file_ref. res_name 'dir_ref 'file_ref -> maybe ty_name_list
let name_list_of_res_name n = (match n with
| RN_dir (_,rp) -> Just rp.rp_nl
| RN_file (_,_,_,rp) -> Just rp.rp_nl
| RN_none (_,_,rp) -> Just rp.rp_nl
| RN_error (_,<|re_nl=nl|>) -> nl
end)
val rn_ends_with_slash : forall 'dir_ref 'file_ref.
res_name 'dir_ref 'file_ref -> bool
let rn_ends_with_slash rn = (
(match name_list_of_res_name rn with
| Nothing -> false (* coverage:impossible -rn_ends_with_slash is never called on an RN_error, so this line is unreachable *)
| Just nl -> (name_list_ends_with_slash (ty_name_list_to_list nl)) end))
(*-------------------------------*)
(* Sysconfig values *)
(*-------------------------------*)
(* see description of sysconf *)
type sysconf_value =
| SC_SYMLOOP_MAX (*o with sexp_of o*)
(* The following values are not used so far. They are commented out in order to keep track of
which values are actually used.
| SC_AIO_LISTIO_MAX
| SC_AIO_MAX
| SC_AIO_PRIO_DELTA_MAX
| SC_ARG_MAX
| SC_ATEXIT_MAX
| SC_BC_BASE_MAX
| SC_BC_DIM_MAX
| SC_BC_SCALE_MAX
| SC_BC_STRING_MAX
| SC_CHILD_MAX
| SC_CLK_TCK
| SC_COLL_WEIGHTS_MAX
| SC_DELAYTIMER_MAX
| SC_EXPR_NEST_MAX
| SC_HOST_NAME_MAX
| SC_IOV_MAX
| SC_LINE_MAX
| SC_LOGIN_NAME_MAX
| SC_NGROUPS_MAX
| SC_GETGR_R_SIZE_MAX
| SC_GETPW_R_SIZE_MAX
| SC_MQ_OPEN_MAX
| SC_MQ_PRIO_MAX
| SC_OPEN_MAX
| SC_ADVISORY_INFO
| SC_BARRIERS
| SC_ASYNCHRONOUS_IO
| SC_CLOCK_SELECTION
| SC_CPUTIME
| SC_FSYNC
| SC_IPV6
| SC_JOB_CONTROL
| SC_MAPPED_FILES
| SC_MEMLOCK
| SC_MEMLOCK_RANGE
| SC_MEMORY_PROTECTION
| SC_MESSAGE_PASSING
| SC_MONOTONIC_CLOCK
| SC_PRIORITIZED_IO
| SC_PRIORITY_SCHEDULING
| SC_RAW_SOCKETS
| SC_READER_WRITER_LOCKS
| SC_REALTIME_SIGNALS
| SC_REGEXP
| SC_SAVED_IDS
| SC_SEMAPHORES
| SC_SHARED_MEMORY_OBJECTS
| SC_SHELL
| SC_SPAWN
| SC_SPIN_LOCKS
| SC_SPORADIC_SERVER
| SC_SS_REPL_MAX
| SC_SYNCHRONIZED_IO
| SC_THREAD_ATTR_STACKADDR
| SC_THREAD_ATTR_STACKSIZE
| SC_THREAD_CPUTIME
| SC_THREAD_PRIO_INHERIT
| SC_THREAD_PRIO_PROTECT
| SC_THREAD_PRIORITY_SCHEDULING
| SC_THREAD_PROCESS_SHARED
| SC_THREAD_ROBUST_PRIO_INHERIT
| SC_THREAD_ROBUST_PRIO_PROTECT
| SC_THREAD_SAFE_FUNCTIONS
| SC_THREAD_SPORADIC_SERVER
| SC_THREADS
| SC_TIMEOUTS
| SC_TIMERS
| SC_TRACE
| SC_TRACE_EVENT_FILTER
| SC_TRACE_EVENT_NAME_MAX
| SC_TRACE_INHERIT
| SC_TRACE_LOG
| SC_TRACE_NAME_MAX
| SC_TRACE_SYS_MAX
| SC_TRACE_USER_EVENT_MAX
| SC_TYPED_MEMORY_OBJECTS
| SC_VERSION
| SC_V7_ILP32_OFF32
| SC_V7_ILP32_OFFBIG
| SC_V7_LP64_OFF64
| SC_V7_LPBIG_OFFBIG
| SC_V6_ILP32_OFF32
| SC_V6_ILP32_OFFBIG
| SC_V6_LP64_OFF64
| SC_V6_LPBIG_OFFBIG
| SC_2_C_BIND
| SC_2_C_DEV
| SC_2_CHAR_TERM
| SC_2_FORT_DEV
| SC_2_FORT_RUN
| SC_2_LOCALEDEF
| SC_2_PBS
| SC_2_PBS_ACCOUNTING
| SC_2_PBS_CHECKPOINT
| SC_2_PBS_LOCATE
| SC_2_PBS_MESSAGE
| SC_2_PBS_TRACK
| SC_2_SW_DEV
| SC_2_UPE
| SC_2_VERSION
| SC_PAGE_SIZE
| SC_PAGESIZE
| SC_THREAD_DESTRUCTOR_ITERATIONS
| SC_THREAD_KEYS_MAX
| SC_THREAD_STACK_MIN
| SC_THREAD_THREADS_MAX
| SC_RE_DUP_MAX
| SC_RTSIG_MAX
| SC_SEM_NSEMS_MAX
| SC_SEM_VALUE_MAX
| SC_SIGQUEUE_MAX
| SC_STREAM_MAX
| SC_TIMER_MAX
| SC_TTY_NAME_MAX
| SC_TZNAME_MAX
| SC_XOPEN_CRYPT
| SC_XOPEN_ENH_I18N
| SC_XOPEN_REALTIME
| SC_XOPEN_REALTIME_THREADS
| SC_XOPEN_SHM
| SC_XOPEN_STREAMS
| SC_XOPEN_UNIX
| SC_XOPEN_UUCP
| SC_XOPEN_VERSION
*)
instance ( SetType sysconf_value )
let setElemCompare = defaultCompare
end
(* Some default values. It is documented for each entry, where the
value comes from. If no other value could be found, I used the one
on my machine running Ubuntu 12.04 64 bit on x86. *)
let sysconf_default = function
SC_SYMLOOP_MAX -> (40 : nat) (* Ubuntu has value unbound, but my filesystem complains after 40,
Posix demands a minimum of POSIX_SYMLOOP_MAX, which seems to be 8. *)
end
(*-------------------------------*)
(* FS-commands *)
(*-------------------------------*)
(* commands that do not mirror the original posix-commands,
but others, which might be useful for e.g. testing *)
type ty_fs_ext_command 'dir_ref 'file_ref =
| FS_PREAD of (res_name 'dir_ref 'file_ref * size_t * off_t)
(* reading and writing is supported by posix only at the OS level, since
file-descriptors are used. This version is a wrapper that uses resolved-names instead.
[FS_PREAD (entry, len, ofs)] tries to read [len] bytes from
entry [entry] at offset [ofs] (from beginning of file).
*)
| FS_PWRITE of (res_name 'dir_ref 'file_ref * ty_bytes * size_t * off_t)
(* This is the write version of [FS_PREAD]. See above. *)
| FS_OPEN_CLOSE of (res_name 'dir_ref 'file_ref * int_open_flags * maybe file_perm) (*o with sexp_of o*)
(* operation at fs level - perform an open with side-effects and then discard any resulting info;
similar to an open followed by an immediate close on the fd at os level *)
(* this interface represents that part of the spec that makes sense
at the fs level (eg without file descriptors) *)
type ty_fs_command 'dir_ref 'file_ref =
FS_LINK of (res_name 'dir_ref 'file_ref * res_name 'dir_ref 'file_ref)
| FS_MKDIR of (res_name 'dir_ref 'file_ref * file_perm)
| FS_READLINK of res_name 'dir_ref 'file_ref
| FS_RENAME of (res_name 'dir_ref 'file_ref * res_name 'dir_ref 'file_ref)
| FS_RMDIR of res_name 'dir_ref 'file_ref
| FS_STAT of res_name 'dir_ref 'file_ref
| FS_LSTAT of res_name 'dir_ref 'file_ref
| FS_SYMLINK of (ty_bytes * res_name 'dir_ref 'file_ref)
| FS_TRUNCATE of (res_name 'dir_ref 'file_ref * off_t)
| FS_UNLINK of res_name 'dir_ref 'file_ref
| FS_CHMOD of (res_name 'dir_ref 'file_ref * file_perm)
| FS_CHOWN of (res_name 'dir_ref 'file_ref * uid * gid)
| FS_EXTENDED_CMD of ty_fs_ext_command 'dir_ref 'file_ref (*o with sexp_of o*)
val res_names_of_ty_fs_command : forall 'dir_ref 'file_ref.
ty_fs_command 'dir_ref 'file_ref -> list (res_name 'dir_ref 'file_ref)
let res_names_of_ty_fs_command cmd = (match cmd with
| FS_LINK (s,d) -> [s;d] (* coverage:unused *)
| FS_MKDIR (s,p) -> [s] (* coverage:unused *)
| FS_READLINK p -> [p] (* coverage:unused *)
| FS_RENAME (s,d) -> [s;d] (* coverage:unused *)
| FS_RMDIR p -> [p] (* coverage:unused *)
| FS_STAT p -> [p] (* coverage:unused *)
| FS_LSTAT p -> [p] (* coverage:unused *)
| FS_SYMLINK (s,d) -> [d] (* coverage:unused *)
| FS_TRUNCATE (p,l) -> [p] (* coverage:unused *)
| FS_UNLINK p -> [p] (* coverage:unused *)
| FS_CHMOD (s, p) -> [s] (* coverage:unused *)
| FS_CHOWN (s, u, g) -> [s] (* coverage:unused *)
| FS_EXTENDED_CMD (FS_OPEN_CLOSE (p,fs,mo)) -> [p] (* coverage:unused *)
| FS_EXTENDED_CMD (FS_PREAD (p,len_,ofs)) -> [p] (* coverage:unused *)
| FS_EXTENDED_CMD (FS_PWRITE (p,bs,len_,ofs)) -> [p] (* coverage:unused *)
end)
(*-------------------------------*)
(* OS commands *)
(*-------------------------------*)
(* an extended version of [ty_os_command]. It does not mirror the original posix-commands,
but slightly extended versions, which might be useful for e.g. testing *)
type ty_os_ext_command =
| OS_OPEN_CLOSE of (cstring * int_open_flags * maybe file_perm) (* see FS_OPEN_CLOSE *)
| OS_ADD_USER_TO_GROUP of (uid * gid)
| OS_DET_PREAD of (ty_fd * size_t * off_t) (* deterministic version of pread *)
| OS_DET_READ of (ty_fd * size_t) (* deterministic version of read *)
| OS_DET_PWRITE of (ty_fd * ty_bytes * size_t * off_t) (* deterministic version of pwrite *)
| OS_DET_WRITE of (ty_fd * ty_bytes * size_t) (*o with sexp o*) (* deterministic version of write *)
val paths_of_ty_os_ext_command : ty_os_ext_command -> list cstring
let paths_of_ty_os_ext_command cmd = (match cmd with
| OS_OPEN_CLOSE (p,fs,mo) -> [p]
| OS_ADD_USER_TO_GROUP (u, g) -> []
| OS_DET_PREAD (fd,sz,ofs) -> []
| OS_DET_PWRITE (fd,bs,sz,ofs) -> []
| OS_DET_WRITE (fd,bs,sz) -> []
| OS_DET_READ (fd,sz) -> []
end)
(* top-level labels, intended to mirror the syscalls, but with functional interface; *)
type ty_os_command =
| OS_CLOSE of ty_fd
| OS_LINK of (cstring * cstring)
| OS_MKDIR of (cstring * file_perm)
| OS_OPEN of (cstring * int_open_flags * maybe file_perm)
| OS_PREAD of (ty_fd * size_t * off_t)
| OS_READ of (ty_fd * size_t)
| OS_READDIR of ty_dh
| OS_OPENDIR of cstring
| OS_REWINDDIR of ty_dh
| OS_CLOSEDIR of ty_dh
| OS_READLINK of cstring
| OS_RENAME of (cstring * cstring)
| OS_RMDIR of cstring
| OS_STAT of cstring
| OS_LSTAT of cstring
| OS_SYMLINK of (cstring * cstring)
| OS_TRUNCATE of (cstring * off_t)
| OS_UNLINK of cstring
| OS_PWRITE of (ty_fd * ty_bytes * size_t * off_t)
| OS_WRITE of (ty_fd * ty_bytes * size_t)
| OS_UMASK of file_perm
| OS_CHMOD of (cstring * file_perm)
| OS_CHOWN of (cstring * uid * gid)
| OS_CHDIR of cstring
| OS_LSEEK of (ty_fd * off_t * int_seek_command)
| OS_EXTENDED_CMD of ty_os_ext_command (*o with sexp o*)
val paths_of_ty_os_command : ty_os_command -> list cstring
let paths_of_ty_os_command cmd = (match cmd with
| OS_CLOSE fd -> []
| OS_LINK (s,d) -> [s;d]
| OS_MKDIR (s,p) -> [s]
| OS_OPEN (p,fs,mo) -> [p]
| OS_PREAD (fd,sz,ofs) -> []
| OS_PWRITE (fd,bs,sz,ofs) -> []
| OS_WRITE (fd,bs,sz) -> []
| OS_READ (fd,sz) -> []
| OS_READDIR dh -> []
| OS_CLOSEDIR dh -> []
| OS_REWINDDIR dh -> []
| OS_OPENDIR p -> [p]
| OS_READLINK p -> [p]
| OS_RENAME (s,d) -> [s;d]
| OS_RMDIR p -> [p]
| OS_STAT p -> [p]
| OS_LSTAT p ->[p]
| OS_SYMLINK (s,d) -> [s;d]
| OS_TRUNCATE (p,l) -> [p]
| OS_UNLINK p -> [p]
| OS_UMASK p -> []
| OS_CHMOD (s, p) -> [s]
| OS_CHOWN (s, u, g) -> [s]
| OS_CHDIR s -> [s]
| OS_LSEEK (fd,ofs,c) -> []
| OS_EXTENDED_CMD cmd' -> paths_of_ty_os_ext_command cmd'
end)
(*-------------------------------*)
(* Architecture *)
(*-------------------------------*)
(* a representation of the available architectures *)
type ty_arch = ARCH_LINUX | ARCH_POSIX | ARCH_MAC_OS_X (*o with sexp_of o*)
instance (Eq ty_arch)
let (=) = unsafe_structural_equality
let (<>) = unsafe_structural_inequality
end
(* the spec is parameterized by various traits, combined to form an "architecture" *)
type architecture = <|
arch_abs_path_slash_slash: bool; (* whether an absolute path can start with a double slash - POSIX has maybe implementation defined *)
arch_linux_non_posix: bool; (* Linux specific behaviour that is not POSIX compliant *)
arch_link_directories: bool; (* whether the implementation allows links on dirs; not supported in this spec *)
arch_open_flags_of_int: int_open_flags -> finset open_flag (*o sexp_opaque o*);
arch_int_of_open_flags: finset open_flag -> int_open_flags (*o sexp_opaque o*);
arch_seek_command_of_int : int_seek_command -> maybe seek_command (*o sexp_opaque o*);
arch_int_of_seek_command : seek_command -> int_seek_command (*o sexp_opaque o*);
arch_allows_dir_read : bool; (* allow reading from a directory? If set to false, reading a directory needs readdir command instead of read. *)
arch_group_from_parent_dir: bool; (* Should new directories inherit the group of their parent dir? If set false, they use
the effective group id of the process instead. *)
arch_allows_removing_from_protected_dir_if_writeable : bool (* Allow deleting files and directories from protected directories, if the file or dir
is writeable? see posix/dir_protect.md *)
|>(*o with sexp_of o*)
type ignore_j5f (* to force trailing comment above, see lem issue #174 *)
#ifdef aspect_perms
(*-------------------------------*)
(* Permission operations *)
(*-------------------------------*)
(* Operations concerned with permissions. This includes ownership of files and directories as well as
and group membership operations. *)
type perm_ops 'dir_ref 'file_ref 'jimpl = <|
pops_set_perm_file : 'jimpl -> file_perm -> 'file_ref -> 'jimpl;
pops_set_perm_dir : 'jimpl -> file_perm -> 'dir_ref -> 'jimpl;
pops_chown_file: 'jimpl -> (uid * gid) -> 'file_ref -> 'jimpl;
pops_chown_dir: 'jimpl -> (uid * gid) -> 'dir_ref -> 'jimpl;
pops_uid_is_superuser : 'jimpl -> uid -> bool
|> (* sexp_opaque with sexp *)
(* a dummy implementation of perm_ops with no-ops everywhere *)
val perm_ops_noops : forall 'dir_ref 'file_ref 'impl. unit -> perm_ops 'dir_ref 'file_ref 'impl
let perm_ops_noops () = <| (* coverage:unused *)
pops_set_perm_file = (fun s0 _ _ -> s0); (* coverage:unused *)
pops_set_perm_dir = (fun s0 _ _ -> s0); (* coverage:unused *)
pops_chown_file = (fun s0 _ _ -> s0); (* coverage:unused *)
pops_chown_dir = (fun s0 _ _ -> s0); (* coverage:unused *)
pops_uid_is_superuser = (fun _ uid -> uid = root_uid) (* coverage:unused *)
|>
(*-------------------------------*)
(* Checking permissions *)
(*-------------------------------*)
type check_permissions 'dir_ref 'file_ref 'jimpl = <|
(* get the umask and default user and group of new files *)
cp_get_umask : 'jimpl -> file_perm;
cp_get_euid : unit -> uid;
cp_get_egid : unit -> gid;
(* has the current process certain permissions on a directory ? *)
cp_has_dir_search_permission : 'jimpl -> 'dir_ref -> bool;
cp_has_dir_read_permission : 'jimpl -> 'dir_ref -> bool;
cp_has_dir_write_permission : 'jimpl -> 'dir_ref -> bool;
cp_has_dir_chmod_permission : 'jimpl -> 'dir_ref -> bool;
cp_has_dir_chown_permission : 'jimpl -> 'dir_ref -> bool;
(* has the current process certain permissions on a file ? *)
cp_has_file_execute_permission : 'jimpl -> 'file_ref -> bool;
cp_has_file_read_permission : 'jimpl -> 'file_ref -> bool;
cp_has_file_write_permission : 'jimpl -> 'file_ref -> bool;
cp_has_file_chmod_permission : 'jimpl -> 'file_ref -> bool;
cp_has_file_chown_permission : 'jimpl -> 'file_ref -> bool;
(* special stuff ? *)
cp_has_dir_link_create_privilege : 'jimpl -> 'dir_ref -> bool; (* posix/link.md EPERM:1 *)
(* can the dir or file be deleted, if it's parent directory has the restricted deletion flag set?
Depending on the architecture this access is given for files with write permission. *)
cp_has_dir_restricted_delete_privilege : (* allow for files with write perm? *) bool ->
'jimpl -> (* parent dir *) 'dir_ref -> 'dir_ref -> bool;
cp_has_file_restricted_delete_privilege : bool -> 'jimpl -> (* parent dir *) 'dir_ref -> 'file_ref -> bool;
|>
#endif
(*-------------------------------*)
(* Observing directories *)
(*-------------------------------*)
(* For operations like readdir it is important to keep track of
the changes to a directory between different calls. For this
one can register for observing a directory via
[fops_observe_dir_register]. This returns a handle, which can be used
via [fops_observe_dir] to get the changes since the last call.
Finally [fops_observe_dir_unregister] is used to clear the handle.
These functions are part of the [fs_ops] record defined below.
Here only a few auxiliary datatypes are defined.*)
type ty_od_handle 'dir_ref = OD_handle of (nat * 'dir_ref) (*o with sexp_of o*) (* todo: perhaps make it a type variable *)
type ty_od_entry = OD_removed of name
| OD_added of name (*o with sexp_of o*)
(*-------------------------------*)
(* Filesystem operations *)
(*-------------------------------*)
type fs_ops 'dir_ref 'file_ref 'jimpl = <|
fops_get_init_state: unit -> 'jimpl;
fops_get_parent: 'jimpl -> 'dir_ref -> maybe ('dir_ref * name); (* if root, parent is none; possibly disconnected dirs can also have no parent *)
fops_get_root: 'jimpl -> maybe 'dir_ref;
fops_dest_dir_ref: 'jimpl -> 'dir_ref -> inode;
fops_dest_file_ref: 'jimpl -> 'file_ref -> inode;
fops_file_ref_eq : 'jimpl -> 'file_ref -> 'file_ref -> bool; (* equality check on file-refs *)
fops_dir_ref_eq : 'jimpl -> 'dir_ref -> 'dir_ref -> bool; (* equality check on dir-refs *)
fops_link_file: 'jimpl -> 'file_ref -> 'dir_ref -> name -> 'jimpl;
fops_unlink: 'jimpl -> 'dir_ref -> name -> 'jimpl;
fops_mkdir: 'jimpl -> 'dir_ref -> name -> ('jimpl * 'dir_ref);
fops_mvfile: 'jimpl -> 'dir_ref -> name -> 'dir_ref -> name -> 'jimpl;
fops_mvdir: 'jimpl -> 'dir_ref -> name -> 'dir_ref -> name -> 'jimpl;
fops_read: 'jimpl -> 'file_ref -> ('jimpl * ret_value); (* FIXME return value should be bytes? *)
fops_readdir: 'jimpl -> 'dir_ref -> ('jimpl * list name); (* don't return . and .. entries *)
fops_resolve: 'jimpl -> 'dir_ref -> name -> maybe (entry 'dir_ref 'file_ref); (* resolves normal entries; use get_parent for .. *)
fops_lookup_sysconf: 'jimpl -> sysconf_value -> nat;
fops_write: 'jimpl -> 'file_ref -> ty_bytes -> 'jimpl;
fops_mkfile: 'jimpl -> 'dir_ref -> name -> 'jimpl * 'file_ref; (* FIXME prefer this to touch *)
fops_readlink: 'jimpl -> 'file_ref -> ty_bytes; (* internal *)
fops_symlink: 'jimpl -> 'dir_ref -> name -> ty_bytes -> 'jimpl;
fops_stat_file: 'jimpl -> 'file_ref -> ty_stats; (* this is internal - doesn't expect to update times etc *)
fops_stat_dir: 'jimpl -> 'dir_ref -> ty_stats; (* this is internal - doesn't expect to update times etc *)
fops_lstat: 'jimpl -> 'file_ref -> ty_stats; (* this is internal -doesn't expect to update times etc *)
fops_observe_dir_register : 'jimpl -> 'dir_ref -> ('jimpl * ty_od_handle 'dir_ref);
fops_observe_dir : 'jimpl -> ty_od_handle 'dir_ref -> ('jimpl * list ty_od_entry);
fops_observe_dir_unregister : 'jimpl -> ty_od_handle 'dir_ref -> 'jimpl;
|>
(*-------------------------------*)
(* Environments *)
(*-------------------------------*)
type environment 'dir_ref 'file_ref 'jimpl = <|
env_ops: fs_ops 'dir_ref 'file_ref 'jimpl (*o sexp_opaque o*);
env_arch: ty_arch;
#ifdef aspect_perms
env_prms : check_permissions 'dir_ref 'file_ref 'jimpl (*o sexp_opaque o*);
env_perm_ops: perm_ops 'dir_ref 'file_ref 'jimpl (*o sexp_opaque o*);
#endif
|> (*o with sexp_of o*)
(*-------------------------------*)
(* Process ids *)
(*-------------------------------*)
type ty_pid = Pid of nat (*o with sexp o*)
let ty_pid_compare (Pid n0) (Pid n1) = compare n0 n1
instance ( SetType ty_pid )
let setElemCompare = ty_pid_compare
end
instance (Eq ty_pid)
let (=) = unsafe_structural_equality
let (<>) = unsafe_structural_inequality
end
val dest_PID : ty_pid -> nat
let dest_PID x = (match x with Pid n -> n end) (* coverage:unused *)
(*-------------------------------*)
(* OS_labels *)
(*-------------------------------*)
(* a process can only make a single call into OS (so, no threads); process is blocked until return *)
type os_label =
OS_CALL of (ty_pid * ty_os_command)
| OS_RETURN of (ty_pid * error_or_value ret_value)
| OS_CREATE of (ty_pid * uid * gid)
| OS_DESTROY of ty_pid
| OS_TAU (*o with sexp o*)
(*-------------------------------*)
(* file descriptor ids *)
(*-------------------------------*)
(* open file descriptions, per host *)
type ty_fid = FID of nat (*o with sexp_of o*)
let ty_fid_compare (FID n0) (FID n1) = compare n0 n1
instance ( SetType ty_fid )
let setElemCompare = ty_fid_compare
end
val dest_FID : ty_fid -> nat
let dest_FID x = (match x with FID n -> n end) (* coverage:unused *)
(*-------------------------------*)
(* directory handle state *)
(*-------------------------------*)
type dh_state 'dir_ref = <|
dhs_dir_ref: 'dir_ref;
dhs_observe_handle : ty_od_handle 'dir_ref;
dhs_must_report : list name;
(* the entries of the directory that still need to be reported by readdir. This list will never contain duplicates. *)
dhs_may_report : list name; (* the entries of the directory that may, but does not need to be still reported.
This list might contain duplicates, which indicates that these entries might be reported twice. *)
|> (*o with sexp_of o*)
(*-------------------------------*)
(* file descriptor state *)
(*-------------------------------*)
type fd_state = <|
fds_fid: ty_fid;
fds_FD_CLOEXEC: bool; (* FIXME how to test? *)
|> (*o with sexp_of o*)
(*-------------------------------*)
(* file identifier states *)
(*-------------------------------*)
type fid_open_closed_state = FID_OPEN | FID_CLOSED (*o with sexp_of o*)
type fid_state 'dir_ref 'file_ref = <|
fids_offset: nat; (* cannot be negative *)
fids_entry: entry 'dir_ref 'file_ref;
fids_oflags: finset open_flag (*o sexp_opaque o*); (* flags that were provided on creation *)
fids_open_or_closed: fid_open_closed_state;
|> (*o with sexp_of o*)
(*-------------------------------*)
(* per process states *)
(*-------------------------------*)
type ty_pps_pid_run_state = RUNNING | BLOCKED_CALL of ty_os_command | PENDING_RETURN of (error_or_value ret_value) (*o with sexp_of o*)
(*o
let sexp_of_fmap a b x = x |> (fmap_bindings
(Lem_map.instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict)
instance_Basic_classes_SetType_var_dict
instance_Basic_classes_SetType_var_dict)
|> sexp_of_list (sexp_of_pair a b)
o*)
type per_process_state 'dir_ref = <|
pps_cwd: 'dir_ref;
pps_fd_table: fmap ty_fd (fd_state) (*o sexp_opaque o*);
pps_dh_table: fmap ty_dh (dh_state 'dir_ref) (*o sexp_opaque o*);
pps_pid_run_state : ty_pps_pid_run_state;
pps_file_creation_mask : file_perm;
pps_effective_uid : uid;
pps_real_uid : uid;
pps_saved_uid : uid;
pps_effective_gid : gid;
pps_real_gid : gid;
pps_saved_gid : gid;
|> (*o with sexp_of o*)
(*-------------------------------*)
(* operating system states *)
(*-------------------------------*)
type ty_os_state 'dir_ref 'file_ref 'jimpl = <|
oss_pid_table: fmap ty_pid (per_process_state 'dir_ref);
oss_fid_table: fmap ty_fid (fid_state 'dir_ref 'file_ref);
oss_group_table: fmap gid (finset uid) (*o sexp_opaque o*);
oss_fs_state: 'jimpl;
oss_env: environment 'dir_ref 'file_ref 'jimpl
|> (*o with sexp_of o*)
val os_state_to_fs_state : forall 'dir_ref 'file_ref 'jimpl. ty_os_state 'dir_ref 'file_ref 'jimpl -> 'jimpl
let os_state_to_fs_state s0 = s0.oss_fs_state
let os_state_to_env s0 = s0.oss_env
(*-------------------------------*)
(* Monad states *)
(*-------------------------------*)
(* We model the non-deterministic behaviour of the specification
explicitly. A normal monad state consists of a file-system state
with either a posix defined error or with a return
value. However, we might also have special states. Special states
from the specification are states where the specification is
vague (explicitly for various reasons) and we therefore just have
to stop and say that we don't know what happens. Another reason
is that we just did not get around (yet) modeling some less common
parts of the specification. *)
type monad_special_state = Impossible | Implementation_defined | Unspecified | Undefined | FIXME (*o with sexp o*)
(* Since we also support non-determinism, a monad state is either a (finite) set of normal states or of special states. *)
type monad_state 'impl 'ja =
Normal_state of ('impl * 'ja)
| Error_state of ('impl * error)
| Special_state of (monad_special_state * string)
val is_Normal_state : forall 'impl 'a. monad_state 'impl 'a -> bool
let is_Normal_state st = match st with
| Normal_state _ -> true
| _ -> false
end
val is_Error_state : forall 'impl 'a. monad_state 'impl 'a -> bool
let is_Error_state st = match st with
| Error_state _ -> true (* coverage:unused *)
| _ -> false (* coverage:unused *)
end
val is_Error_state_err : forall 'impl 'a. error -> monad_state 'impl 'a -> bool
let is_Error_state_err e st = match st with
| Error_state (_, e') -> (e = e') (* coverage:unused *)
| _ -> false (* coverage:unused *)
end
val is_Special_state : forall 'impl 'a. monad_state 'impl 'a -> bool
let is_Special_state st = match st with
| Special_state _ -> true (* coverage:unused *)
| _ -> false (* coverage:unused *)
end
val is_Impossible_state : forall 'impl 'a. monad_state 'impl 'a -> bool
let is_Impossible_state st = match st with
| Special_state (Impossible, _) -> true (* coverage:unused *)
| _ -> false (* coverage:unused *)
end
val dest_Normal_state : forall 'impl 'a. monad_state 'impl 'a -> ('impl * 'a)
val dest_Error_state : forall 'impl 'a. monad_state 'impl 'a -> ('impl * error)
val dest_Special_state : forall 'impl 'a. monad_state 'impl 'a -> (monad_special_state * string)
let dest_Normal_state (Normal_state sx) = sx (* coverage:unused *)
let dest_Error_state (Error_state se) = se (* coverage:unused *)
let dest_Special_state (Special_state sm) = sm (* coverage:unused *)
(* We can't compare all 'impl. So let's use the following heuristic. If it returns true,
two states are equal, otherwise, we don't know. *)
val monad_state_shallow_eq : forall 'impl 'a. Eq 'a => monad_state 'impl 'a -> monad_state 'impl 'a -> bool
let monad_state_shallow_eq st1 st2 = match (st1, st2) with
| (Normal_state (s1, v1), Normal_state (s2, v2)) -> (* coverage:impossible *)
(v1 = v2) && (shallow_equality s1 s2) (* coverage:impossible -monad_state_shallow_eq is used only on partitions of states that are not normal *)
| (Error_state (s1, e1), Error_state (s2, e2)) -> (e1 = e2) && (shallow_equality s1 s2)
| (Special_state (ss1, m1), Special_state (ss2, m2)) -> (ss1 = ss2) && (m1 = m2) (* coverage:linux:irrelevant *)
| _ -> false
end
(*-------------------------------*)
(* OS states *)
(*-------------------------------*)
type os_state_or_special 'dir_ref 'file_ref 'impl =
| OS_normal of (ty_os_state 'dir_ref 'file_ref 'impl)
| OS_special of (monad_special_state * string) (*o with sexp_of o*)
let is_OS_normal s = (match s with | OS_normal s -> true | _ -> false end) (* coverage:unused *)
let is_OS_special s = (match s with | OS_special s -> true | _ -> false end) (* coverage:unused *)
let dest_OS_normal s = (match s with | OS_normal s -> s | _ -> failwith "dest_OS_normal" end) (* coverage:unused *)
let dest_OS_special s = (match s with | OS_special s -> s | _ -> failwith "dest_OS_special" end) (* coverage:unused *)
end(* Fs_types *)
(******************************************************************************)
(* Fs_arch *)
(* *)
(* Architecture-specific definitions *)
(******************************************************************************)
module Fs_arch = struct
open Fs_types
(*-------------------------------*)
(* Encoding of open-flags *)
(*-------------------------------*)
(* taken from Linux/include/uapi/asm-generic/fcntl.h http://lxr.free-electrons.com/source/include/uapi/asm-generic/fcntl.h *)
val linux_int_of_open_flag : open_flag -> maybe int_open_flags
let linux_int_of_open_flag = (fun f ->
match f with
(* ACCMODE 00000003 *)
| O_EXEC -> Nothing (* coverage:mac_os_x:posix:irrelevant *)
| O_RDONLY -> Nothing (* note that this is non-posix behaviour - O_RDONLY should be represented by a bit, rather than the absence of other bits *) (* coverage:mac_os_x:posix:irrelevant *)
| O_WRONLY -> (Just 0O00000001) (* coverage:mac_os_x:posix:irrelevant *)
| O_RDWR -> (Just 0O00000002) (* coverage:mac_os_x:posix:irrelevant *)
| O_SEARCH -> Nothing (* coverage:mac_os_x:posix:irrelevant *)
| O_CREAT -> (Just 0O00000100) (* coverage:mac_os_x:posix:irrelevant *)
| O_EXCL -> (Just 0O00000200) (* coverage:mac_os_x:posix:irrelevant *)
| O_NOCTTY -> (Just 0O00000400) (* coverage:mac_os_x:posix:irrelevant *)
| O_TRUNC -> (Just 0O00001000) (* coverage:mac_os_x:posix:irrelevant *)
| O_APPEND -> (Just 0O00002000) (* coverage:mac_os_x:posix:irrelevant *)
| O_NONBLOCK -> (Just 0O00004000) (* coverage:mac_os_x:posix:irrelevant *)
| O_RSYNC -> Nothing (* coverage:mac_os_x:posix:irrelevant *)
| O_SYNC -> Nothing (* coverage:mac_os_x:posix:irrelevant *)
| O_DSYNC -> (Just 0O00010000) (* coverage:mac_os_x:posix:irrelevant *)
(* | FASYNC 0o00020000 *)
(* | O_DIRECT 0o00040000 *)
(* | O_LARGEFILE 00100000 *)
| O_DIRECTORY -> (Just 0O00200000) (* coverage:mac_os_x:posix:irrelevant *)
| O_NOFOLLOW -> (Just 0O00400000) (* coverage:mac_os_x:posix:irrelevant *)
(* | O_NOATIME 01000000 *)
| O_CLOEXEC -> (Just 0O02000000) (* coverage:mac_os_x:posix:irrelevant *)
| O_TTY_INIT -> Nothing (* coverage:mac_os_x:posix:irrelevant *)
end)
(* taken from Xcode/.../usr/include/sys/fcntl.h *)
val mac_int_of_open_flag : open_flag -> maybe int_open_flags
let mac_int_of_open_flag = (fun f ->
match f with
(* ACCMODE 00000003 *)
| O_EXEC -> Nothing
| O_RDONLY -> Nothing (* actually defined as 0x0000 on mac, but this is not useful when dealing with bits where a 1 represents the presence of a flag *)
| O_WRONLY -> (Just 0X0001)
| O_RDWR -> (Just 0X0002)
| O_SEARCH -> Nothing
| O_NONBLOCK -> (Just 0X0004)
| O_APPEND -> (Just 0X0008)
| O_CREAT -> (Just 0X0200)
| O_EXCL -> (Just 0X0800)
| O_NOCTTY -> (Just 0X20000)
| O_TRUNC -> (Just 0X0400)
| O_RSYNC -> Nothing
| O_SYNC -> (Just 0X0080)
| O_DSYNC -> (Just 0X400000)
(* | FASYNC 0o00020000 *)
(* | O_DIRECT 0o00040000 *)
(* | O_LARGEFILE 00100000 *)
| O_DIRECTORY -> (Just 0X100000)
| O_NOFOLLOW -> (Just 0X0100)
(* | O_NOATIME 01000000 *)
| O_CLOEXEC -> (Just 0X1000000)
| O_TTY_INIT -> Nothing
end)
(* A dummy one that encodes (in contrast to Linux) really everything *)
val posix_int_of_open_flag : open_flag -> maybe int_open_flags
let posix_int_of_open_flag = (fun f ->
match f with
(* ACCMODE 00000003 *)
| O_EXEC -> (Just 0O000000001) (* coverage:linux:irrelevant *)
| O_RDONLY -> (Just 0O000000002) (* coverage:linux:irrelevant *)
| O_WRONLY -> (Just 0O000000004) (* coverage:linux:irrelevant *)
| O_RDWR -> (Just 0O000000010) (* coverage:linux:irrelevant *)
| O_SEARCH -> (Just 0O000000020) (* coverage:linux:irrelevant *)
| O_CREAT -> (Just 0O000000040) (* coverage:linux:irrelevant *)
| O_EXCL -> (Just 0O000000100) (* coverage:linux:irrelevant *)
| O_NOCTTY -> (Just 0O000000200) (* coverage:linux:irrelevant *)
| O_TRUNC -> (Just 0O000000400) (* coverage:linux:irrelevant *)
| O_APPEND -> (Just 0O000001000) (* coverage:linux:irrelevant *)
| O_NONBLOCK -> (Just 0O000002000) (* coverage:linux:irrelevant *)
| O_RSYNC -> (Just 0O000004000) (* coverage:linux:irrelevant *)
| O_SYNC -> (Just 0O000010000) (* coverage:linux:irrelevant *)
| O_DSYNC -> (Just 0O000020000) (* coverage:linux:irrelevant *)
| O_DIRECTORY -> (Just 0O000040000) (* coverage:linux:irrelevant *)
| O_NOFOLLOW -> (Just 0O000100000) (* coverage:linux:irrelevant *)
| O_CLOEXEC -> (Just 0O000200000) (* coverage:linux:irrelevant *)
| O_TTY_INIT -> (Just 0O000400000) end) (* coverage:linux:irrelevant *)
(* convert an oflag int argument to a set of flags *)
val gen_arch_open_flags_of_int : (open_flag -> maybe int_open_flags) -> int_open_flags -> finset open_flag
let gen_arch_open_flags_of_int int_of_open_flag = (fun oflag ->
let is_flag_in_oflag flag = (
let i = int_of_open_flag flag in
(match i with
| Nothing -> false (* coverage:mac_os_x:posix:irrelevant *)
| Just i -> (i land oflag) <> 0
end)
) in
let fs = finset_filter is_flag_in_oflag open_flags in
(* if no access mode, then the access mode is O_RDONLY! this arises because Linux (and Mac) defines O_RDONLY=0 *)
if finset_all (fun flag -> not (finset_mem flag fs)) access_mode_flags then
finset_insert O_RDONLY fs
else
fs)
val linux_arch_open_flags_of_int : int_open_flags -> finset open_flag
let linux_arch_open_flags_of_int = gen_arch_open_flags_of_int linux_int_of_open_flag
val mac_arch_open_flags_of_int : int_open_flags -> finset open_flag
let mac_arch_open_flags_of_int = gen_arch_open_flags_of_int mac_int_of_open_flag
val posix_arch_open_flags_of_int : int_open_flags -> finset open_flag
let posix_arch_open_flags_of_int = gen_arch_open_flags_of_int posix_int_of_open_flag
val gen_arch_int_of_open_flags : (open_flag -> maybe int_open_flags) -> finset open_flag -> int_open_flags
let gen_arch_int_of_open_flags int_of_open_flag = (fun fs ->
let flags = list_from_finset fs in
let sum = List.foldl (fun sum f -> match int_of_open_flag f with
| Nothing -> sum (* coverage:mac_os_x:posix:irrelevant *)
| Just i -> sum lor i
end) 0 flags in
sum)
val linux_arch_int_of_open_flags : finset open_flag -> int_open_flags
let linux_arch_int_of_open_flags = gen_arch_int_of_open_flags linux_int_of_open_flag
val mac_arch_int_of_open_flags : finset open_flag -> int_open_flags
let mac_arch_int_of_open_flags = gen_arch_int_of_open_flags mac_int_of_open_flag
val posix_arch_int_of_open_flags : finset open_flag -> int_open_flags
let posix_arch_int_of_open_flags = gen_arch_int_of_open_flags posix_int_of_open_flag
(*-------------------------------*)
(* Encoding of seek-commands *)
(*-------------------------------*)
(* values copied from linux stdio.h *)
val linux_arch_int_of_seek_command : seek_command -> int_seek_command
let linux_arch_int_of_seek_command c = (match c with
| SEEK_SET -> 0 (* coverage:mac_os_x:posix:irrelevant *)
| SEEK_CUR -> 1 (* coverage:mac_os_x:posix:irrelevant *)
| SEEK_END -> 2 (* coverage:mac_os_x:posix:irrelevant *)
| SEEK_DATA -> 3 (* coverage:mac_os_x:posix:irrelevant *)
| SEEK_HOLE -> 4 (* coverage:mac_os_x:posix:irrelevant *)
end)
val posix_arch_int_of_seek_command : seek_command -> int_seek_command
let posix_arch_int_of_seek_command c = linux_arch_int_of_seek_command c (*coverage:linux:irrelevant*)
val linux_arch_seek_command_of_int : int_seek_command -> maybe seek_command
let linux_arch_seek_command_of_int i = (
if i = 0 (* coverage:mac_os_x:posix:irrelevant *)
then Just SEEK_SET (* coverage:mac_os_x:posix:irrelevant *)
else
if i = 1 (* coverage:mac_os_x:posix:irrelevant *)
then Just SEEK_CUR (* coverage:mac_os_x:posix:irrelevant *)
else
if i = 2 (* coverage:mac_os_x:posix:irrelevant *)
then Just SEEK_END (* coverage:mac_os_x:posix:irrelevant *)
else
if i = 3 (* coverage:mac_os_x:posix:irrelevant *)
then Just SEEK_DATA (* coverage:unused *)
else
if i = 4 (* coverage:mac_os_x:posix:irrelevant *)
then Just SEEK_HOLE (* coverage:unused *)
else Nothing (* coverage:mac_os_x:posix:irrelevant *)
)
val posix_arch_seek_command_of_int : int_seek_command -> maybe seek_command
let posix_arch_seek_command_of_int i = (
if i = 0 then Just SEEK_SET else (* coverage:linux:irrelevant *)
if i = 1 then Just SEEK_CUR else (* coverage:linux:irrelevant *)
if i = 2 then Just SEEK_END else (* coverage:linux:irrelevant *)
Nothing (*coverage:linux:irrelevant*)
)
(*-------------------------------*)
(* Architecture records *)
(*-------------------------------*)
val linux_arch : architecture
let linux_arch = <|
arch_abs_path_slash_slash = true;
arch_linux_non_posix = true;
arch_link_directories = false; (* this is not supported *)
arch_open_flags_of_int = linux_arch_open_flags_of_int;
arch_int_of_open_flags = linux_arch_int_of_open_flags;
arch_seek_command_of_int = linux_arch_seek_command_of_int;
arch_int_of_seek_command = linux_arch_int_of_seek_command;
arch_allows_dir_read = false;
arch_group_from_parent_dir = false; (* use effective gid of process for new dirs *)
arch_allows_removing_from_protected_dir_if_writeable = false;
|>
(* for testing, we don't want to fail every time we hit a POSIX
"implementation defined" feature; the following architecture is
POSIX, but with implementation defined features selected so that the
behaviour is sensible *)
val posix_test_arch : architecture
let posix_test_arch = <|
arch_abs_path_slash_slash = true;
arch_linux_non_posix = false;
arch_link_directories = false; (* for testing? we should also test the spec if this is allowed *)
arch_open_flags_of_int = posix_arch_open_flags_of_int;
arch_int_of_open_flags = posix_arch_int_of_open_flags;
arch_seek_command_of_int = posix_arch_seek_command_of_int;
arch_int_of_seek_command = posix_arch_int_of_seek_command;
arch_allows_dir_read = false;
arch_group_from_parent_dir = false; (* for testing perhaps try true as well *)
arch_allows_removing_from_protected_dir_if_writeable = false;
|>
(* mac os x arch is like posix, but allows dir links *)
val mac_os_x_test_arch : architecture
let mac_os_x_test_arch = <|
arch_abs_path_slash_slash = true;
arch_linux_non_posix = false;
arch_link_directories = false; (* FIXME not observed on Mac OS X tests yet? reverting to false for the time being *)
arch_open_flags_of_int = mac_arch_open_flags_of_int;
arch_int_of_open_flags = mac_arch_int_of_open_flags;
arch_seek_command_of_int = posix_arch_seek_command_of_int;
arch_int_of_seek_command = posix_arch_int_of_seek_command;
arch_allows_dir_read = false;
arch_group_from_parent_dir = false; (* for testing perhaps try true as well *)
arch_allows_removing_from_protected_dir_if_writeable = false;
|>
let architecture_of_ty_arch a = (match a with
| ARCH_LINUX -> linux_arch (* coverage:mac_os_x:irrelevant *)
| ARCH_POSIX -> posix_test_arch (* coverage:linux:mac_os_x:irrelevant *)
| ARCH_MAC_OS_X -> mac_os_x_test_arch end) (* coverage:linux:posix:irrelevant *)
val default_arch : ty_arch
let default_arch = ARCH_POSIX
(*-------------------------------*)
(* auxiliary functions to access *)
(* architecture records *)
(*-------------------------------*)
val is_linux_arch : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> bool
let is_linux_arch env = (env.env_arch = ARCH_LINUX)
val is_mac_os_x_arch: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> bool
let is_mac_os_x_arch env = (env.env_arch = ARCH_MAC_OS_X)
val arch_allows_dir_links : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> bool
let arch_allows_dir_links env = (
(architecture_of_ty_arch (env.env_arch)).arch_link_directories) (* coverage:unused *)
end
#ifdef aspect_perms
(******************************************************************************)
(* Fs_permissions *)
(* *)
(* operations concerned with file permissions *)
(******************************************************************************)
module Fs_permissions = struct
open Fs_types
(* ------------------------------------ *)
(* constants for file permissions *)
(* ------------------------------------ *)
let S_IRWXU : file_perm = File_perm 0O0700 (* Read, write, execute/search by owner. *)
let S_IRUSR : file_perm = File_perm 0O0400 (* Read permission, owner. *)
let S_IWUSR : file_perm = File_perm 0O0200 (* Write permission, owner. *)
let S_IXUSR : file_perm = File_perm 0O0100 (* Execute/search permission, owner. *)
let S_IRWXG : file_perm = File_perm 0O0070 (* Read, write, execute/search by group. *)
let S_IRGRP : file_perm = File_perm 0O0040 (* Read permission, group. *)
let S_IWGRP : file_perm = File_perm 0O0020 (* Write permission, group. *)
let S_IXGRP : file_perm = File_perm 0O0010 (* Execute/search permission, group. *)
let S_IRWXO : file_perm = File_perm 0O0007 (* Read, write, execute/search by others. *)
let S_IROTH : file_perm = File_perm 0O0004 (* Read permission, others. *)
let S_IWOTH : file_perm = File_perm 0O0002 (* Write permission, others. *)
let S_IXOTH : file_perm = File_perm 0O0001 (* Execute/search permission, others. *)
let S_ISUID : file_perm = File_perm 0O4000 (* Set-user-ID on execution. *)
let S_ISGID : file_perm = File_perm 0O2000 (* Set-group-ID on execution. *)
let S_ISVTX : file_perm = File_perm 0O1000 (* On directories, restricted deletion flag *)
(* ------------------------------------ *)
(* some operations on file permissions *)
(* ------------------------------------ *)
val combine_file_perms : list file_perm -> file_perm
let combine_file_perms pl = File_perm (List.foldl (fun i p -> (i lor (dest_file_perm p))) 0 pl) (* coverage:unused *)
(* the Posix defined file permissions only use the lower 12 bits. 3 * 3 bits are used for
read, write and search/execute permissions for owner, group and others + 3 bits for
special permissions. However, some implementations may use further bits. Some functions
need to be able to check, whether such permissions are present. *)
val contains_implementation_specific_file_perms : file_perm -> bool
let contains_implementation_specific_file_perms p = not ((dest_file_perm p) land (lnot 0O07777) = 0)
(* [set_file_perms org_perm new_perm] updates the permission [org_perm] to now contain also
the permissions [new_perm] *)
val set_file_perms : file_perm -> file_perm -> file_perm
let set_file_perms org_perm new_perm = File_perm (dest_file_perm org_perm lor dest_file_perm new_perm) (* coverage:unused *)
(* [unset_file_perms org_perm new_perm] updates the permission [org_perm] to remove the permissions [new_perm] *)
val unset_file_perms : file_perm -> file_perm -> file_perm
let unset_file_perms org_perm new_perm = File_perm (dest_file_perm org_perm land (lnot (dest_file_perm new_perm)))
(* [check_file_perms perm check_perm] checks whether the permission [perm] contains permissions [check_perm] *)
val check_file_perms : file_perm -> file_perm -> bool
let check_file_perms perm check_perm = ((dest_file_perm perm land dest_file_perm check_perm) = dest_file_perm check_perm)
(* --------------------------------------------- *)
(* check whether a user has certain permissions *)
(* --------------------------------------------- *)
(* extract the relevant permission from a stat result for a given uid *)
type permission_type =
Perm_read | Perm_write | Perm_execute_search
val permission_type_to_user_perm : permission_type -> file_perm
let permission_type_to_user_perm = function
| Perm_read -> S_IRUSR
| Perm_write -> S_IWUSR
| Perm_execute_search -> S_IXUSR
end
val permission_type_to_group_perm : permission_type -> file_perm
let permission_type_to_group_perm = function
| Perm_read -> S_IRGRP
| Perm_write -> S_IWGRP
| Perm_execute_search -> S_IXGRP
end
val permission_type_to_other_perm : permission_type -> file_perm
let permission_type_to_other_perm = function
| Perm_read -> S_IROTH
| Perm_write -> S_IWOTH
| Perm_execute_search -> S_IXOTH
end
(* [uid_check_permission ops s0 uid pt stat] checks whether
in the state [s0] the user [uid] has permission of type [pt] on a file or directory
with stats [stat]. In order to do this, one needs to figure
out whether to look in the user, group or other part of the
permissions. *)
val uid_check_permission : forall 'dir_ref 'file_ref 'impl 'a 'b 'c.
environment 'dir_ref 'file_ref 'impl ->
(uid -> gid -> bool) ->
uid -> permission_type ->
ty_stats -> bool
let uid_check_permission env is_user_in_group uid pt stat = begin
let perm_check =
if (uid = stat.st_uid) then
permission_type_to_user_perm pt
else if is_user_in_group uid stat.st_gid then
permission_type_to_group_perm pt
else
permission_type_to_other_perm pt
in
check_file_perms stat.st_perm perm_check
end
(* ------------------------------------ *)
(* check-permission records *)
(* ------------------------------------ *)
(* ................ *)
(* full permissions *)
(* ................ *)
(* full_permissions grants all permissions, effectively, it turns off permission checking *)
val full_permissions : forall 'dir_ref 'file_ref 'impl. check_permissions 'dir_ref 'file_ref 'impl
let full_permissions = <|
cp_get_umask = (fun _ -> File_perm 0O0000); (* don't restrict anything *) (* coverage:unused -this field is overwritten by the only call to full_permissions *)
cp_get_euid = (fun () -> root_uid); (* coverage:unused -this field is overwritten by the only call to full_permissions *)
cp_get_egid = (fun () -> root_gid); (* coverage:unused -this field is overwritten by the only call to full_permissions *)
cp_has_dir_search_permission = (fun _ _ -> true);
cp_has_dir_read_permission = (fun _ _ -> true);
cp_has_dir_write_permission = (fun _ _ -> true);
cp_has_dir_chmod_permission = (fun _ _ -> true);
cp_has_dir_chown_permission = (fun _ _ -> true);
cp_has_file_execute_permission = (fun _ _ -> true); (* coverage:unused -this field is overwritten by the only call to full_permissions *)
cp_has_file_read_permission = (fun _ _ -> true);
cp_has_file_write_permission = (fun _ _ -> true);
cp_has_file_chmod_permission = (fun _ _ -> true);
cp_has_file_chown_permission = (fun _ _ -> true);
cp_has_dir_link_create_privilege = (fun _ _ -> true); (* coverage:unused -this field is overwritten by the only call to full_permissions *)
cp_has_dir_restricted_delete_privilege = (fun _ _ _ _ -> true);
cp_has_file_restricted_delete_privilege = (fun _ _ _ _ -> true);
|>
(* ..................... *)
(* superuser permissions *)
(* ..................... *)
(* superuser_permissions models the permissions of a superuser.
Only a tiny bit more restrictive than full_permissions (e.g. when
asking for execute permission) *)
(* check whether anyone is allowed to execute the file *)
val anyone_has_file_execute_permission : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
'impl -> 'file_ref -> bool
let anyone_has_file_execute_permission ops s0 i0_ref =
let i0_stats = ops.fops_stat_file s0 i0_ref in (* coverage:linux:irrelevant *)
let i0_perms = i0_stats.st_perm in (* coverage:linux:irrelevant *)
check_file_perms i0_perms S_IXUSR (* coverage:linux:irrelevant *)
||
check_file_perms i0_perms S_IXGRP (* coverage:linux:irrelevant *)
||
check_file_perms i0_perms S_IXOTH (* coverage:linux:irrelevant *)
val superuser_permissions : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
uid -> gid -> file_perm ->
check_permissions 'dir_ref 'file_ref 'impl
let superuser_permissions ops uid gid umask = <| full_permissions with
cp_get_euid = (fun () -> uid);
cp_get_egid = (fun () -> gid);
cp_has_file_execute_permission = anyone_has_file_execute_permission ops; (* coverage:linux:irrelevant *)
cp_has_dir_link_create_privilege = (fun _ _ -> true); (* allow superusers to create links to dirs, posix/link.md EPERM:1 FIXME this depends on the underlying filesystem as well *)
cp_get_umask = (fun _ -> umask);
|>
(* ............... *)
(* uid_permissions *)
(* ............... *)
(* uid_permissions gets the effective user uid from the process running. It then checks the permissions
for this user *)
val uid_has_dir_permission : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
(uid -> gid -> bool) ->
uid -> permission_type -> 'impl -> 'dir_ref -> bool
let uid_has_dir_permission env in_group uid pt s0 d0_ref =
let d0_stats = env.env_ops.fops_stat_dir s0 d0_ref in
uid_check_permission env in_group uid pt d0_stats
val uid_has_file_permission : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
(uid -> gid -> bool) ->
uid -> permission_type -> 'impl -> 'file_ref -> bool
let uid_has_file_permission env in_group uid pt s0 i0_ref =
let i0_stats = env.env_ops.fops_stat_file s0 i0_ref in
uid_check_permission env in_group uid pt i0_stats
(* [uid_has_restricted_delete_privilege ops uid allow_write s0 dir_stats file_stats] implements the
check, whether a file or directory can be deleted from a protected directory
(see posix/dir_protect.md). It is an auxiliary function used for both files and
directories. It gets only the stats, not a link to the file or it's parent dir.
Wrapper functions acquire these stats. *)
val uid_has_restricted_delete_privilege : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
(uid -> gid -> bool) ->
uid -> bool ->
ty_stats -> ty_stats -> bool
let uid_has_restricted_delete_privilege env in_group uid allow_write dir_stats file_stats = (
(* abort if there is no write permission on the directory. In this case, one
does not have delete permission, but the restricted one is fine. This is important
since a different error is raised if write permission is missing by e.g. rename or rm.
(see e.g. posix/rename.md EACCES:2 EPERM:1). *)
if (not (uid_check_permission env in_group uid Perm_write dir_stats)) then true else
(* Similarly abort, if the parent directory is not protected. *)
let dir_is_protected = check_file_perms dir_stats.st_perm S_ISVTX in
if (not dir_is_protected) then true else begin
(uid = file_stats.st_uid) ||
(uid = dir_stats.st_uid) ||
(allow_write
&& (uid_check_permission env in_group uid Perm_write file_stats)) (* coverage:impossible -there are no architectures that have arch_allows_removing_from_protected_dir_if_writeable set to true, so allow_write is always false*)
end
)
val uid_has_dir_restricted_delete_privilege : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
(uid -> gid -> bool) ->
uid -> bool -> 'impl ->
'dir_ref -> 'dir_ref -> bool
let uid_has_dir_restricted_delete_privilege env in_group uid allow_write s0 parent_dir_ref dir_ref =
let parent_dir_stats = env.env_ops.fops_stat_dir s0 parent_dir_ref in
let dir_stats = env.env_ops.fops_stat_dir s0 dir_ref in
uid_has_restricted_delete_privilege env in_group uid allow_write parent_dir_stats dir_stats
val uid_has_file_restricted_delete_privilege : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
(uid -> gid -> bool) ->
uid -> bool -> 'impl ->
'dir_ref -> 'file_ref -> bool
let uid_has_file_restricted_delete_privilege env in_group uid allow_write s0 parent_dir_ref file_ref =
let parent_dir_stats = env.env_ops.fops_stat_dir s0 parent_dir_ref in
let file_stats = env.env_ops.fops_stat_file s0 file_ref in
uid_has_restricted_delete_privilege env in_group uid allow_write parent_dir_stats file_stats
val uid_owns_file : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
uid ->
'impl ->
'file_ref -> bool
let uid_owns_file env uid s0 file_ref =
let file_stats = env.env_ops.fops_stat_file s0 file_ref in
(file_stats.st_uid = uid)
val uid_owns_dir : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
uid ->
'impl ->
'dir_ref -> bool
let uid_owns_dir env uid s0 dir_ref =
let file_stats = env.env_ops.fops_stat_dir s0 dir_ref in
(file_stats.st_uid = uid)
val uid_permissions : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
(uid -> gid -> bool) ->
uid -> gid -> file_perm ->
check_permissions 'dir_ref 'file_ref 'impl
let uid_permissions env in_group uid gid umask = <|
cp_get_umask = (fun _ -> umask);
cp_get_euid = (fun () -> uid);
cp_get_egid = (fun () -> gid);
cp_has_dir_search_permission = uid_has_dir_permission env in_group uid Perm_execute_search;
cp_has_dir_read_permission = uid_has_dir_permission env in_group uid Perm_read;
cp_has_dir_write_permission = uid_has_dir_permission env in_group uid Perm_write;
cp_has_dir_chmod_permission = uid_owns_dir env uid;
cp_has_dir_chown_permission = uid_owns_dir env uid;
cp_has_file_execute_permission= uid_has_file_permission env in_group uid Perm_execute_search;
cp_has_file_read_permission = uid_has_file_permission env in_group uid Perm_read;
cp_has_file_write_permission = uid_has_file_permission env in_group uid Perm_write;
cp_has_file_chmod_permission = uid_owns_file env uid;
cp_has_file_chown_permission = uid_owns_file env uid;
cp_has_dir_link_create_privilege = (fun _ _ -> false);
cp_has_dir_restricted_delete_privilege = uid_has_dir_restricted_delete_privilege env in_group uid;
cp_has_file_restricted_delete_privilege = uid_has_file_restricted_delete_privilege env in_group uid;
|>
(* ------------------------------------ *)
(* user management *)
(* ------------------------------------ *)
val get_uids_in_gid : forall 'dir_ref 'file_ref 'impl. ty_os_state 'dir_ref 'file_ref 'impl -> gid -> finset uid
let get_uids_in_gid s gid =
match fmap_lookup s.oss_group_table gid with
| Nothing -> finset_empty ()
| Just uids -> uids
end
val is_uid_in_gid : forall 'dir_ref 'file_ref 'impl. ty_os_state 'dir_ref 'file_ref 'impl -> uid -> gid -> bool
let is_uid_in_gid s uid gid = finset_mem uid (get_uids_in_gid s gid)
val add_uid_to_gid : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl -> uid -> gid -> ty_os_state 'dir_ref 'file_ref 'impl
let add_uid_to_gid s uid gid = (
let current_uids = get_uids_in_gid s gid in
let new_uids = finset_insert uid current_uids in
let new_groups = fmap_update s.oss_group_table (gid, new_uids) in
<| s with oss_group_table = new_groups |>
)
end
#endif
(******************************************************************************)
(* Resolving paths *)
(******************************************************************************)
(**
## Resolve names
Update: we first process the string to give a list of entries; /a/b/c -> ["";"a";"b";"c"]; /a/b/c/ -> ["";"a";"b";"c";""]; a/b/c -> ["a";"b";"c"]; note that [] is not in the range of this function; the empty string "" maps to [""]. We keep this first list because we may need to examine it at some points.
FIXME we need to distinguish between a null string and an empty string
what about a relative path that is empty? in this case, it appears that this is returned as an error ENOENT (so the CWD is not appended in this case)
interestingly if you delete /tmp/d1 and a process is still in d1, the PWD for that process is /tmp/d1; and in /proc/pid/cwd it says "/tmp/d1 (deleted)"
**)
module Resolve = struct
open T_fs_prelude
open Fs_types
open Fs_arch
#ifdef aspect_perms
open Fs_permissions
#endif
(*-------------------------------*)
(* real_path_dir_ref *)
(*-------------------------------*)
val is_root_dir : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
'impl ->
'dir_ref ->
bool
let is_root_dir ops s0 d0_ref = (
let root = (
match ops.fops_get_root s0 with
| Nothing -> (failwith "is_root_dir: impossible: no root")
| Just x -> x end)
in
ops.fops_dir_ref_eq s0 root d0_ref)
(* get the real path, given a dir_ref; the real path of "/" is ["";""] the real path of "/n" is ["";"n"] *)
val real_path_dir_ref : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl -> 'impl ->
'dir_ref -> list name
let rec real_path_dir_ref ops s0 d0_ref = (
match (is_root_dir ops s0 d0_ref) with
| true -> ["";""] (* if root, return the corresponding real path *)
| false -> (
let p = ops.fops_get_parent s0 d0_ref in
(match p with
| Nothing -> (
(* d0_ref is not root, but no parent; disconnected directory? *)
failwith "real_path_dir_ref: disconnected directory? FIXME")
| Just(d1_ref,n) -> (
if (is_root_dir ops s0 d1_ref) then
["";n]
else
(real_path_dir_ref ops s0 d1_ref)++[n]) end)) end)
(* Termination argument:
Why does real_path_dir_ref terminate? Informal argument: there is a fixed mapping to absolute dirs. *)
val fops_get_parent_OK_abs_map : forall 'a 'b 'c. Eq 'a => fs_ops 'a 'b 'c -> 'c -> ('a -> list string) -> bool
let non_exec fops_get_parent_OK_abs_map ops s0 abs_map = (forall d0_ref.
match (abs_map d0_ref) with
| [] -> (ops.fops_get_parent s0 d0_ref = Nothing)
| (n :: ns) -> ((n <> "") && (n <> ".") && (n <> "..") &&
(exists d1_ref. (ops.fops_get_parent s0 d0_ref = Just (d1_ref, n)) &&
(abs_map d1_ref = ns)))
end);;
let non_exec fops_get_parent_OK ops s0 = (exists abs_map. fops_get_parent_OK_abs_map ops s0 abs_map);;
theorem real_path_dir_ref_wf : (forall ops s0 d0_ref. fops_get_parent_OK ops s0 -->
is_simple_absolute_path (real_path_dir_ref ops s0 d0_ref))
(*-------------------------------*)
(* datatype for resolve results *)
(*-------------------------------*)
(* this is a cutdown version of res_name that is used
during resolution. Once resolution is finished, it is
transformed into a res_name by adding additional fields. *)
type ty_resolve_relative_result 'dir_ref 'file_ref =
RR_dir of 'dir_ref
| RR_file of ('dir_ref * name * 'file_ref)
| RR_none of ('dir_ref * name)
| RR_error of (error * maybe (ty_resolve_relative_result 'dir_ref 'file_ref))
val ty_resolve_relative_result2res_name : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
'impl ->
'dir_ref ->
ty_name_list ->
ty_resolve_relative_result 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref
let rec ty_resolve_relative_result2res_name ops s0 cwd nl x =
match x with
| RR_dir d0_ref -> (
let rp = <| rp_cwd=cwd; rp_nl=nl; rp_ns=(real_path_dir_ref ops s0 d0_ref) |> in
RN_dir(d0_ref,rp))
| RR_file (d0_ref,n,i0_ref) -> (
let rp = <| rp_cwd=cwd; rp_nl=nl; rp_ns=((real_path_dir_ref ops s0 d0_ref)++[n]) |> in
RN_file(d0_ref,n,i0_ref,rp))
| RR_none (d0_ref,n) ->
let rp = <| rp_cwd=cwd; rp_nl=nl; rp_ns=(real_path_dir_ref ops s0 d0_ref)++[n] |> in
RN_none (d0_ref,n,rp)
| RR_error (e, res_without_sl) -> (RN_error(e,<| re_cwd=cwd; re_nl=(Just nl);
re_rn=Maybe.map (ty_resolve_relative_result2res_name ops s0 cwd nl) res_without_sl |>))
end
declare termination_argument ty_resolve_relative_result2res_name = automatic
(*-------------------------------*)
(* split path into name lists *)
(*-------------------------------*)
(* [split_path_string] is the first processing step during path resolution.
It splits a path into a non-empty list of names separated by "/".
See tests in fs_test/paths.testpath.ml and fs_test/testpath.native. The expected invariant is that
s |> split_path_string |> ty_name_list_to_list |> String.concat "/" should be the identity.
*)
val split_path_string : string -> ty_name_list
let split_path_string path = (
let p = String.toCharList path in
let f1 ((ns:list string),(cur:list char)) c = (if c=#'/' then (ns++[String.toString (reverse cur)],[]) else (ns,c::cur)) in
let (ns,cur) = List.foldl f1 ([],[]) p in
let ns = ns++[String.toString (reverse cur)] in
make_ty_name_list ns) (* invariant: ns is not [] - see line above! *)
(* inverse of split_path_string *)
val ty_name_list_to_string: ty_name_list -> string
let ty_name_list_to_string tnl = (
match tnl with
| Name_list (n,nl) ->
let f1 sofar n = sofar^"/"^n in
List.foldl f1 n nl end)
(*-------------------------------*)
(* resolve_relative *)
(*-------------------------------*)
(* whether to follow the last symlink when resolving paths for a command; apart from OS_CHXXX, the default appears to be false, but POSIX does resolve if a trailing slash whereas Linux typically doesn't *)
val follow_last_symlink : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_os_command ->
bool
let follow_last_symlink env cmd = (
let arch = architecture_of_ty_arch env.env_arch in
let dummy = true in (* some commands don't have paths, so follow_last_symlink is irrelevant *)
match cmd with
| OS_CLOSE _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_LINK _ -> (
if is_mac_os_x_arch env then
true (* check_exec_adhoc_symlink_tests-int.trace link "/dir_link" "/dir_4" ; mac follows /dir_link and result is EPERM *)
else
false)
| OS_MKDIR _ -> false
| OS_OPEN (p,fs,mo) -> (
let oflags = arch.arch_open_flags_of_int fs in
if finset_mem O_EXCL oflags && finset_mem O_CREAT oflags then
false (* posix/open.md O_EXCL:3 , don't follow if O_EXCL and O_CREAT *)
else if finset_mem O_NOFOLLOW oflags then (* posix/open.md ELOOP:1 *)
false
else
true)
| OS_PREAD _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_READ _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_READDIR _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_OPENDIR _ -> true (* can't opendir a symlink *)
| OS_REWINDDIR _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_CLOSEDIR _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_READLINK _ -> false (* FIXME on Linux, it does follow if there is a trailing slash *)
| OS_RENAME _ -> false (* FIXME false on Linux, but under posix should this be true? cf POSIX/Linux differences with rename of link to dir *)
| OS_RMDIR _ -> false (* FIXME really? *)
| OS_STAT _ -> true
| OS_LSTAT _ -> false (* lstat doesn't follow *)
| OS_SYMLINK _ -> false
| OS_TRUNCATE _ -> true (* can't truncate a link *)
| OS_UNLINK _ -> false
| OS_PWRITE _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_WRITE _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_UMASK _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_CHMOD _ -> true
| OS_CHOWN _ -> true
| OS_CHDIR _ -> true
| OS_LSEEK _ -> dummy (* coverage:impossible -this command does not use path, so follow_last_symlink is never called on it *)
| OS_EXTENDED_CMD _ -> dummy (* only matters for OPEN_CLOSE, where hopefully we don't use it on a symlink *)
end)
let is_OS_READLINK cmd = (match cmd with OS_READLINK _ -> true | _ -> false end) (* coverage:mac_os_x:posix:irrelevant - used only in a case for linux only *)
let is_OS_LSTAT cmd = (match cmd with OS_LSTAT _ -> true | _ -> false end) (* coverage:mac_os_x:posix:irrelevant - used only in a case for linux only *)
type rr_params 'dir_ref 'file_ref 'impl = <| rr_env: environment 'dir_ref 'file_ref 'impl; rr_s0: 'impl; rr_cmd: ty_os_command |>
(* in order to make the recursive structure clear (for theorem
provers, and humans) auxiliary functions don't recurse directly, but
return the result of processing, which may be [RR_final] to indicate
that processing is finished, or [RR_inter] to indicate that further
processing should happen *)
type rr_input 'dir_ref = <| rr_symlinks_so_far: nat; rr_so_far: 'dir_ref; rr_ns: list string |>
type rr_output 'dir_ref 'file_ref =
| RR_inter of rr_input 'dir_ref
| RR_final of ty_resolve_relative_result 'dir_ref 'file_ref
val rr_dot_dot : forall 'dir_ref 'file_ref 'impl.
rr_params 'dir_ref 'file_ref 'impl ->
nat ->
'dir_ref ->
list string ->
rr_output 'dir_ref 'file_ref
let rr_dot_dot ps symlinks_so_far so_far ns =
(match ps.rr_env.env_ops.fops_get_parent ps.rr_s0 so_far with
| Nothing -> (RR_inter <| rr_symlinks_so_far=symlinks_so_far; rr_so_far=so_far; rr_ns=ns |>)
(* FIXME not correct for disconnected dirs - should probably throw an exception ENOENT *)
| Just(dir_ref,_) -> (RR_inter <| rr_symlinks_so_far=symlinks_so_far; rr_so_far=dir_ref; rr_ns=ns |>) end)
(* i0_ref is a symlink *)
val rr_symlink : forall 'dir_ref 'file_ref 'impl.
rr_params 'dir_ref 'file_ref 'impl ->
nat ->
'dir_ref ->
list string ->
string ->
'file_ref ->
rr_output 'dir_ref 'file_ref
let rr_symlink ps symlinks_so_far so_far ns n i0_ref = (
(* process a symlink *)
(* do we follow the symlink? *)
let is_last_component = List.all (fun s -> s="") ns in (* the last component is n in .../n or .../n//// *)
let follow_last_symlink = follow_last_symlink ps.rr_env ps.rr_cmd in (* whether to follow last symlink depends mainly on the command *)
let follow_symlink = (
match is_linux_arch ps.rr_env with
| true -> (
if is_last_component then (* coverage:mac_os_x:posix:irrelevant *)
follow_last_symlink (* regardless of trailing slashes *) (* coverage:mac_os_x:posix:irrelevant *)
|| (
let is_os_open_nofollow = (match ps.rr_cmd with
| OS_OPEN (_,fs,_) -> (
let arch = architecture_of_ty_arch ps.rr_env.env_arch in
let oflags = arch.arch_open_flags_of_int fs in
(finset_mem O_NOFOLLOW oflags))
| _ -> false end)
in
(is_OS_READLINK ps.rr_cmd || is_OS_LSTAT ps.rr_cmd || is_os_open_nofollow) && ns <> []) (* ie readlink symlink/ or lstat symlink/ or open [O_NOFOLLOW] symlink/, in which case do follow *) (* coverage:mac_os_x:posix:irrelevant *)
else
true(*ns <> [] || follow_last_symlink *)) (* coverage:mac_os_x:posix:irrelevant *)
| false -> ( (*coverage:linux:irrelevant*)
ns <> [] (* if used as a directory, link is always followed except under Linux *) (*coverage:linux:irrelevant*)
|| follow_last_symlink) end) (* if last component, then as follow_last_symlink *) (*coverage:linux:irrelevant*)
in
(match follow_symlink with
| true -> (
(* check whether too many symbolic links have already been followed *)
if (symlinks_so_far >= ps.rr_env.env_ops.fops_lookup_sysconf ps.rr_s0 SC_SYMLOOP_MAX) then RR_final (RR_error(ELOOP, Nothing)) else
(* read the link contents *)
let bs = ps.rr_env.env_ops.fops_readlink ps.rr_s0 i0_ref in
let s = T_list_array.to_string bs in
(* at this point, we need to process bs as a path, possibly an absolute path *)
let nl = split_path_string s in
if nl_starts_with_slash nl then
let root = fromJust (ps.rr_env.env_ops.fops_get_root ps.rr_s0) in
RR_inter <| rr_symlinks_so_far=(succ symlinks_so_far); rr_so_far=root; rr_ns=(ty_name_list_to_list nl ++ ns) |>
else
RR_inter <| rr_symlinks_so_far=(succ symlinks_so_far); rr_so_far=so_far; rr_ns=(ty_name_list_to_list nl ++ ns) |>)
| false -> (
(* in this case, ns=[] and ps.rr_follow_last_symlink was false; return the symlink itself *)
RR_final (RR_file(so_far,n,i0_ref)) (* if we are at the end, return the file *)) end))
val alt_rr : forall 'dir_ref 'file_ref 'impl.
rr_params 'dir_ref 'file_ref 'impl ->
nat ->
'dir_ref -> list string ->
ty_resolve_relative_result 'dir_ref 'file_ref
let rec alt_rr ps symlinks_so_far so_far ns = (
(match ns with
| [] -> (RR_dir(so_far))
| n::ns -> (
#ifdef aspect_perms
(* if we have no search permission on component n, raise EACCES, except
on Linux for the parent directory *)
if ((not (ps.rr_env.env_prms.cp_has_dir_search_permission ps.rr_s0 so_far)) &&
(not (is_linux_arch ps.rr_env && (n = "")))) then (* FIXME trace? *) (* coverage:mac_os_x:posix:irrelevant *)
RR_error(EACCES, Nothing) else
#endif
let is_last_component = List.all (fun s -> s="") ns in (* the last component is n in .../n or .../n//// *)
(match n with
(* process empty and . and .. entries *)
| "" -> (alt_rr ps symlinks_so_far so_far ns)
| "." -> (alt_rr ps symlinks_so_far so_far ns)
| ".." -> (match rr_dot_dot ps symlinks_so_far so_far ns with
| RR_inter i0 -> alt_rr ps i0.rr_symlinks_so_far i0.rr_so_far i0.rr_ns
| RR_final r -> r end) (* coverage:impossible - rr_dot_dot can only return RR_inter *)
| _ -> (
(* try and resolve n (the next path component) *)
let m = ps.rr_env.env_ops.fops_resolve ps.rr_s0 so_far n in
(match m with
| Nothing -> (if is_last_component then RR_none(so_far,n) else RR_error(ENOENT, Nothing)) (* posix/rename.md ENOENT:2; posix/link.md ENOENT:1; posix/rmdir.md ENOENT:2 *)
| Just entry -> ( (* process the entry corresponding to n *)
(match entry with
| Dir_ref_entry d0_ref -> (alt_rr ps symlinks_so_far d0_ref ns)
| File_ref_entry i0_ref -> (
let is_symlink = ((ps.rr_env.env_ops.fops_stat_file ps.rr_s0 i0_ref).st_kind = S_IFLNK) in
(match is_symlink with
| true -> (match rr_symlink ps symlinks_so_far so_far ns n i0_ref with
| RR_inter i0 -> alt_rr ps i0.rr_symlinks_so_far i0.rr_so_far i0.rr_ns
| RR_final r -> r end)
| false -> (match ns with
| [] -> (RR_file(so_far,n,i0_ref)) (* return if no more path components to process *)
| _ -> (
(* we got a file, which is not a symlink and it is not the last component during
path resolution. So always raise an error. However, a common problem are trailing
slashes. In this case raise and error, but also return the file found. *)
let opt = (if is_last_component then Just (RR_file(so_far,n,i0_ref)) else Nothing) in
RR_error(ENOTDIR, opt)) end) (* posix/rename.md ENOTDIR:1 ENOTDIR:3 ENOTDIR:5; posix/link.md ENOTDIR:1 ENOTDIR:3; FIXME posix/mkdir.md ENOENT:4 specifies that this may return ENOENT, but this is surely a POSIX specification error *)
end)) end)) end) ) end)) end))
val resolve_relative : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
'impl -> ty_os_command -> nat ->
'dir_ref -> list string ->
ty_resolve_relative_result 'dir_ref 'file_ref
let rec resolve_relative env s0 cmd symlinks_so_far so_far ns = (
alt_rr <| rr_env=env; rr_s0=s0; rr_cmd=cmd |> symlinks_so_far so_far ns)
(*
let rec resolve_relative env s0 follow_last_symlink symlinks_so_far sofar ns = (
match ns with
| [] -> (RR_dir(sofar))
| n::ns -> (
(* process . and .. entries *)
if (n=".") || (n="") then (
resolve_relative env s0 follow_last_symlink symlinks_so_far sofar ns
) else if (n="..") then (
(match env.env_ops.fops_get_parent s0 sofar with
| Nothing -> (resolve_relative env s0 follow_last_symlink symlinks_so_far sofar ns) (* FIXME not correct for disconnected dirs *)
| Just(dir_ref,_) -> (resolve_relative env s0 follow_last_symlink symlinks_so_far dir_ref ns)
end)
#ifdef aspect_perms
) else if (not (env.env_prms.cp_has_dir_search_permission s0 sofar)) then RR_error(EACCES, Nothing) else (
#else
) else (
#endif
(* try and resolve n (the next path component) *)
let m = env.env_ops.fops_resolve s0 sofar n in
(match m with
| Nothing -> (
if (ns=[]) || (ns=[""]) then (* may end in a slash; FIXME what about multiple slashes? *)
RR_none(sofar,n)
else
RR_error(ENOENT, Nothing)) (* posix/rename.md ENOENT:2; posix/link.md ENOENT:1; posix/rmdir.md ENOENT:2 *)
| Just entry -> (
(* process the entry corresponding to n *)
(match entry with
| File_ref_entry i0_ref -> (
(* process a symlink *)
(* If i0_ref is a symlink, do we follow it? *)
let follow_symlink =
(* of course we only do it, if it is really a symlink *)
((env.env_ops.fops_stat_file s0 i0_ref).st_kind = S_IFLNK) (* is it actually one *) && (
(* if used as a directory, it is always followed *)
(ns <> []) ||
(* if it is the last component, it depends on
the command that requested the resolution. Commands like
[open] want to follow the symlink, whereas e.g. [unlink] does
not. The argument [follow_last_symlink] is used for this purpose. *)
follow_last_symlink
) in
if (follow_symlink) then
(* check whether too many symbolic links have already been followed *)
if (symlinks_so_far >= env.env_ops.fops_lookup_sysconf s0 SC_SYMLOOP_MAX) then
RR_error(ELOOP, Nothing)
else (
let bs = env.env_ops.fops_readlink s0 i0_ref in
let s = T_list_array.to_string bs in
(* FIXME at this point, we need to process bs as a path, possibly an absolute path *)
let nl = split_path_string s in
if nl_starts_with_slash nl then
let root = fromJust (env.env_ops.fops_get_root s0) in
resolve_relative env s0 follow_last_symlink (succ symlinks_so_far) root (ty_name_list_to_list nl ++ ns)
else
resolve_relative env s0 follow_last_symlink (succ symlinks_so_far) sofar (ty_name_list_to_list nl ++ ns) (* potentially non-terminating eg ln -s loop loop *)
)
(* return if no more path components to process *)
else if (ns=[]) then
RR_file(sofar,n,i0_ref) (* if we are at the end, return the file *)
else
(* we got a file, which is no symlink and it is not the last component
during path resolution. So, we are in trouble. So always raise an error.
However, a common problem are trailing slashes. In this case raise and error,
but also return the file found. *)
(let res_without_slashes = (if (List.all (fun s -> s = "") ns) then Just (RR_file(sofar,n,i0_ref)) else Nothing) in
RR_error(ENOTDIR, res_without_slashes))) (* posix/rename.md ENOTDIR:1 ENOTDIR:3 ENOTDIR:5; posix/link.md ENOTDIR:1 ENOTDIR:3; FIXME posix/mkdir.md ENOENT:4 specifies that this may return ENOENT, but this is surely a POSIX specification error *)
| Dir_ref_entry d0_ref -> (
resolve_relative env s0 follow_last_symlink symlinks_so_far d0_ref ns) end)) end)) ) end)
*)
(* if a path starts with two slashes, the behaviour is impl defined;
we don't want to deal with this in every command, so we have a
clause in os_trans that uses this definition *)
val path_starts_with_exactly_two_slashes : cstring -> bool
let path_starts_with_exactly_two_slashes s = (
match s with | CS_Null -> false | CS_Some s ->
let nl = split_path_string s in
(match (ty_name_list_to_list nl) with
| (""::""::[]) -> false (* / *)
| (""::""::xs) -> (
(* starts with at least two slashes, but how many exactly? *)
match xs with
| [] -> (failwith "impossible: case considered above")
| ""::[] -> true (* // *)
| ""::_ -> false (* three slashes *)
| _ -> true (* //tom *) end)
| _ -> false
end) end)
(* process path is only called, on path that do NOT start with with
two slashes, the behaviour in this case is impl defined, the the
implementation of pre_os_trans guarentees that process_path is
only called on such paths *)
val process_path : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
'impl ->
'dir_ref -> ty_os_command -> cstring ->
res_name 'dir_ref 'file_ref
let process_path env s0 cwd cmd path = (
match path with
| CS_Null -> (RN_error(ENOENT,<|re_cwd=cwd;re_nl=Nothing;re_rn=Nothing|>))
| CS_Some path -> (
let nl = split_path_string path in
if (path = "") then
RN_error(ENOENT,<|re_cwd=cwd;re_nl=Just nl;re_rn=Nothing|>)
(* posix/rename.md ENOENT:3; posix/link.md ENOENT:3; posix/rmdir.md ENOENT:3 *)
else (
let init_cwd = if nl_starts_with_slash nl then fromJust (env.env_ops.fops_get_root s0) else cwd in
let res = resolve_relative env s0 cmd 0 init_cwd (ty_name_list_to_list nl) in
ty_resolve_relative_result2res_name env.env_ops s0 cwd nl res
))
end)
(* FIXME this complexity should be incorporated into process path? *)
(* this is a complete hack because Mac OS X behaviour is very
strange wrt trailing slashes and symlinks; we try to resolve a path,
after first removing any trailing slashes; we then check if we have a symlink *)
val process_path_no_follow_no_trailing_slash : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
'impl ->
'dir_ref -> cstring ->
res_name 'dir_ref 'file_ref
let process_path_no_follow_no_trailing_slash env s0 cwd path = (
let cmd = OS_READLINK path in
let path = (match path with
| CS_Null -> CS_Null
| CS_Some path -> (
(* strip trailing slashes *)
let p = String.toCharList path in
let p = reverse p in
let p = dropWhile (fun c -> c=#'/') p in
let p = reverse p in
CS_Some(String.toString p)) end)
in
process_path env s0 cwd cmd path)
val process_path_from_root : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
'impl ->
ty_os_command -> cstring -> res_name 'dir_ref 'file_ref
let process_path_from_root env s0 cmd path = (
let root = fromJust (env.env_ops.fops_get_root s0) in
process_path env s0 root cmd path)
val res_name_is_symlink : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
'impl -> res_name 'dir_ref 'file_ref -> bool
let res_name_is_symlink ops s0 rn = match rn with
| RN_file(_,_,i0_ref,_) -> ((ops.fops_stat_file s0 i0_ref).st_kind = S_IFLNK)
| _ -> false
end
end
(******************************************************************************)
(* The Monad *)
(******************************************************************************)
module The_monad = struct
open Fs_types
(*---------------------------------*)
(* Monad type with bind and return *)
(*---------------------------------*)
(* Our monad is used to implement filesystem operations. It is able
to encode non-deterministic choice between a finite set of
states. Normal states are abstract fs-states, there are also
error and special states, though. (see type-definition of
monad_state). *)
type fsmonad 'impl 'ja = Fsmonad of ('impl -> finset (monad_state 'impl 'ja ))
val dest_fsmonad : forall 'impl 'a. fsmonad 'impl 'a ->
('impl -> finset (monad_state 'impl 'a))
let dest_fsmonad (Fsmonad u) = u (* coverage:unused *)
val fsm_return : forall 'impl 'a. 'a -> fsmonad 'impl 'a
let fsm_return x = Fsmonad (fun s -> finset_singleton (Normal_state (s, x)))
val run_fsmonad : forall 'impl 'a. fsmonad 'impl 'a ->
'impl -> finset (monad_state 'impl 'a)
let run_fsmonad (Fsmonad f) s = (f s)
val fsm_bind_process_single_state : forall 'impl 'a 'b.
('a -> fsmonad 'impl 'b) ->
monad_state 'impl 'a ->
finset (monad_state 'impl 'b)
let fsm_bind_process_single_state f v = (match v with
| Error_state se -> (finset_singleton (Error_state se)) (* stop once error is reached *)
| Special_state sm -> (finset_singleton (Special_state sm)) (* stop once special state is reached *)
| Normal_state sx -> (run_fsmonad (f (snd sx)) (fst sx))
end)
val fsm_bind : forall 'impl 'a 'b.
fsmonad 'impl 'a ->
('a -> fsmonad 'impl 'b) ->
fsmonad 'impl 'b
let fsm_bind u f = Fsmonad (fun s0 ->
let result_states = run_fsmonad u s0 in
(finset_bigunion_image (fsm_bind_process_single_state f) result_states))
val (>>=) : forall 'impl 'a 'b. fsmonad 'impl 'a -> ('a -> fsmonad 'impl 'b) -> fsmonad 'impl 'b
let (>>=) = fsm_bind
(*---------------------------------*)
(* Basic monad operations *)
(*---------------------------------*)
(* we have 3 main constructor:
- fsm_normal: construct successful executions
- fsm_raise: raise an error
- fsm_special: mark a special state
*)
val fsm_normal : forall 'impl 'a. ('impl -> ('impl * 'a)) -> fsmonad 'impl 'a
let fsm_normal f = Fsmonad (fun s -> finset_singleton (Normal_state (f s)))
val fsm_raise : forall 'impl 'a. error -> fsmonad 'impl 'a
let fsm_raise e = Fsmonad (fun s -> finset_singleton(Error_state (s, e)))
val fsm_special : forall 'impl 'a. monad_special_state -> string -> fsmonad 'impl 'a
let fsm_special spec_s m = Fsmonad (fun s -> finset_singleton(Special_state(spec_s,m)))
(*---------------------------------*)
(* Useful operations *)
(* derived from basic ones *)
(*---------------------------------*)
val fsm_get_state : forall 'impl. fsmonad 'impl 'impl
let ~{ocaml} fsm_get_state = fsm_normal (fun s -> (s, s))
let {ocaml} fsm_get_state = Fsmonad (fun s -> finset_singleton (Normal_state (s, s)))
(* OCaml needs unfolding the definition of fsm_normal to generalize the state type *)
val fsm_put_state : forall 'impl. 'impl -> fsmonad 'impl ret_value
let fsm_put_state s = fsm_normal (fun _ -> (s, RV_none))
val fsm_put_state_return : forall 'impl 'a. 'impl -> 'a -> fsmonad 'impl 'a
let fsm_put_state_return s x = fsm_normal (fun _ -> (s, x))
lemma fsm_put_state_alt_def : forall s. fsm_put_state s = fsm_put_state_return s RV_none
val fsm_do_nothing : forall 'impl. fsmonad 'impl ret_value
let ~{ocaml} fsm_do_nothing = fsm_normal (fun s -> (s, dummy_return_value))
let {ocaml} fsm_do_nothing = Fsmonad (fun s -> finset_singleton (Normal_state (s, dummy_return_value)))
(* OCaml needs unfolding the definition of fsm_normal to generalise the state type *)
lemma fsm_return_alt_def : forall x. fsm_return x = fsm_normal (fun s -> (s, x))
(*--------------------------------------*)
(* multiple sucessful return states *)
(*--------------------------------------*)
val fsm_normals : forall 'impl 'a 'b. (('impl * 'b) -> ('impl * 'a)) -> list 'b -> fsmonad 'impl 'a
let fsm_normals f l = Fsmonad (fun s -> finset_from_list (map (fun x -> Normal_state (f (s, x))) l))
val fsm_returns : forall 'impl 'a. list 'a -> fsmonad 'impl 'a
let fsm_returns xs = fsm_normals id xs
(* [fsm_choose_nat n] chooses nondeterministically a number between [0] (including) and
[n] (including) *)
val fsm_choose_nat : forall 'impl. nat -> fsmonad 'impl nat
let fsm_choose_nat n = fsm_returns (List.genlist id (succ n))
(*--------------------------------------*)
(* raising multiple errors and specials *)
(*--------------------------------------*)
(* Instead of raising errors and special states individually, it is convenient to use
lists and non-deterministically raise one in the list. *)
type error_or_special =
| EOS_error of error
| EOS_special of (monad_special_state * string)
val error_or_special_to_state : forall 'impl 'a. 'impl -> error_or_special -> monad_state 'impl 'a
let error_or_special_to_state s eos =
match eos with
| EOS_error e -> Error_state (s, e)
| EOS_special ssm -> Special_state ssm (* coverage:linux:irrelevant *)
end
val fsm_raises_specials : forall 'impl 'a.
list error_or_special ->
fsmonad 'impl 'a
let fsm_raises_specials eoss =
Fsmonad (fun s -> finset_from_list (List.map (error_or_special_to_state s) eoss))
val fsm_raises : forall 'impl 'a. list error -> fsmonad 'impl 'a
let fsm_raises es = fsm_raises_specials (map EOS_error es)
val fsm_specials : forall 'impl 'a. list (monad_special_state * string) -> fsmonad 'impl 'a
let fsm_specials sms = (* coverage:unused *)
fsm_raises_specials (map EOS_special sms) (* coverage:unused *)
val fsm_cond_raises_specials : forall 'impl.
list (error_or_special * bool) ->
fsmonad 'impl ret_value
let fsm_cond_raises_specials ceoss =
let eoss = (List.map fst (List.filter snd ceoss)) in
if List.null eoss then
fsm_do_nothing
else
fsm_raises_specials eoss
val fsm_cond_raises : forall 'impl. list (error * bool) -> fsmonad 'impl ret_value
let fsm_cond_raises bes = fsm_cond_raises_specials (List.map (fun (e, b) -> (EOS_error e, b)) bes)
val fsm_cond_raise : forall 'impl. error -> bool -> fsmonad 'impl ret_value
let fsm_cond_raise e b = fsm_cond_raises [(e, b)]
val fsm_cond_specials : forall 'impl. list ((monad_special_state * string) * bool) -> fsmonad 'impl ret_value
let fsm_cond_specials bsms = fsm_cond_raises_specials (List.map (fun (sm, b) -> (EOS_special sm, b)) bsms)
val fsm_cond_special : forall 'impl. monad_special_state -> string -> bool -> fsmonad 'impl ret_value
let fsm_cond_special ss m b = fsm_cond_specials [((ss, m), b)]
(*---------------------------------*)
(* non-deterministic choice *)
(*---------------------------------*)
val fsm_empty : forall 'impl 'a. fsmonad 'impl 'a
let fsm_empty = Fsmonad (fun s -> finset_empty ()) (* coverage:unused *)
val fsm_choice : forall 'impl 'a. fsmonad 'impl 'a -> fsmonad 'impl 'a -> fsmonad 'impl 'a
let fsm_choice m1 m2 = Fsmonad (fun s -> finset_union (run_fsmonad m1 s) (run_fsmonad m2 s)) (* coverage:unused *)
(*---------------------------------*)
(* parallel composition *)
(*---------------------------------*)
(* When checking for errors, it is often handy to be able to
consider errors independently. The following parallel composition
operator first runs two monads in both orders and returns all
possible results. This is a crude model for parallel
composition. *)
val fsm_parallel_composition : forall 'impl 'a 'b.
fsmonad 'impl 'a ->
fsmonad 'impl 'b ->
fsmonad 'impl ('a * 'b)
let fsm_parallel_composition m1 m2 = (* coverage:unused *)
fsm_choice
((* either un m1 and then m2 *)
(m1 >>= (fun x1 -> (m2 >>= (fun x2 -> fsm_return (x1, x2)))))) (* coverage:unused *)
((* or m2 and then m1 *)
(m2 >>= (fun x2 -> (m1 >>= (fun x1 -> fsm_return (x1, x2)))))) (* coverage:unused *)
(* [fsm_parallel_composition] is simple to define, but rather
crude. One problem is for example that the operation is not
associative in general, a property that one normally would
expect. We intend to use parallel composition mainly for
error-checking. In this case we can enforce that the operations
do not modify the state and we can discard the return values. The
resulting operation [fsm_parallel_composition_drop] has nice properties
like being associative.
The described high-level, abstract definition of
[fsm_parallel_composition_drop] is inefficient to execute. So, we
first define an efficiently executable version and then state as
a lemma that this efficient implementation is equivalent to the
abstract definition described above. The implementation is
interesting on it's own. It shows that the parallel composition
operator collects the errors from both monads and combines
them. It adds a normal state, iff both monads might right a
normal state. *)
val fsm_parallel_composition_drop : forall 'impl.
fsmonad 'impl ret_value ->
fsmonad 'impl ret_value ->
fsmonad 'impl ret_value
let fsm_parallel_composition_drop m1 m2 = Fsmonad (fun s ->
let (st_s1_n, st_s1) = finset_partition is_Normal_state (run_fsmonad m1 s) in
let (st_s2_n, st_s2) = finset_partition is_Normal_state (run_fsmonad m2 s) in
let res = finset_union st_s1 st_s2 in
let res' = finset_cleanup monad_state_shallow_eq res in (* remove obvious duplicates *)
if (finset_is_empty st_s1_n || finset_is_empty st_s2_n) then
res'
else
finset_insert (Normal_state (s, dummy_return_value)) res'
)
(* enforce that a monad does not change the state *)
val fsm_preserve_state : forall 'a 'b. fsmonad 'a 'b -> fsmonad 'a 'b
let fsm_preserve_state m = (* coverage:unused *)
fsm_get_state >>= (fun s0 -> m >>= (fun r -> fsm_normal (fun _ -> (s0, r))))
lemma fsm_parallel_composition_drop_alt_def : (forall m1 m2. fsm_parallel_composition_drop m1 m2 =
(fsm_parallel_composition
(fsm_preserve_state (m1 : fsmonad 'impl ret_value))
(fsm_preserve_state (m2 : fsmonad 'impl ret_value)) >>=
(fun (_, _) -> fsm_return dummy_return_value)))
(* define infix notations for parallel composition operators *)
val (<|||>) : forall 'impl 'a 'b. fsmonad 'impl 'a -> fsmonad 'impl 'b -> fsmonad 'impl ('a * 'b)
let (<|||>) = fsm_parallel_composition
val (|||) : forall 'impl. fsmonad 'impl ret_value -> fsmonad 'impl ret_value -> fsmonad 'impl ret_value
let (|||) = fsm_parallel_composition_drop
end
(******************************************************************************)
(* Fs_operations *)
(* *)
(* This is one of the central parts of the specifications. It contains *)
(* models of the operations at file-system level. *)
(******************************************************************************)
module Fs_operations = struct
open T_fs_prelude
open Fs_types
open Fs_arch
open The_monad
#ifdef aspect_perms
open Fs_permissions
#endif
(*--------------------------*)
(* auxiliary functions *)
(*--------------------------*)
(* [dir_is_empty env.env_ops s0 d0_ref] checks that a directory [d0_ref] is empty in state [s0]. *)
val dir_is_empty : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
'impl -> 'dir_ref -> bool
let dir_is_empty ops s0 d0_ref = (match (ops.fops_readdir s0 d0_ref) with
| (_, []) -> true | _ -> false end)
(* get the size of a file quickly *)
val file_get_size : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
'impl -> 'file_ref -> nat
let file_get_size ops s0 i0_ref = (
let (_, ret) = ops.fops_read s0 i0_ref in
let bs = dest_RV_bytes ret in
let len_bs = T_list_array.dim bs in
len_bs
)
(* [parent_dir_of_res_name] tries to return the parent directory of
the resolved name. For [RN_error] and the root directory,
[Nothing] is returned. *)
val parent_dir_of_res_name : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
'impl ->
res_name 'dir_ref 'file_ref ->
maybe 'dir_ref
let parent_dir_of_res_name ops s0 rn = (match rn with
| RN_file (d0_ref, _, _, _) -> Just d0_ref
| RN_none (d0_ref, _, _) -> Just d0_ref
| RN_error _ -> Nothing
| RN_dir (d0_ref, rpd) -> (
match (ops.fops_get_parent s0 d0_ref) with
| Nothing -> Nothing (* src is the root dir, catched by subdir check *)
| Just (d1_ref, _) -> Just d1_ref
end)
end)
#ifdef aspect_perms
val res_name_has_restricted_delete_privilege : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
'impl ->
res_name 'dir_ref 'file_ref ->
bool
let res_name_has_restricted_delete_privilege env s0 rn = begin
let arch = architecture_of_ty_arch env.env_arch in
let arch_allows_removing_writable = arch.arch_allows_removing_from_protected_dir_if_writeable in
match rn with
| RN_file (d0_ref, _, i0_ref, _) ->
(env.env_prms.cp_has_file_restricted_delete_privilege arch_allows_removing_writable s0 d0_ref i0_ref)
| RN_dir (d0_ref, _) -> (
match (env.env_ops.fops_get_parent s0 d0_ref) with
| Nothing -> true (* src is the root dir, we can't do anything, better return true to be conservative *)
| Just (d1_ref, _) ->
(env.env_prms.cp_has_dir_restricted_delete_privilege arch_allows_removing_writable s0 d1_ref d0_ref)
end)
| _ -> true (* we can't check, because there is no source file *)
end
end
#endif
(* mac os x non-POSIX behaviour on symlinks to files with a trailing slash *)
let mac_os_x_map_rpath env s0 rpath = (
match is_mac_os_x_arch env with
| false -> rpath
| true -> (
match rpath with
| RN_error(ENOTDIR,<|re_cwd=cwd;re_nl=Just nl;re_rn=Just fopt|>) -> (
let path = CS_Some(Resolve.ty_name_list_to_string nl) in
let b = Resolve.res_name_is_symlink env.env_ops s0 (Resolve.process_path_no_follow_no_trailing_slash env s0 cwd path) in
if b then fopt else rpath)
| _ -> rpath end) end)
(*--------------------------*)
(* link *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_link_checks_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_link_checks_perms env spath dpath = (
fsm_get_state >>= fun s0 ->
match dpath with
| RN_none (d0_ref,n,rp) -> (fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref))) (* posix/link.md EACCES:2 *)
| _ -> fsm_do_nothing end)
#endif
val fsop_link_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_link_checks env spath dpath = (
fsm_get_state >>= fun s0 ->
(* sanity check spath in parallel with dpath *)
( match dpath with
| RN_error(e,<|re_rn=fopt|>) -> (
fsm_cond_raises [
(e,true);
(EEXIST, is_linux_arch env && isJust fopt && (e = ENOTDIR)); (* tr/23 probable non-POSIX Linux behaviour (path should not resolve) *) (* coverage:mac_os_x:posix:irrelevant *)
(EEXIST, is_mac_os_x_arch env && isJust fopt && (e = ENOTDIR)) (* tr/27 apparent non-POSIX behaviour - symlink is followed but a different error results *) (* coverage:linux:posix:irrelevant *)
])
| RN_file _ -> (fsm_raise EEXIST) (* posix/link.md EEXIST:1 *)
| RN_dir _ -> (fsm_raise EEXIST) (* posix/link.md EEXIST:1 *)
| RN_none (d0_ref,n,rp) -> (
let cwd = rp.rp_cwd in
let nl = rp.rp_nl in
let path = CS_Some(Resolve.ty_name_list_to_string nl) in
let b0 = Resolve.res_name_is_symlink env.env_ops s0 (Resolve.process_path_no_follow_no_trailing_slash env s0 cwd path) in
(if (is_linux_arch env || (is_mac_os_x_arch env && not b0)) && rn_ends_with_slash dpath then
fsm_raise ENOENT (* tr/24, mac hfsplus_loop/link/results/check_exec_link___link_nonempty_dir2__f2.txt___nonexist_2__-int.trace *)
else
fsm_do_nothing)
||| ((* a symlink to a non-existing entry on mac is treated as though the path resolved to the symlink itself hfsplus_loop/link/results/check_exec_link___link_empty_dir1_____nonempty_dir1__d2__sl_dotdot_no_such_target-int.trace *)
if is_mac_os_x_arch env && b0 && not (rn_ends_with_slash dpath) then fsm_raise EEXIST else fsm_do_nothing))
end
) ||| (
match spath with
| RN_error(e,_) -> (fsm_raise e)
| RN_none _ -> (fsm_raise ENOENT) (* posix/link.md ENOENT:2 *)
| RN_file _ -> (
let cond = is_linux_arch env && Resolve.res_name_is_symlink env.env_ops s0 spath && rn_ends_with_slash spath in (* coverage:mac_os_x:posix:irrelevant *)
fsm_cond_raises
[(ENOTDIR, (is_RN_none dpath && rn_ends_with_slash dpath && (not (is_mac_os_x_arch env)))); (* posix/link.md ENOTDIR:4 hfsplus_loop/link/results/check_exec_link___link_nonempty_dir1__d2__f3.txt___nonempty_dir1__d2__sl_dotdot_no_such_target__-int.trace *)
(ENOTDIR, cond); (* FIXME tr/?? *)
(EPERM, cond); (* FIXME tr/?? *)
(ENOENT, cond)]) (* FIXME tr/?? *)
| RN_dir(d0_ref, _) -> (
(* FIXME we should check link /a/exist_dir /b/f1.txt/ *)
#ifdef aspect_perms
if (env.env_prms.cp_has_dir_link_create_privilege s0 d0_ref &&
arch_allows_dir_links env) then
#else
if (arch_allows_dir_links env) then
#endif
fsm_special FIXME "link: directory links unsupported in this spec" (* coverage:impossible *)
else
fsm_raise EPERM) (* posix/link.md EPERM:2 *)
end)
#ifdef aspect_perms
||| fsop_link_checks_perms env spath dpath
#endif
)
val fsop_link_core : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_link_core env spath dpath = (
fsm_get_state >>= fun s0 ->
(match (spath, dpath) with
| (RN_file(_,_,i0_ref,_), RN_none(d0_ref, n, _)) -> (
let s0 = env.env_ops.fops_link_file s0 i0_ref d0_ref n in
fsm_put_state s0)
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end))
(* posix/1 *)
val fsop_link : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_link env spath dpath = (fsm_get_state >>= (fun s0 ->
let spath = (if (is_mac_os_x_arch env) then (mac_os_x_map_rpath env s0 spath) else spath) in
fsop_link_checks env spath dpath >>= (fun _ -> fsop_link_core env spath dpath)))
(*--------------------------*)
(* mkdir *)
(*--------------------------*)
#ifdef aspect_perms
let fsop_mkdir_checks_perms env rpath mode = fsm_get_state >>= fun s0 ->
(fsm_cond_special Implementation_defined "mkdir: additional file permission bits"
(contains_implementation_specific_file_perms mode)
) |||
(match rpath with
| RN_none(d0_ref,n,_) -> (
fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref))) (* posix/mkdir.md EACCES:2 *)
| _ -> fsm_do_nothing
end)
#endif
let fsop_mkdir_checks env rpath mode =
(match rpath with
| RN_none(d0_ref,n,_) -> fsm_do_nothing
| RN_error(e,<|re_rn=fopt|>) ->
fsm_cond_raises [
(e, true);
(ENOENT, e = ENOTDIR); (* posix/mkdir.md ENOENT:4; probable POSIX spec error; confirmed on austin group mailing list 2014-06-16 by Geoff Clare *)
(EEXIST, is_linux_arch env && isJust fopt && (e = ENOTDIR)); (* tr/22 FIXME check other places where we have ENOTDIR because last component is /f1.txt/ - we need to add isJust check *) (* coverage:mac_os_x:posix:irrelevant *)
(EEXIST, is_mac_os_x_arch env && isJust fopt && (e = ENOTDIR)) (* tr/26 apparent non-posix behaviour - symlink is followed but a different error results *) (* coverage:linux:posix:irrelevant *)
]
| RN_dir _ -> (fsm_raise EEXIST) (* posix/mkdir.md EEXIST:1 *)
| RN_file _ -> (fsm_raise EEXIST) (* posix/mkdir.md EEXIST:1 *)
end
)
#ifdef aspect_perms
|||
(* additionally check for permissions *)
(fsop_mkdir_checks_perms env rpath mode)
#endif
#ifdef aspect_perms
(* mkdir_core_perms is the permission concerned part of mkdir. It sets
the correct permissions and owner for the new directory. *)
let fsop_mkdir_core_perms env mode s1 d0_ref d1_ref =
(* set the permissions of new dir *)
let mode' = unset_file_perms mode (env.env_prms.cp_get_umask s1) in
let s2 = env.env_perm_ops.pops_set_perm_dir s1 mode' d1_ref in
(* set owner of the new file *)
let arch = architecture_of_ty_arch env.env_arch in
let new_uid = env.env_prms.cp_get_euid () in
let new_gid = if arch.arch_group_from_parent_dir then
(* inherit group from parent directory d0_ref *)
(env.env_ops.fops_stat_dir s2 d0_ref).st_gid (* coverage:impossible -no architecture has this field set to true *)
else
(* use effective group id of process *)
env.env_prms.cp_get_egid ()
in
let s3 = env.env_perm_ops.pops_chown_dir s2 (new_uid, new_gid) d1_ref in
s3
#endif
let fsop_mkdir_core env rpath mode =
fsm_get_state >>= (fun s0 ->
(match rpath with
| RN_none(d0_ref,n,_) -> (
(* create the new directory and get a reference to it back *)
let (s1, d1_ref) = env.env_ops.fops_mkdir s0 d0_ref n in
#ifdef aspect_perms
let s1 = fsop_mkdir_core_perms env mode s1 d0_ref d1_ref in (* update permissions and owner of new directory *)
#endif
fsm_put_state s1)
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end))
val fsop_mkdir : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
file_perm ->
fsmonad 'impl ret_value
let fsop_mkdir env rpath mode =
(fsop_mkdir_checks env rpath mode >>= (fun _ -> fsop_mkdir_core env rpath mode))
(*--------------------------*)
(* open *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_open_checks_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref ->
finset open_flag -> maybe file_perm -> fsmonad 'impl ret_value
let fsop_open_checks_perms env rpath oflags mode = (fsm_get_state >>= fun s0 ->
(* check for posix/open.md EACCES:2 *)
( match rpath with
| RN_file (_,_,i0_ref,_) -> (fsm_get_state >>= (fun s0 -> (
let o_exec_ok = (finset_mem O_EXEC oflags --> env.env_prms.cp_has_file_execute_permission s0 i0_ref) in (* coverage:linux:irrelevant *)
let o_rdonly_ok = (finset_mem O_RDONLY oflags --> env.env_prms.cp_has_file_read_permission s0 i0_ref) in
let o_rdwr_ok = (finset_mem O_RDWR oflags --> (env.env_prms.cp_has_file_read_permission s0 i0_ref &&
env.env_prms.cp_has_file_write_permission s0 i0_ref)) in
let o_wronly_ok = (finset_mem O_WRONLY oflags --> env.env_prms.cp_has_file_write_permission s0 i0_ref) in
let o_trunc_ok = (finset_mem O_TRUNC oflags --> env.env_prms.cp_has_file_write_permission s0 i0_ref) in (* posix/open.md EACCES:4 *)
fsm_cond_raise EACCES (not (o_exec_ok && o_rdonly_ok && o_rdwr_ok && o_wronly_ok && o_trunc_ok))
)))
| RN_dir (d0_ref,_) -> (fsm_get_state >>= (fun s0 -> (
let o_search_ok = (finset_mem O_SEARCH oflags --> env.env_prms.cp_has_dir_search_permission s0 d0_ref) in (* coverage:linux:irrelevant *)
let o_rdonly_ok = (finset_mem O_RDONLY oflags --> env.env_prms.cp_has_dir_read_permission s0 d0_ref) in
(* write permissions on dirs don't make sense and whether permission is granted or not,
EISDIR:1 is raised anyhow. *)
let o_rdwr_ok = (finset_mem O_RDWR oflags --> (env.env_prms.cp_has_dir_read_permission s0 d0_ref &&
env.env_prms.cp_has_dir_write_permission s0 d0_ref)) in
let o_wronly_ok = (finset_mem O_WRONLY oflags --> env.env_prms.cp_has_dir_write_permission s0 d0_ref) in
fsm_cond_raise EACCES (not (o_search_ok && o_rdonly_ok && o_rdwr_ok && o_wronly_ok))
)))
| _ -> fsm_do_nothing (* only check for existing files *)
end
)
|||
(match rpath with
| RN_none(d0_ref,n,ns) -> if (finset_mem O_CREAT oflags) then
(* check that mode is OK *)
( (fsm_cond_special
Undefined "open: extra permissions bit for newly created file"
(isJust mode && (contains_implementation_specific_file_perms (fromJust mode))))
|||
(fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref))) (* posix/open.md EACCES:3 *)
)
else fsm_do_nothing
| _ -> fsm_do_nothing
end))
#endif
val fsop_open_checks_flags : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref ->
finset open_flag -> maybe file_perm -> fsmonad 'impl ret_value
let fsop_open_checks_flags env rpath oflags mode_opt = (
(
(if (is_linux_arch env || is_mac_os_x_arch env) then fsm_do_nothing else (* tr/15 *) (* hfsplus_loop/open/results/check_exec_open___open_nonexist_dir__nonexist2___O_EXCL__O_WRONLY___none___close_3-int.trace *)
(fsm_cond_special Undefined "open: O_EXCL, no O_CREAT, posix/open.md D:1" (* coverage:linux:irrelevant *)
((finset_mem O_EXCL oflags) && (* coverage:linux:irrelevant *)
not ( (* coverage:linux:irrelevant *) finset_mem O_CREAT oflags)))) (* coverage:linux:irrelevant *)
|||
(if is_linux_arch env then fsm_do_nothing else (* tr/16 note this leads to the file being truncated even though the file was opened O_RDONLY FIXME very strange behaviour *) (* coverage:mac_os_x:posix:irrelevant *)
if is_mac_os_x_arch env then fsm_do_nothing else (* exec_open___open_broken_sl_____O_APPEND__O_CLOEXEC__O_CREAT__O_DIRECTORY__O_EXCL__O_EXEC__O_NOFOLLOW__O_TRUNC___0666___close_3-int.trace *)
(fsm_cond_special (* coverage:linux:irrelevant *)
Undefined "open: O_TRUNC, no O_RDWR or O_WRONLY, posix/open.md O_TRUNC:4" (* coverage:linux:irrelevant *)
(( (* coverage:linux:irrelevant *)finset_mem O_TRUNC oflags) && (* coverage:linux:irrelevant *)
not ( (* coverage:linux:irrelevant *) finset_mem O_RDWR oflags || (* coverage:linux:irrelevant *)
(* coverage:linux:irrelevant *) finset_mem O_WRONLY oflags)))) (* coverage:linux:irrelevant *)
|||
(* check that exactly one file access mode is provided *)
(if is_linux_arch env then fsm_do_nothing else (* tr/17 FIXME confirm that this is treated as O_RDWR not O_RDONLY *) (* coverage:mac_os_x:posix:irrelevant *)
(fsm_cond_special Undefined "open: not exactly one file access mode" (* coverage:linux:irrelevant *)
(not (open_flag_set_access_mode_ok oflags))))
|||
(if is_mac_os_x_arch env && finset_mem O_CREAT oflags && finset_mem O_DIRECTORY oflags then
fsm_raise EINVAL (* FIXME this may be too loose; does Mac always return EINVAL in this situation? *)
else
fsm_do_nothing)
)
)
val fsop_open_checks_rpath : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref ->
finset open_flag -> maybe file_perm -> fsmonad 'impl ret_value
let fsop_open_checks_rpath env rpath oflags mode_opt = (fsm_get_state >>= fun s0 ->
(* RN_error *)
(match rpath with
| RN_error (e,_) -> (fsm_raise e)
| _ -> fsm_do_nothing
end)
|||
(* RN_none *)
(match rpath with
| RN_none _ -> (fsm_cond_raise ENOENT (not (finset_mem O_CREAT oflags))) (* posix/open.md ENOENT:1 *)
| _ -> fsm_do_nothing
end)
|||
(* RN_dir *)
(fsm_cond_raise EISDIR ((finset_mem O_RDWR oflags || finset_mem O_WRONLY oflags) && is_RN_dir rpath))
(* posix/open.md EISDIR:1 *)
|||
(let cond = ((finset_mem O_TRUNC oflags) && (is_RN_dir rpath)) in
if cond && (is_linux_arch env || is_mac_os_x_arch env) then fsm_raise EISDIR else (* tr/19 hfsplus_loop/open/results/check_exec_open___open_nonempty_dir___O_TRUNC__O_WRONLY___none___close_3-int.trace *)
(fsm_cond_special
Implementation_defined "open: O_TRUNC, directory, posix/open.md O_TRUNC:3")
cond)
|||
(if is_linux_arch env then fsm_do_nothing else (* NB Linux has no O_EXEC flag so this case cannot arise *) (* coverage:mac_os_x:posix:irrelevant *)
(fsm_cond_special (* coverage:linux:irrelevant *)
Unspecified "open: O_EXEC on directory" (* posix/open.md O_EXEC:1 *) (* coverage:linux:irrelevant *)
( (* coverage:linux:irrelevant *) finset_mem O_EXEC oflags (* coverage:linux:irrelevant *)
&& (is_RN_dir rpath)))) (* coverage:linux:irrelevant *)
|||
(* RN_file *)
(let cond = (finset_mem O_DIRECTORY oflags && is_RN_file rpath) in
(fsm_cond_raise ENOTDIR cond)) (* posix/open.md ENOTDIR:1 *)
|||
(if is_linux_arch env then fsm_do_nothing else (* FIXME glibc on Linux has no O_SEARCH flag, so this case cannot arise *) (* coverage:mac_os_x:posix:irrelevant *)
(fsm_cond_special (* coverage:linux:irrelevant *)
Unspecified "open: O_SEARCH on non-directory" (* posix/open.md O_SEARCH:1 *) (* coverage:linux:irrelevant *)
( (* coverage:linux:irrelevant *) finset_mem O_SEARCH oflags (* coverage:linux:irrelevant *)
&& (is_RN_file rpath)))) (* coverage:linux:irrelevant *)
|||
fsm_cond_raise ELOOP (finset_mem O_NOFOLLOW oflags && Resolve.res_name_is_symlink env.env_ops s0 rpath) (* posix/open.md ELOOP:1 FIXME but for open, path resolution always follows symlinks, so this condition never arises? FIXME look at tests for this; mac non-posix behaviour hfsplus_loop/open/results/check_exec_open___open_f3_sl.txt___O_NOFOLLOW__O_WRONLY___none___close_3-int.trace *)
|||
(* O_CREAT *)
(fsm_cond_raise EEXIST (finset_mem O_EXCL oflags && finset_mem O_CREAT oflags
&& (is_RN_dir rpath || is_RN_file rpath))) (* posix/open.md EEXIST:1 *)
|||
(fsm_cond_raise ENOTDIR (finset_mem O_CREAT oflags && rn_ends_with_slash rpath && not(is_mac_os_x_arch env) )) (* posix/open.md ENOTDIR:2 open cannot be used to create a directory (implicit in posix spec), but this arises even if the directory exists; mac non-posix behaviour hfsplus_loop/open/results/check_exec_open___open_nonempty_dir_____O_CREAT__O_SEARCH___0666___close_3-int.trace *)
|||
(fsm_cond_raise EISDIR (is_linux_arch env && finset_mem O_CREAT oflags && (is_RN_dir rpath || rn_ends_with_slash rpath))) (* tr/21 FIXME possible non-posix Linux behaviour *) (* coverage:mac_os_x:posix:irrelevant *)
|||
(fsm_cond_raise ENOENT (
finset_mem O_CREAT oflags && rn_ends_with_slash rpath &&
(is_RN_none rpath || is_RN_error rpath) &&
not (
is_mac_os_x_arch env &&
(match rpath with
| RN_none(d0_ref,n,rp) -> (
let cwd = rp.rp_cwd in
let nl = rp.rp_nl in
let path = CS_Some(Resolve.ty_name_list_to_string nl) in
let b = Resolve.res_name_is_symlink env.env_ops s0 (Resolve.process_path_no_follow_no_trailing_slash env s0 cwd path) in
b)
| _ -> false end)) (* hfsplus_loop/open/results/check_exec_open___open_broken_sl_____O_CREAT__O_WRONLY___0666___close_3-int.trace *)
)) (* posix/open.md ENOENT:3 *)
|||
(if is_linux_arch env then fsm_do_nothing else (* FIXME 2118 see adhoc_open_tests/adhoc_open_test.posix_result in this case, Linux creates a file ---x------ ; is this always the case? could Linux create a file with different permissions e.g. depending on group membership etc? *) (* coverage:mac_os_x:posix:irrelevant *)
(fsm_cond_special FIXME "open with create-flag but without mode argument" (* coverage:linux:irrelevant *)
( (* coverage:linux:irrelevant *) finset_mem O_CREAT oflags && (* coverage:linux:irrelevant *)
is_RN_none rpath && (* coverage:linux:irrelevant *)
isNothing mode_opt))) (* coverage:linux:irrelevant *)
)
val fsop_open_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref ->
int_open_flags -> maybe file_perm -> fsmonad 'impl ret_value
let fsop_open_checks env rpath oflag mode_opt =
let arch = architecture_of_ty_arch env.env_arch in
let oflags = arch.arch_open_flags_of_int oflag in (
fsop_open_checks_rpath env rpath oflags mode_opt
|||
fsop_open_checks_flags env rpath oflags mode_opt
#ifdef aspect_perms
|||
fsop_open_checks_perms env rpath oflags mode_opt
#endif
)
#ifdef aspect_perms
val fsop_open_core_create_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref ->
file_perm -> 'dir_ref -> 'file_ref -> 'impl -> 'impl
let fsop_open_core_create_perms env rpath mode d0_ref i0_ref s1 =
(* set the permissions of new file *)
let mode' = unset_file_perms mode (env.env_prms.cp_get_umask s1) in
let s2 = env.env_perm_ops.pops_set_perm_file s1 mode' i0_ref in
(* set owner of the new file *)
let arch = architecture_of_ty_arch env.env_arch in
let new_uid = env.env_prms.cp_get_euid () in
let new_gid = if arch.arch_group_from_parent_dir then
(* inherit group from parent directory d0_ref *)
(env.env_ops.fops_stat_dir s2 d0_ref).st_gid (* coverage:impossible -group inheritance unsupported by the existing architectures*)
else
(* use effective group id of process *)
env.env_prms.cp_get_egid ()
in
let s3 = env.env_perm_ops.pops_chown_file s2 (new_uid, new_gid) i0_ref in
s3
#endif
val fsop_open_core_create_if_not_exists : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref ->
maybe file_perm -> fsmonad 'impl (entry 'dir_ref 'file_ref)
let fsop_open_core_create_if_not_exists env rpath mode_opt =
(match rpath with
| RN_error _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
| RN_dir(d0_ref,rp)-> fsm_return (Dir_ref_entry d0_ref) (* we can open a dir *)
| RN_file(d0_ref,n,i0_ref,rp) -> fsm_return (File_ref_entry i0_ref)
| RN_none(d0_ref,n,ns) -> (
let mode_opt = (match mode_opt with
| Nothing -> (if is_linux_arch env (* coverage:mac_os_x:posix:irrelevant - this if is never checked for non-linux architectures for there is a check for the O_CREAT flag earlier *)
then (Just (File_perm 0O101)) (* coverage:mac_os_x:posix:irrelevant *)
else Nothing) (* FIXME Linux called with no mode, but with O_CREAT, creates the file see fs_test/adhoc_open_test.posix_result; see also FIXME 2118 *) (* coverage:impossible -the absence of permissions for non-linux is checked before in fsop_open_checks for O_CREAT *)
| Just _ -> mode_opt end)
in
match mode_opt with
| Nothing -> (fsm_special Impossible "error raised before") (* coverage:impossible *)
| Just mode -> (fsm_get_state >>= (fun s0 ->
(* We are sure we want to create a new regular file,
since if we tried to open a directory, we would have run into an error above. *)
let (s1,i0_ref) = env.env_ops.fops_mkfile s0 d0_ref n in
#ifdef aspect_perms
let s1 = fsop_open_core_create_perms env rpath mode d0_ref i0_ref s1 in
#endif
fsm_put_state_return s1 (File_ref_entry i0_ref)))
end)
end)
val fsop_open_core_truncate : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref ->
int_open_flags -> entry 'dir_ref 'file_ref ->
fsmonad 'impl (entry 'dir_ref 'file_ref * finset open_flag)
let fsop_open_core_truncate env rpath oflag entry = (
fsm_get_state >>= (fun s0 -> (
let arch = architecture_of_ty_arch env.env_arch in
let oflags = arch.arch_open_flags_of_int oflag in
(* truncate if necessary; at this point, rpath can only be a file. *)
if finset_mem O_TRUNC oflags then (match entry with
| Dir_ref_entry _ -> (fsm_special Impossible "error raised before") (* coverage:impossible *)
| File_ref_entry i0_ref -> (
let zero_bytes = T_list_array.of_string "" in (* FIXME define elsewhere? *)
let s0 = env.env_ops.fops_write s0 i0_ref zero_bytes in
fsm_put_state_return s0 (entry,oflags))
end) else
fsm_return (entry, oflags)
)))
val fsop_open_core : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref ->
int_open_flags -> maybe file_perm -> fsmonad 'impl (entry 'dir_ref 'file_ref * finset open_flag)
let fsop_open_core env rpath oflag mode_opt = (
fsop_open_core_create_if_not_exists env rpath mode_opt >>= (fun entry ->
fsop_open_core_truncate env rpath oflag entry >>= (fun (entry, oflags) ->
fsm_return (entry, oflags))))
val fsop_open : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
int_open_flags ->
maybe file_perm ->
fsmonad 'impl (entry 'dir_ref 'file_ref * finset open_flag)
let fsop_open env rpath oflag mode = (fsm_get_state >>= (fun s0 ->
let rpath = if (is_mac_os_x_arch env) then (mac_os_x_map_rpath env s0 rpath) else rpath in
fsop_open_checks env rpath oflag mode >>= (fun _ ->
fsop_open_core env rpath oflag mode)))
(*--------------------------*)
(* open_close *)
(*--------------------------*)
val fsop_open_close_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
int_open_flags ->
maybe file_perm ->
fsmonad 'impl ret_value
let fsop_open_close_checks env rpath oflag mode = fsop_open_checks env rpath oflag mode
val fsop_open_close_core : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
int_open_flags ->
maybe file_perm ->
fsmonad 'impl ret_value
let fsop_open_close_core env rpath oflag mode =
(fsop_open_core env rpath oflag mode >>= (fun _x_ -> fsm_return RV_none))
val fsop_open_close : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
int_open_flags ->
maybe file_perm ->
fsmonad 'impl ret_value
let fsop_open_close env rpath oflag mode = (
fsop_open_close_checks env rpath oflag mode >>= (fun _ ->
fsop_open_close_core env rpath oflag mode
))
(*--------------------------*)
(* pread *)
(*--------------------------*)
(* reading is split into two functions
fsop_pread works with an entry - this is what is available when using read at the OS level with a file descriptor
fsop_pread_rn is really just a dummy function to allow fsop_pread to be called; we need to provide some way to read from a resolved name (e.g. for linking with fuse, or if we are discarding the os level stuff)
any permissions checks should work on pre_fs_read, not read
*)
val fsop_pread_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
entry 'dir_ref 'file_ref ->
nat -> off_t ->
fsmonad 'impl ret_value
let fsop_pread_checks env entry len ofs = (
fsm_cond_raise EINVAL (ofs < 0) (* posix/read.md EINVAL:2 *)
|||
((* check we read a regular file *)
match entry with
| Dir_ref_entry _ -> (
(* FIXME we should check link /a/exist_dir /b/f1.txt/ *)
let arch = architecture_of_ty_arch env.env_arch in
if arch.arch_allows_dir_read then
fsm_special FIXME "read: directory reads unsupported in this spec" (* coverage:impossible *)
else
fsm_raise EISDIR) (* posix/read.md EISDIR:1 *)
| File_ref_entry i0_ref -> fsm_do_nothing
end
))
val fsop_pread_core : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
entry 'dir_ref 'file_ref ->
nat -> off_t ->
fsmonad 'impl ret_value
let fsop_pread_core env entry len ofs = (fsm_get_state >>= (fun s0 -> (match entry with
| Dir_ref_entry _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
| File_ref_entry i0_ref -> (
let ofs = (natFromInt ofs) in
let (s1, res) = env.env_ops.fops_read s0 i0_ref in
(fsm_put_state s1) >>= (fun _x_ ->
let bs = dest_RV_bytes res in
let len_bs = T_list_array.dim bs in
let len_max = if ofs+len <= len_bs then len else len_bs - ofs in
(* non-deterministically choose the amount of data to read,
if an interrupt occurs during reading or when reading from a FIFO
that is has not enough data yet, read might not read up to the given length. *)
(fsm_choose_nat len_max) >>= (fun len_to_read ->
let bs' = T_list_array.sub bs ofs len_to_read in
fsm_return (RV_bytes(bs')))
))
end)))
(* Notice that pre_fs_read does not perform any checks for permissions.
This is done by the calling functions, fs_read and os_read. *)
val fsop_pread : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
entry 'dir_ref 'file_ref ->
nat -> off_t ->
fsmonad 'impl ret_value
let fsop_pread env entry len ofs = (
fsop_pread_checks env entry len ofs >>= (fun _ ->
fsop_pread_core env entry len ofs))
(*--------------------------*)
(* pread with resolved name *)
(*--------------------------*)
(* note that these definitions are just placeholders - pre_fs_read is the real spec *)
#ifdef aspect_perms
val fsop_pread_rn_checks_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
nat -> off_t ->
fsmonad 'impl ret_value
let fsop_pread_rn_checks_perms env rn len ofs = (fsm_get_state >>= fun s0 -> (* coverage:unused *)
(match rn with
| RN_dir (d0_ref, _) ->
fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_read_permission s0 d0_ref)) (* guessing here *) (* coverage:unused *)
| RN_file(_,_,i0_ref,_) ->
fsm_cond_raise EACCES (not (env.env_prms.cp_has_file_read_permission s0 i0_ref)) (* guessing here *) (* coverage:unused *)
| _ -> fsm_do_nothing (* coverage:unused *)
end))
#endif
val fsop_pread_rn_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
nat -> off_t ->
fsmonad 'impl ret_value
let fsop_pread_rn_checks env rn len ofs = (
(fsm_cond_raise EINVAL (ofs < 0)) (* coverage:unused *)
|||
(match rn with
| RN_dir (d0_ref, _) -> fsop_pread_checks env ((Dir_ref_entry d0_ref):entry 'dir_ref 'file_ref) len ofs (* coverage:unused *)
| RN_file(_,_,i0_ref,_) ->
fsop_pread_checks env ((File_ref_entry i0_ref):entry 'dir_ref 'file_ref) len ofs (* coverage:unused *)
| RN_none _ -> (fsm_raise ENOENT) (* coverage:unused *)
| RN_error (e,_) -> (fsm_raise e) (* coverage:unused *)
end)
#ifdef aspect_perms
||| fsop_pread_rn_checks_perms env rn len ofs
#endif
)
val fsop_pread_rn_core : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
nat -> off_t ->
fsmonad 'impl ret_value
let fsop_pread_rn_core env rn ofs len =
(match rn with
| RN_dir (d0_ref, _) ->
fsop_pread_core env ((Dir_ref_entry d0_ref):entry 'dir_ref 'file_ref) ofs len (* coverage:unused *)
| RN_file(_,_,i0_ref,_) ->
fsop_pread_core env ((File_ref_entry i0_ref):entry 'dir_ref 'file_ref) ofs len (* coverage:unused *)
| _ -> fsm_special Impossible "error raised before" (* coverage:unused *)
end)
(* FIXME the real spec would allow reading less than all the bytes; recall len is maxlen *)
(* fsop_pread using a resolved name and an *)
val fsop_pread_rn : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
nat -> off_t ->
fsmonad 'impl ret_value
let fsop_pread_rn env rn len ofs = (
fsop_pread_rn_checks env rn len ofs >>= (fun _ -> (* coverage:unused *)
fsop_pread_rn_core env rn len ofs) (* coverage:unused *))
(*--------------------------*)
(* opendir *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_opendir_checks_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_opendir_checks_perms env rn = (fsm_get_state >>= (fun s0 ->
(match rn with
RN_dir(d0_ref,_) -> (fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_read_permission s0 d0_ref))) (* posix/opendir.md EACCES:2 *)
| _ -> fsm_do_nothing
end)))
#endif
val fsop_opendir_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_opendir_checks env rn = (
(match rn with
| RN_error (e,_) -> (fsm_raise e)
| RN_none _ -> (fsm_raise ENOENT) (* posix/opendir.md ENOENT:1 *)
| RN_file _ -> (fsm_raise ENOTDIR) (* posix/opendir.md ENOTDIR:1 *)
| RN_dir(d0_ref,rp) -> fsm_do_nothing
end)
#ifdef aspect_perms
|||
fsop_opendir_checks_perms env rn
#endif
)
val fsop_opendir_core : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl 'dir_ref
let fsop_opendir_core env rn = (
match rn with
| RN_dir(d0_ref,rp) -> fsm_return d0_ref
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end
)
val fsop_opendir : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl 'dir_ref
let fsop_opendir env rn = (
fsop_opendir_checks env rn >>= (fun _ ->
fsop_opendir_core env rn))
(*--------------------------*)
(* rename *)
(*--------------------------*)
(* NB later we may want to also return a state, given access times can cause changes when reading etc *)
(* FIXME surely a lot of this complexity is because this is the user land behaviour of the mv command - but we want to target the syscall interface *)
(* FIXME rename to subdir of self? *)
(* posix/rename.md *)
val fsop_rename_checks_rsrc_rdst : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rename_checks_rsrc_rdst env rsrc rdst = (fsm_get_state >>= (fun s0 -> (
(fsm_cond_raise ENOENT (is_RN_none rsrc)) (* no src file; posix/rename.md ENOENT:1 *)
|||
(match rsrc with
| RN_error (e,_) -> fsm_raise e (* tr/2 *)
| _ -> fsm_do_nothing
end)
|||
(match rdst with
| RN_error (e,_) -> fsm_raise e (* tr/1 *)
| _ -> fsm_do_nothing
end)
|||
(* renaming files into non-files *)
(fsm_cond_raise EISDIR (is_RN_file rsrc && is_RN_dir rdst)) (* posix/rename.md EISDIR:1 *)
|||
(fsm_cond_raise ENOTDIR (is_RN_file rsrc && is_RN_none rdst && rn_ends_with_slash rdst && not (is_mac_os_x_arch env)))
(* tr/3 similar to tr/5; posix/rename.md ENOTDIR:4
2014-10-27_mJ4/hfsplus_loop/rename/results/check_exec_rename___rename_nonempty_dir1__d2__f3.txt___nonempty_dir1__d2__sl_dotdot_no_such_target__-int.trace
rename "nonempty_dir1/d2/f3.txt"
"nonempty_dir1/d2/sl_dotdot_no_such_target/" gives RV_none, mac_os_x
non-posix behaviour ignores trailing slash when going via a symlink *)
|||
(fsm_cond_raise ENOENT (is_RN_file rsrc && is_RN_none rdst && rn_ends_with_slash rdst && is_mac_os_x_arch env
&& not (
let rp = (match rdst with | RN_none(_,_,rp) -> rp end) in
let cwd = rp.rp_cwd in
let path = CS_Some(Resolve.ty_name_list_to_string rp.rp_nl) in
Resolve.res_name_is_symlink env.env_ops s0 (Resolve.process_path_no_follow_no_trailing_slash env s0 cwd path)))) (* hfsplus_loop/rename/results/check_exec_rename___rename_nonempty_dir1__d2__f3.txt___nonempty_dir1__nonexist_4__-int.trace hfsplus_loop/rename/results/check_exec_rename___rename_nonempty_dir1__d2__f3.txt___nonempty_dir1__d2__sl_dotdot_no_such_target__-int.trace
: the path "nonempty_dir1/nonexist_4/" is treated differently to "nonempty_dir1/d2/sl_dotdot_no_such_target/" *)
|||
(fsm_cond_raise ENOTDIR (is_RN_file rsrc && is_RN_dir rdst && is_linux_arch env && rn_ends_with_slash rdst)) (* coverage:mac_os_x:posix:irrelevant *)
(* tr/5 even if empty; arguably a Linux bug? Confirmed non-posix behaviour *)
|||
(fsm_cond_raise ENOTDIR (is_RN_dir rsrc && (is_RN_file rdst || is_RN_error rdst))) (* posix/rename.md ENOTDIR:2 *)
|||
(fsm_cond_raise ENOTDIR (is_linux_arch env && Resolve.res_name_is_symlink env.env_ops s0 rsrc && rn_ends_with_slash rsrc)) (* coverage:mac_os_x:posix:irrelevant *)
|||
(fsm_cond_raise ENOTDIR (is_linux_arch env && Resolve.res_name_is_symlink env.env_ops s0 rdst && rn_ends_with_slash rdst)) (* coverage:mac_os_x:posix:irrelevant *)
|||
( (* link to a non-empty directory *)
match rdst with
| RN_dir (d0_ref, _) -> (
if (not (dir_is_empty env.env_ops s0 d0_ref)) then
fsm_raises [ENOTEMPTY;EEXIST] (* tr/6 ENOTEMPTY:1 *)
else
fsm_do_nothing)
| _ -> fsm_do_nothing
end
))))
(* attempt to rename root? *)
val fsop_rename_checks_root : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rename_checks_root env rsrc = (fsm_get_state >>= (fun s0 -> (
match rsrc with
| RN_dir (d0_ref, _) -> ( (* attempt to rename root on linux or mac? *)
if (Resolve.is_root_dir env.env_ops s0 d0_ref && (is_linux_arch env || is_mac_os_x_arch env)) then (
fsm_cond_raises [
(EBUSY,true); (* http://fs.dsheets.name/2015-03-15_linux_ext+hfsplus+tmpfs/html/suite/rename/test/adhoc_rename_root-int.trace/index.html#23 ; also on Mac? *)
(EISDIR,is_mac_os_x_arch env)]) (* http://fs.dsheets.name/2015-03-16_osx_hfsplus+fusexmp+sshfs/html/suite/rename/test/adhoc_rename_root-int.trace/index.html#23 *)
else
fsm_do_nothing) (* coverage:linux:mac_os_x:irrelevant *)
| _ -> fsm_do_nothing end)))
(* check that a directory is not renamed into a subdir of itself *)
val fsop_rename_checks_subdir : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rename_checks_subdir env rsrc rdst =
(
let rps_opt = match rsrc with RN_dir (_, rps) -> Just rps | _ -> Nothing end in
let rpd_opt = match rdst with
| RN_dir (_, rpd) -> Just rpd
| RN_file (_, _, _, rpd) -> Just rpd
| RN_none (_, _, rpd) -> Just rpd
| RN_error (e,<|re_rn=Just (RN_file(_,_,_,rpd)) |>) -> Just rpd (* on Linux, this presumably captures rename /tmp/a /tmp/a/f1.txt/ ; FIXME this should only matter on Linux FIXME trace?*)
| RN_error (e,_) -> Nothing
end in
match (rps_opt, rpd_opt) with
| (Just rps, Just rpd) ->
fsm_cond_raise EINVAL (realpath_proper_subdir rps rpd) (* posix/rename.md EINVAL:1 ; similar to tr/7 *)
| _ -> fsm_do_nothing
end
)
val fsop_rename_checks_parentdirs : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rename_checks_parentdirs env rsrc rdst = fsm_get_state >>= (fun s0 -> (
( (* ensure we can get the parent of rsrc *)
(match rsrc with
| RN_dir (d0_ref, _) -> (
(* Hack: This should be impossible because we assume that we can get the parent of every directory
except root. We can't rename the root dir, because the subdir check would fail. However, we don't
enforce that there are no disconnected dirs. So, as a hack, let's raise EINVAL as in the subdir check. *)
fsm_cond_raise EINVAL (isNothing (env.env_ops.fops_get_parent s0 d0_ref))
)
| _ -> fsm_do_nothing
end)
) |||
(* ensure we can get the parent of rdst *)
(match rdst with
| RN_dir (d0_ref, _) -> (
(* Hack: This should be impossible because we assume that we can get the parent of every directory
except root. We can't rename to root dir, as we can only renaming an existing dir to a directory and
because the root is non-empty. However, we don't enforce that there are no disconnected dirs. So, as a hack,
let's raise a proper error. *)
fsm_cond_raises [(ENOTEMPTY, isNothing (env.env_ops.fops_get_parent s0 d0_ref) && is_RN_dir rsrc) (* tr/6 ENOTEMPTY:1 *);
(EEXIST, isNothing (env.env_ops.fops_get_parent s0 d0_ref) && is_RN_dir rsrc) (* tr/6 ENOTEMPTY:1 *)]
)
| _ -> fsm_do_nothing
end)
))
#ifdef aspect_perms
val fsop_rename_checks_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rename_checks_perms env rsrc rdst = fsm_get_state >>= (fun s0 -> (
( (* write permission for dir of rsrc *)
match parent_dir_of_res_name env.env_ops s0 rsrc with
| Nothing -> fsm_do_nothing
| Just d0_ref -> fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref)) (* posix/rename.md EACCES:2 *)
end
) |||
( (* write permission for dir of rdst *)
match parent_dir_of_res_name env.env_ops s0 rdst with
| Nothing -> fsm_do_nothing
| Just d0_ref -> fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref)) (* posix/rename.md EACCES:3 *)
end
) |||
( (* restricted delete/rename permission for dir of rsrc ( posix/rename.md EPERM:1 EACCES:6 ) *)
if res_name_has_restricted_delete_privilege env s0 rsrc then
fsm_do_nothing
else
fsm_raises [EPERM; EACCES] (* posix/rename.md EPERM:1 EACCES:6 *)
) |||
( (* restricted delete/rename permission for dir of rdst ( posix/rename.md EPERM:2 EACCES:7 ) *)
if res_name_has_restricted_delete_privilege env s0 rdst then
fsm_do_nothing
else
fsm_raises [EPERM; EACCES] (* posix/rename.md EPERM:1 EACCES:6 *)
) |||
( (* write permission for dir rsrc *)
match rsrc with
| RN_dir(d0_ref, _) -> fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref)) (* posix/rename.md EACCES:4 *)
| _ -> fsm_do_nothing
end
) |||
( (* write permission for dir rdst *)
match rdst with
| RN_dir(d0_ref, _) -> fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref)) (* posix/rename.md EACCES:5 *)
| _ -> fsm_do_nothing
end
)))
#endif
val fsop_rename_same_rsrc_rdst : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
'impl ->
bool
let fsop_rename_same_rsrc_rdst env rsrc rdst s0 = (match (rsrc, rdst) with
| (RN_file (_,_,i0_ref,_), RN_file (_,_,i1_ref,_)) -> (
if (
(* under linux, eg nonempty_dir1/d2/sl_dotdot_f1.txt/ is not the same as itself!; or rather, we want the checks on paths to occur, so we set this test to fail *)
is_linux_arch env
&& ((Resolve.res_name_is_symlink env.env_ops s0 rsrc && rn_ends_with_slash rsrc) (* coverage:mac_os_x:posix:irrelevant *)
|| (Resolve.res_name_is_symlink env.env_ops s0 rdst && rn_ends_with_slash rdst))) (* coverage:mac_os_x:posix:irrelevant *)
then
false (* coverage:mac_os_x:posix:irrelevant *)
else
(Resolve.res_name_is_symlink env.env_ops s0 rsrc && rn_ends_with_slash rdst)) (* FIXME this isn't right - surely we should check i0_ref and i1_ref - need to see where this breaks the rename tests *)
| (RN_dir (d0_ref,_), RN_dir (d1_ref,_)) ->
(env.env_ops.fops_dir_ref_eq s0 d1_ref d0_ref)
| _ -> false
end)
val fsop_rename_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rename_checks env rsrc rdst = (fsm_get_state >>= (fun s0 ->
if (fsop_rename_same_rsrc_rdst env rsrc rdst s0) then
fsm_do_nothing (* posix/rename.md RENAME:3 *)
else
( fsop_rename_checks_rsrc_rdst env rsrc rdst
|||
fsop_rename_checks_root env rsrc
|||
fsop_rename_checks_subdir env rsrc rdst
|||
fsop_rename_checks_parentdirs env rsrc rdst (* hack to make the invariant that the parent-dirs exist explicit *)
#ifdef aspect_perms
|||
fsop_rename_checks_perms env rsrc rdst
#endif
)
))
val fsop_rename_core : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rename_core env rsrc rdst = (fsm_get_state >>= (fun s0 ->
(match (rsrc, rdst) with
| (RN_file (d0_ref,nsrc,_,_), RN_none (d1_ref, ndst, _)) ->
(* do the move; there is no file ns_dst *)
fsm_put_state (env.env_ops.fops_mvfile s0 d0_ref nsrc d1_ref ndst)
| (RN_file (d0_ref,nsrc,i0_ref,_), RN_file (d1_ref,ndst,i1_ref,_)) -> (
(* do the move; there is a file name ns_dst *)
if (env.env_ops.fops_file_ref_eq s0 i1_ref i0_ref) then
fsm_return RV_none (* tr/4; posix/rename.md RENAME:3 *)
else
fsm_put_state (env.env_ops.fops_mvfile s0 d0_ref nsrc d1_ref ndst))
| (RN_dir (d0_ref,rps), RN_none (d1_ref,ndst,rpd)) ->
(* do the move; there is no file ns_dst *)
let p = env.env_ops.fops_get_parent s0 d0_ref in
(match p with
| Nothing -> (fsm_special Impossible "src was root; can not happen because subdir would be true") (* coverage:impossible*)
| Just(d0_ref,nsrc) -> (
fsm_put_state (env.env_ops.fops_mvdir s0 d0_ref nsrc d1_ref ndst)) end)
| (RN_dir (d0_ref,_), RN_dir (d1_ref,_)) ->
(* if same dir, return silently *)
(if (env.env_ops.fops_dir_ref_eq s0 d1_ref d0_ref) then
(fsm_return RV_none) (* tr/8 posix/rename.md RENAME:3 *)
else
let x = env.env_ops.fops_get_parent s0 d0_ref in
let y = env.env_ops.fops_get_parent s0 d1_ref in
(match (x,y) with
| (Nothing,_) -> (fsm_special Impossible "impossible 1763") (* attempt to rename root; captured by subdir check above *) (* coverage:impossible *)
| (_,Nothing) -> (
fsm_special Impossible "impossible 1765 rename of dir onto root; can not happen because dst must be nonempty") (* coverage:impossible *)
| (Just(d0_ref',nsrc),Just(d1_ref',ndst)) -> (
fsm_put_state (env.env_ops.fops_mvdir s0 d0_ref' nsrc d1_ref' ndst)) end))
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end)))
val fsop_rename : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rename env rsrc rdst = (fsm_get_state >>= (fun s0 ->
let (rsrc,rdst) = if (is_mac_os_x_arch env) then (mac_os_x_map_rpath env s0 rsrc, mac_os_x_map_rpath env s0 rdst) else (rsrc,rdst) in
(fsop_rename_checks env rsrc rdst >>= (fun _ ->
fsop_rename_core env rsrc rdst))))
(*--------------------------*)
(* rmdir *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_rmdir_checks_perms: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
'dir_ref ->
'dir_ref ->
fsmonad 'impl ret_value
let fsop_rmdir_checks_perms env d0_ref d1_ref =
(* we want to remove d0_ref, which lives in dir d1_ref *)
fsm_get_state >>= (fun s0 ->
(fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d1_ref)) (* posix/rmdir.md EACCES:2 *))
|||
(
let arch = architecture_of_ty_arch env.env_arch in
let arch_allows_removing_writable = arch.arch_allows_removing_from_protected_dir_if_writeable in
let delete_ok = (env.env_prms.cp_has_dir_restricted_delete_privilege arch_allows_removing_writable s0 d1_ref d0_ref) in
if delete_ok
then fsm_do_nothing
else fsm_raises [EPERM; EACCES] (* posix/rmdir.md EPERM:1 EACCES:3 *)
))
#endif
val fsop_rmdir_checks: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rmdir_checks env rpath =
fsm_get_state >>= (fun s0 ->
(match rpath with
| RN_file _ -> (fsm_raise ENOTDIR) (* posix/rmdir.md ENOTDIR:1 *)
| RN_none _ -> (fsm_raise ENOENT) (* posix/rmdir.md ENOENT:1 *)
| RN_error (e,_) -> (fsm_raise e)
| RN_dir(d0_ref,_) -> (
(if (not (dir_is_empty env.env_ops s0 d0_ref)) then fsm_raises [ENOTEMPTY;EEXIST] else fsm_do_nothing)
|||
(match (env.env_ops.fops_get_parent s0 d0_ref) with
| Nothing ->
if (is_linux_arch env || is_mac_os_x_arch env)
then
(fsm_raise EBUSY) (* coverage:posix:irrelevant *)
else
fsm_special Implementation_defined (* coverage:linux:mac_os_x:irrelevant *)
"rmdir: attempt to remove root; implementation defined behaviour; may throw EBUSY or remove the root directory; see posix/rmdir.md EBUSY:1" (* FIXME use parameters to isolate implementation-defined behaviour *)
#ifdef aspect_perms
| Just (d1_ref, _) -> fsop_rmdir_checks_perms env d0_ref d1_ref
#else
| Just _ -> fsm_do_nothing
#endif
end))
end))
val fsop_rmdir_core: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rmdir_core env rpath =
fsm_get_state >>= (fun s0 ->
(match rpath with
| RN_dir(d0_ref,_) ->
(match env.env_ops.fops_get_parent s0 d0_ref with
| Nothing -> fsm_special Impossible "error raised before" (* coverage:impossible *)
| Just (d1_ref, n) ->
let s1 = env.env_ops.fops_unlink s0 d1_ref n in
fsm_put_state s1
end)
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end))
val fsop_rmdir: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_rmdir env rpath =
(fsop_rmdir_checks env rpath >>= (fun _ ->
fsop_rmdir_core env rpath))
(*--------------------------*)
(* stat *)
(*--------------------------*)
val fsop_stat_checks : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_stat_checks ops rn =
(match rn with
| RN_error (e,_) -> (fsm_raise e)
| RN_none _ -> (fsm_raise ENOENT)
| _ -> fsm_do_nothing
end)
val fsop_stat_core: forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_stat_core ops rn = (
fsm_get_state >>= (fun s0 -> (
(match rn with
| RN_file(d0_ref,n,i0_ref,rp) -> (fsm_return (RV_stats (ops.fops_stat_file s0 i0_ref)))
| RN_dir(d0_ref,rp) -> (fsm_return (RV_stats (ops.fops_stat_dir s0 d0_ref)))
| _ -> fsm_special Impossible "error raised before" end)))) (* coverage:impossible *)
val fsop_stat: forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_stat ops rn = (
fsop_stat_checks ops rn >>= (fun _ ->
fsop_stat_core ops rn))
(*--------------------------*)
(* lstat *)
(*--------------------------*)
val fsop_lstat: forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_lstat ops rn =
(fsop_stat_checks ops rn >>=
(fun _ -> fsop_stat_core ops rn))
(*--------------------------*)
(* truncate *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_truncate_checks_perms: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> int -> fsmonad 'impl ret_value
let fsop_truncate_checks_perms env rpath len = (fsm_get_state >>= fun s0 ->
(match rpath with
| RN_file(_,_,i0_ref,_) ->
(fsm_cond_raise EACCES (not (env.env_prms.cp_has_file_write_permission s0 i0_ref))) (* posix/truncate.md EACCES:2 *)
| _ -> fsm_do_nothing
end))
#endif
val fsop_truncate_checks: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> int -> fsmonad 'impl ret_value
let fsop_truncate_checks env rpath len = (
(fsm_cond_raise EINVAL (len < 0)) (* posix/truncate.md EINVAL:1 *)
|||
(match rpath with
| RN_error (e,_) -> (fsm_raise e)
| RN_none _ -> (fsm_raise ENOENT) (* posix/truncate.md ENOENT:1 *)
| RN_dir _ -> (fsm_raise EISDIR) (* posix/truncate.md EISDIR:1 *)
| RN_file(_,_,i0_ref,_) -> fsm_do_nothing
end)
#ifdef aspect_perms
|||
(fsop_truncate_checks_perms env rpath len)
#endif
)
val fsop_truncate_core: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> int -> fsmonad 'impl ret_value
let fsop_truncate_core env rpath len = (
fsm_get_state >>= (fun s0 ->
(match rpath with
| RN_file(_,_,i0_ref,_) -> begin
let len = natFromInt len in
let (s0, res) = env.env_ops.fops_read s0 i0_ref in
let bs = dest_RV_bytes res in
(* create a new array, of length len, with same contents *)
let bs' = T_list_array.resize bs len in
let s0 = env.env_ops.fops_write s0 i0_ref bs' in
fsm_put_state s0
end
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end)))
val fsop_truncate: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
int ->
fsmonad 'impl ret_value
let fsop_truncate env rpath len = (
let default rpath =
fsop_truncate_checks env rpath len >>= (fun _ ->
fsop_truncate_core env rpath len)
in
(match (rpath, is_mac_os_x_arch env) with
| (RN_error(ENOTDIR,<|re_nl=Just nl;re_rn=Just fopt|>),true) -> (
(* exec_truncate___truncate_nonempty_dir1__d2__sl_dotdot_f1.txt_____0-int.trace for truncate mac os x can resolve nonempty_dir1/d2/sl_dotdot_f1.txt/ to a file FIXME non-posix behaviour *)
fsm_choice (default fopt) (default rpath))
| (_,_) -> default rpath end))
(*--------------------------*)
(* unlink *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_unlink_checks_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> fsmonad 'impl ret_value
let fsop_unlink_checks_perms env rpath = (
fsm_get_state >>= fun s0 ->
(match rpath with
| RN_file(d0_ref,n,i0_ref,rp) -> (
begin (* check permissions *)
fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref)) (* posix/unlink.md EACCES:2 *)
|||
(
let arch = architecture_of_ty_arch env.env_arch in
let arch_allows_removing_writable = arch.arch_allows_removing_from_protected_dir_if_writeable in
let delete_ok = (env.env_prms.cp_has_file_restricted_delete_privilege arch_allows_removing_writable s0 d0_ref i0_ref) in
if delete_ok
then fsm_do_nothing
else fsm_raises [EPERM; EACCES] (* posix/unlink.md EPERM:2 EACCES:3 *)
)
end)
| _ -> fsm_do_nothing
end))
#endif
val fsop_unlink_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> fsmonad 'impl ret_value
let fsop_unlink_checks env rpath =
fsm_get_state >>= fun s0 ->
(match rpath with
| RN_error(e,_) -> fsm_raise e
| RN_none _ -> (fsm_cond_raises
[(ENOENT,true); (* posix/unlink.md ENOENT:1 *)
(ENOTDIR,is_linux_arch env && rn_ends_with_slash rpath)]) (* FIXME possibly posix/unlink.md ENOTDIR:2 , tr/25 *) (* coverage:mac_os_x:posix:irrelevant *)
| RN_dir _ -> (fsm_cond_raises
[(EISDIR,is_linux_arch env);
(EPERM,true)]) (* posix/unlink.md EPERM:1 *) (* LSB has EISDIR; POSIX requires EPERM; FIXME parameterize *)
| RN_file(d0_ref,n,i0_ref,rp) -> (
fsm_cond_raise ENOTDIR (is_linux_arch env && Resolve.res_name_is_symlink env.env_ops s0 rpath && rn_ends_with_slash rpath)) (* coverage:mac_os_x:posix:irrelevant *)
end)
#ifdef aspect_perms
|||
fsop_unlink_checks_perms env rpath
#endif
val fsop_unlink_core: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> fsmonad 'impl ret_value
let fsop_unlink_core env rpath = (
fsm_get_state >>= fun s0 ->
(match rpath with
| RN_file(d0_ref,n,_,_) -> (
let s0 = env.env_ops.fops_unlink s0 d0_ref n in
fsm_put_state s0)
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end))
val fsop_unlink: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_unlink env rpath = (
let default rpath =
fsop_unlink_checks env rpath >>= (fun _ ->
fsop_unlink_core env rpath)
in
(match (rpath, is_mac_os_x_arch env) with
| (RN_error(ENOTDIR,<|re_nl=Just nl;re_rn=Just fopt|>),true) -> (
(* exec_unlink___unlink_nonempty_dir1__sl_f1.txt__-int.trace for unlink mac os x can resolve sl_f1.txt/ to a file FIXME non-posix behaviour *)
fsm_choice (default fopt) (default rpath))
| (_,_) -> default rpath end))
(*--------------------------*)
(* chmod *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_chmod_checks_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> file_perm -> fsmonad 'impl ret_value
let fsop_chmod_checks_perms env rpath perm = (
fsm_get_state >>= fun s0 ->
(match rpath with
| RN_file(_,_,i0_ref,_) ->
fsm_cond_raise EPERM (not (env.env_prms.cp_has_file_chmod_permission s0 i0_ref))
| RN_dir(d0_ref, _) ->
fsm_cond_raise EPERM (not (env.env_prms.cp_has_dir_chmod_permission s0 d0_ref))
| _ -> fsm_do_nothing
end))
#endif
val fsop_chmod_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> file_perm -> fsmonad 'impl ret_value
let fsop_chmod_checks env rpath perm =
(match rpath with
| RN_error(e,_) -> (fsm_raise e)
| RN_none _ -> (fsm_raise ENOENT) (* posix/chmod.md ENOENT:1 *)
| RN_dir _ -> fsm_do_nothing
| RN_file _ -> fsm_do_nothing
end)
#ifdef aspect_perms
|||
fsop_chmod_checks_perms env rpath perm
#endif
val fsop_chmod_core: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> file_perm -> fsmonad 'impl ret_value
let fsop_chmod_core env rpath perm =
#ifdef aspect_perms
fsm_get_state >>= fun s0 ->
(match rpath with
| RN_file(_,_,i0_ref,_) -> (
let s1 = env.env_perm_ops.pops_set_perm_file s0 perm i0_ref in
fsm_put_state s1)
| RN_dir(d0_ref, _) -> (
let s1 = env.env_perm_ops.pops_set_perm_dir s0 perm d0_ref in
fsm_put_state s1)
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end)
#else
fsm_do_nothing
#endif
val fsop_chmod: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
file_perm ->
fsmonad 'impl ret_value
let fsop_chmod env rpath perm = (
fsop_chmod_checks env rpath perm >>= (fun _ ->
fsop_chmod_core env rpath perm))
(*--------------------------*)
(* chown *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_chown_checks_perms : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> uid -> gid -> fsmonad 'impl ret_value
let fsop_chown_checks_perms env rpath u g = (
fsm_get_state >>= fun s0 ->
(match rpath with
| RN_file(_,_,i0_ref,_) ->
fsm_cond_raise EPERM (not (env.env_prms.cp_has_file_chown_permission s0 i0_ref))
| RN_dir(d0_ref, _) ->
fsm_cond_raise EPERM (not (env.env_prms.cp_has_dir_chown_permission s0 d0_ref))
| _ -> fsm_do_nothing
end))
#endif
val fsop_chown_checks : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> uid -> gid -> fsmonad 'impl ret_value
let fsop_chown_checks env rpath u g =
(match rpath with
| RN_error(e,_) -> (fsm_raise e)
| RN_none _ -> (fsm_raise ENOENT) (* posix/chown.md ENOENT:1 *)
| RN_dir _ -> fsm_do_nothing
| RN_file _ -> fsm_do_nothing
end)
#ifdef aspect_perms
|||
fsop_chown_checks_perms env rpath u g
#endif
val fsop_chown_core: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> uid -> gid -> fsmonad 'impl ret_value
let fsop_chown_core env rpath u g =
#ifdef aspect_perms
fsm_get_state >>= fun s0 ->
(match rpath with
| RN_file(_,_,i0_ref,_) -> (
let s1 = env.env_perm_ops.pops_chown_file s0 (u, g) i0_ref in
fsm_put_state s1)
| RN_dir(d0_ref, _) -> (
let s1 = env.env_perm_ops.pops_chown_dir s0 (u, g) d0_ref in
fsm_put_state s1)
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end)
#else
fsm_do_nothing
#endif
val fsop_chown: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
uid -> gid ->
fsmonad 'impl ret_value
let fsop_chown env rpath u g = (
fsop_chown_checks env rpath u g >>= (fun _ ->
fsop_chown_core env rpath u g))
(*--------------------------*)
(* pwrite *)
(*--------------------------*)
val fsop_pwrite_checks: forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl -> entry 'dir_ref 'file_ref -> ty_bytes -> nat -> off_t -> fsmonad 'impl ret_value
let fsop_pwrite_checks ops entry bs len ofs = (
(fsm_cond_raise EINVAL (ofs < 0) (* invariant: offsets can never be < 0 *))
|||
(fsm_cond_raise EISDIR (is_dir_ref_entry entry) (* coverage:impossible - it is impossible to open a directory with a write flag, so pwrite cannot obtain a directory entry *)
(* posix does not allow writing to a dir. However, this is not explicit.
Posix specifies write in terms of file-descriptors.
It requires that the file descriptor is writeable (posix/write.md EBADF:1). However,
directories cannot be opened for writing (posix/open.md EISDIR:1). Therefore, we cannot
write to a directory. *)
)
)
val fsop_pwrite_core: forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl -> entry 'dir_ref 'file_ref -> ty_bytes -> nat -> off_t -> fsmonad 'impl ret_value
let fsop_pwrite_core ops entry bs len ofs = fsm_get_state >>= (fun s0 ->
(match entry with
| Dir_ref_entry _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
| File_ref_entry i0_ref -> (
let (s1, res) = ops.fops_read s0 i0_ref in
let bs' = dest_RV_bytes res in
(* non-deterministically choose the amount of data to write, if
an interrupt occurs during writing or the file-size reaches
some limit write might not write all the data given. *)
(fsm_choose_nat len >>= (fun len_written ->
(* want to create a new array from bs' and bs *)
let bs'' = T_list_array.list_array_write (bs,0,len_written) (bs',natFromInt ofs) in
let s2 = ops.fops_write s1 i0_ref bs'' in
fsm_put_state_return s2 (RV_num len_written)
)))
end))
val fsop_pwrite: forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
entry 'dir_ref 'file_ref ->
ty_bytes ->
nat ->
off_t ->
fsmonad 'impl ret_value
let fsop_pwrite ops entry bs len ofs = (
fsop_pwrite_checks ops entry bs len ofs >>= (fun _ ->
fsop_pwrite_core ops entry bs len ofs))
(*--------------------------*)
(* pwrite_rn *)
(*--------------------------*)
(* fsop_pwrite_rn is used by the fs level. Similarly to fsop_pread_rn it is not really part of the spec *)
#ifdef aspect_perms
val fsop_pwrite_rn_checks_perms: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> ty_bytes -> nat -> off_t -> fsmonad 'impl ret_value
let fsop_pwrite_rn_checks_perms env (rn:res_name 'dir_ref 'file_ref) bs len ofs = (fsm_get_state >>= (fun s0 -> (* coverage:unused *)
(match rn with
| RN_file (_,_,i0_ref,_) ->
fsm_cond_raise EACCES (not (env.env_prms.cp_has_file_write_permission s0 i0_ref)) (* guessing here *) (* coverage:unused *)
| _ -> fsm_do_nothing (* coverage:unused *)
end)))
#endif
val fsop_pwrite_rn_checks: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> ty_bytes -> nat -> off_t -> fsmonad 'impl ret_value
let fsop_pwrite_rn_checks env (rn:res_name 'dir_ref 'file_ref) bs len ofs = (
(fsm_cond_raise EINVAL (ofs < 0) (* invariant: offsets can never be < 0 *) ) (* coverage:unused *)
|||
(match rn with
| RN_error (e,_) -> (fsm_raise e) (* coverage:unused *)
| RN_none _ -> (fsm_raise ENOENT) (* coverage:unused *)
| RN_dir _ -> (fsm_raise EISDIR) (* directories cannot be written to, see pre_write for explanation *) (* coverage:unused *)
| RN_file (_,_,i0_ref,_) ->
(* actually, these checks are a subset of the already performed tests, so they could be skipped.
However for the sake of clarity and anticipating changes in the future, let's keep them here. *)
fsop_pwrite_checks env.env_ops ((File_ref_entry i0_ref):entry 'dir_ref 'file_ref) bs len ofs (* coverage:unused *)
end)
#ifdef aspect_perms
|||
(fsop_pwrite_rn_checks_perms env rn bs len ofs)
#endif
)
val fsop_pwrite_rn_core: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> ty_bytes -> nat -> off_t -> fsmonad 'impl ret_value
let fsop_pwrite_rn_core env (rn:res_name 'dir_ref 'file_ref) bs len ofs = (fsm_get_state >>= (fun s0 -> (* coverage:unused *)
(match rn with
| RN_file(d0_ref,n,i0_ref,rp) ->
fsop_pwrite_core env.env_ops ((File_ref_entry i0_ref):entry 'dir_ref 'file_ref) bs len ofs (* coverage:unused *)
| _ -> fsm_special Impossible "error raised before" (* coverage:unused *)
end)))
val fsop_pwrite_rn: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
ty_bytes ->
nat ->
off_t ->
fsmonad 'impl ret_value
let fsop_pwrite_rn env (rn:res_name 'dir_ref 'file_ref) bs len ofs = (
fsop_pwrite_rn_checks env rn bs len ofs >>= (fun _ -> (* coverage:unused *)
fsop_pwrite_rn_core env rn bs len ofs) (* coverage:unused *))
(*--------------------------*)
(* symlink *)
(*--------------------------*)
#ifdef aspect_perms
val fsop_symlink_checks_perms: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> ty_bytes -> res_name 'dir_ref 'file_ref -> fsmonad 'impl ret_value
let fsop_symlink_checks_perms env src dst = (fsm_get_state >>= (fun s0 ->
( match dst with
| RN_none(d0_ref,_,_) -> fsm_cond_raise EACCES (not (env.env_prms.cp_has_dir_write_permission s0 d0_ref)) (* posix/symlink.md EACCES:1 *)
| _ -> fsm_do_nothing
end
)))
#endif
val fsop_symlink_checks: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> ty_bytes -> res_name 'dir_ref 'file_ref -> fsmonad 'impl ret_value
let fsop_symlink_checks env src dst = (
( match dst with
| RN_error (e,_) -> (fsm_raise e)
| RN_dir _ -> (fsm_raise EEXIST) (* posix/symlink.md EEXISTS:1 *)
| RN_file _ -> (fsm_raise EEXIST) (* posix/symlink.md EEXISTS:1 *)
| RN_none _ ->
(if (is_linux_arch env || is_mac_os_x_arch env) (* mac: symlink xyz /slink_2/ returns ENOENT; FIXME non-posix behaviour? *)
&& rn_ends_with_slash dst then (* coverage:mac_os_x:posix:irrelevant *)
fsm_raise ENOENT (* adhoc_symlink_tests *) (* coverage:mac_os_x:posix:irrelevant *)
else
fsm_do_nothing)
end
)
#ifdef aspect_perms
|||
fsop_symlink_checks_perms env src dst
#endif
)
val fsop_symlink_core: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> ty_bytes -> res_name 'dir_ref 'file_ref -> fsmonad 'impl ret_value
let fsop_symlink_core env src dst = (fsm_get_state >>= (fun s0 ->
( match dst with
| RN_none(d0_ref,n,_) ->
(let s1 = env.env_ops.fops_symlink s0 d0_ref n src in
fsm_put_state s1)
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end)))
val fsop_symlink: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_bytes ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_symlink env src dst = (
fsop_symlink_checks env src dst >>= (fun _ ->
fsop_symlink_core env src dst))
(*--------------------------*)
(* readlink *)
(*--------------------------*)
(* Notice, that readlink does not check for any read permission on
the link itself. readlinkat however does *)
val fsop_readlink_checks: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> fsmonad 'impl ret_value
let fsop_readlink_checks env src = (fsm_get_state >>= fun s0 ->
(match src with
| RN_error (e,_) -> (fsm_raise e)
| RN_dir _ -> (fsm_raise EINVAL)
| RN_none _ -> (fsm_raise ENOENT)
| RN_file(_,_,i0_ref,_) -> (
let ss = env.env_ops.fops_stat_file s0 i0_ref in
fsm_cond_raise EINVAL (ss.st_kind <> S_IFLNK)
)
end))
val fsop_readlink_core: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl -> res_name 'dir_ref 'file_ref -> fsmonad 'impl ret_value
let fsop_readlink_core env src = (fsm_get_state >>= (fun s0 ->
(match src with
| RN_file(_,_,i0_ref,_) -> (
let bs = env.env_ops.fops_readlink s0 i0_ref in
fsm_return (RV_bytes(bs)))
| _ -> fsm_special Impossible "error raised before" (* coverage:impossible *)
end)))
val fsop_readlink: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
res_name 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let fsop_readlink env src = (
fsop_readlink_checks env src >>= (fun _ ->
fsop_readlink_core env src))
end(* *)
(******************************************************************************)
(* Fs_commands *)
(* *)
(* A kind of interface to Fs_operations. *)
(******************************************************************************)
module Fs_commands = struct
open Fs_operations
(* Dummy open statements to ensure Lem produces decent HOL and Isabelle output *)
open Fs_types
open The_monad
let fs_link = fsop_link
let fs_mkdir = fsop_mkdir
let fs_open_close = fsop_open_close
let fs_pread = fsop_pread_rn
let fs_pwrite = fsop_pwrite_rn
let fs_readlink = fsop_readlink
let fs_rename = fsop_rename
let fs_rmdir = fsop_rmdir
let fs_stat = fsop_stat
let fs_lstat = fsop_lstat
let fs_symlink = fsop_symlink
let fs_truncate = fsop_truncate
let fs_unlink = fsop_unlink
let fs_chown = fsop_chown
let fs_chmod = fsop_chmod
end
(******************************************************************************)
(* Fs transition system *)
(******************************************************************************)
module Fs_transition_system = struct
open The_monad
open Fs_types
open Fs_commands
val ty_fs_ext_command_to_fsmonad : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_fs_ext_command 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let ty_fs_ext_command_to_fsmonad env cmd = match cmd with
| FS_OPEN_CLOSE (p,fs,mo) -> fs_open_close env p fs mo
| FS_PREAD (p,len_,ofs) -> fs_pread env p len_ ofs (* coverage:impossible -the OS_PREAD calls os_read, not this fs command *)
| FS_PWRITE (p,bs,len_,ofs) -> fs_pwrite env p bs len_ ofs (* coverage:impossible -the OS_PWRITE calls os_write, not this fs command *)
end
(* [ty_fs_command_to_fsmonad env cmd] returns the
monad operation for command [cmd] in environment [env]. *)
val ty_fs_command_to_fsmonad : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_fs_command 'dir_ref 'file_ref ->
fsmonad 'impl ret_value
let ty_fs_command_to_fsmonad env cmd = match cmd with
| FS_LINK (s,d) -> (fs_link env s d)
| FS_MKDIR (s,p) -> (fs_mkdir env s p)
| FS_READLINK p -> (fs_readlink env p)
| FS_RENAME (s,d) -> (fs_rename env s d)
| FS_RMDIR p -> (fs_rmdir env p)
| FS_STAT p -> (fs_stat env.env_ops p)
| FS_LSTAT p -> (fs_lstat env.env_ops p)
| FS_SYMLINK (s,d) -> (fs_symlink env s d)
| FS_TRUNCATE (p,l) -> (fs_truncate env p l)
| FS_UNLINK p -> (fs_unlink env p)
| FS_CHMOD (s, p) -> (fs_chmod env s p)
| FS_CHOWN (s, u, g) -> (fs_chown env s u g)
| FS_EXTENDED_CMD cmd' -> ty_fs_ext_command_to_fsmonad env cmd'
end
val fs_trans: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
'impl ->
ty_fs_command 'dir_ref 'file_ref ->
finset (monad_state 'impl ret_value)
let fs_trans env s0 cmd = (
let m = ty_fs_command_to_fsmonad env cmd in
let rs = run_fsmonad m s0 in
rs)
end
(******************************************************************************)
(* Os_operations *)
(* *)
(* This module defines operations at the OS level. These include open, *)
(* close, read and write, which interact with the OS via file descriptors. *)
(******************************************************************************)
module Os_operations = struct
open The_monad
open Fs_types
open Fs_arch
open Fs_operations
#ifdef aspect_perms
open Fs_permissions
#endif
(*-------------------------------*)
(* auxiliary functions *)
(*-------------------------------*)
(* In the following we frequently need to lookup
the state of a process. This can fail, if the process
does not exist. Preceding checks guarantee that this
won't happen. To simplify the code, we don't code a
code distinction all the time, but use this auxiliary
function that fails hard if something goes wrong. *)
val lookup_per_process_state : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
per_process_state 'dir_ref
let lookup_per_process_state s0 pid =
let pps_opt = fmap_lookup s0.oss_pid_table pid in
(match pps_opt with
| Nothing -> failwith "lookup_per_process_state failed" (* coverage:irrelevant *)
| Just pps -> pps
end)
(* [lookup_fid_of_fd s0 pid fd] is a convenience function
that looks up the [fid] and its state for file-descriptor [fd] of
process [pid] in state [s0]. If no such file-descriptor exists,
[Nothing] is returned. *)
val lookup_fid_of_fd : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_fd ->
Maybe.maybe (ty_fid * (fid_state 'dir_ref 'file_ref))
let lookup_fid_of_fd s0 pid fd =
let pps = lookup_per_process_state s0 pid in
let fd_st = fmap_lookup pps.pps_fd_table fd in
(match fd_st with
| Nothing -> Nothing
| Just fd_st -> (
(* get fid *)
let fid = fd_st.fds_fid in
let fid_st = fmap_lookup s0.oss_fid_table fid in
(match fid_st with
| Nothing -> (failwith "impossible: 1601 fds point to fids that are in the oss_fid_table") (* coverage:impossible *)
| Just fid_st -> Just (fid, fid_st)
end))
end)
(* [get_run_state s0 pid rs] gets the run state of process [pid] in state [s0]. *)
val get_run_state : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_pps_pid_run_state
let get_run_state s0 pid = (
let ppstate = lookup_per_process_state s0 pid in
let rs = ppstate.pps_pid_run_state in
rs
)
(* [update_run_state s0 pid rs] updates the
return state of process [pid] in state [s0] to [rs]. *)
val update_run_state : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_pps_pid_run_state ->
ty_os_state 'dir_ref 'file_ref 'impl
let update_run_state s0 pid rs = (
let ppstate = lookup_per_process_state s0 pid in
let ppstate' = <| ppstate with pps_pid_run_state = rs |> in
<| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,ppstate')) |>
)
(* [update_pending_return s0 pid ev] updates the
return state of process [pid] in state [s0] to [PENDING_RETURN(ev)]. *)
val update_pending_return : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
error_or_value ret_value ->
ty_os_state 'dir_ref 'file_ref 'impl
let update_pending_return s0 pid ev =
update_run_state s0 pid (PENDING_RETURN ev)
(* [update_pending_return_and_fs_state s0 pid ev fs_state] updates the
return state of process [pid] in state [s0] to [PENDING_RETURN(ev)]
and the file-system state to [fs_state]. *)
val update_pending_return_and_fs_state : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
error_or_value ret_value ->
'impl ->
ty_os_state 'dir_ref 'file_ref 'impl
let update_pending_return_and_fs_state s0 pid ev fs_state = (
let ppstate = lookup_per_process_state s0 pid in
let ppstate' = <| ppstate with pps_pid_run_state = PENDING_RETURN(ev) |> in
<| s0 with oss_fs_state=fs_state; oss_pid_table=(fmap_update s0.oss_pid_table (pid,ppstate')) |>
)
(*-------------------------------*)
(* create_fd *)
(*-------------------------------*)
(* [smallest_free_nat p current max] finds the smallest number
between [current] (including) and [max] (excluding) that satisfied
[p]. If no such number exists [max] is returned. *)
val smallest_free_nat : (nat -> bool) -> nat -> nat -> nat
let rec smallest_free_nat p current_num max_num =
if (p current_num || (current_num >= max_num)) then current_num else (
smallest_free_nat p (succ current_num) max_num
)
(* [get_smallest_free_fd pid s0] computes the file-descriptor
to use is state [s0] for process [pid]. Posix specifies,
that always the smallest free one is used. *)
val get_smallest_free_fd : forall 'dir_ref 'file_ref 'impl.
ty_pid ->
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_fd
let get_smallest_free_fd pid s0 = (
let pps = lookup_per_process_state s0 pid in
let fdt = pps.pps_fd_table in
let free_check n = not (fmap_in_dom (FD n) fdt) in
let new_fd = FD (smallest_free_nat free_check 0 (fmap_size fdt)) in
new_fd
)
(* [get_free_fid s0] returns a [fid] that is free in state [s0].
In contrast to fds, we don't care, which free one is returned.
So the implementation can be much simpler (max + 1). *)
val get_free_fid : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_fid
let get_free_fid s0 =
FID (fmap_fold (
fun (FID k) _ m ->
if k >= m
then succ k
else m (* coverage:impossible *)
) s0.oss_fid_table 0)
(* [create_fd ops pid entry oflags s0] creates a new file
descriptor for entry [entry] *)
val create_fd : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
ty_pid ->
entry 'dir_ref 'file_ref ->
finset open_flag ->
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_os_state 'dir_ref 'file_ref 'impl * ty_fd * ty_fid
let create_fd ops pid entry oflags s0 = (
(* get free fd and fid *)
let new_fd = get_smallest_free_fd pid s0 in
let new_fid = get_free_fid s0 in
(* get initial states for them *)
let fd_state = <| fds_fid=new_fid; fds_FD_CLOEXEC=(finset_mem O_CLOEXEC oflags) |> in
let fid_state = <| fids_offset=0; fids_entry=entry; fids_oflags=oflags; fids_open_or_closed=FID_OPEN |> in
(* store it *)
let pps = lookup_per_process_state s0 pid in
let pps = <| pps with pps_fd_table=(fmap_update pps.pps_fd_table (new_fd,fd_state)) |> in
let s0 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,pps)) |> in
let s0 = <| s0 with oss_fid_table=(fmap_update s0.oss_fid_table (new_fid,fid_state)) |> in
(s0,new_fd,new_fid))
(*-------------------------------*)
(* create_dh *)
(*-------------------------------*)
(* [get_smallest_free_dh s0] gets a free dir-handle
is state [s0]. Posix does not specify, what dir-handles are
or which ones are used. For Posix, it is a pointer to a dir-structure.
However, for our model, we want some predictability, since we
want use dir-handles in our testing-traces. Therefore, we
always return the smallest free one. *)
val get_smallest_free_dh : forall 'dir_ref 'file_ref 'impl.
ty_pid ->
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_dh
let get_smallest_free_dh pid s0 = (
let pps = lookup_per_process_state s0 pid in
let dht = pps.pps_dh_table in
let free_check n = not (fmap_in_dom (DH n) dht) in
let new_dh = DH (smallest_free_nat free_check 1 (fmap_size dht + 1)) in
new_dh
)
(** [rewind_dh ops dhs fs0] rewinds directory handle state [dhs] in fs-state [fs0].
It returns the updated dir-handle and fs-states. *)
val rewind_dhs : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
dh_state 'dir_ref ->
'impl ->
(dh_state 'dir_ref * 'impl)
let rewind_dhs ops dhs fs_st = (
(* reset the observer *)
let (fs_st', _) = ops.fops_observe_dir fs_st dhs.dhs_observe_handle in
(* reset the dh_state *)
let (fs_st'', current_entries) = ops.fops_readdir fs_st' dhs.dhs_dir_ref in
let dhs' = <| dhs with dhs_must_report = "."::".."::current_entries; dhs_may_report = [] |> in
(dhs',fs_st'')
)
(* [create_dh ops pid d0_ref s0] creates a new directory
handle for directory d0_ref *)
val create_dh : forall 'dir_ref 'file_ref 'impl.
fs_ops 'dir_ref 'file_ref 'impl ->
ty_pid ->
'dir_ref ->
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_os_state 'dir_ref 'file_ref 'impl * ty_dh
let create_dh ops pid d0_ref s0 = (
(* get free dh *)
let new_dh = get_smallest_free_dh pid s0 in
(* start observing the directory *)
let (fs_st', oh) = ops.fops_observe_dir_register s0.oss_fs_state d0_ref in
(* get initial states for them *)
let (dh_st, fs_st'') = rewind_dhs ops
(<| dhs_dir_ref = d0_ref; dhs_observe_handle = oh;
dhs_must_report = []; dhs_may_report = [] |>) fs_st' in
(* store it *)
let pps = lookup_per_process_state s0 pid in
let pps = <| pps with pps_dh_table=(fmap_update pps.pps_dh_table (new_dh,dh_st)) |> in
let s0 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,pps)); oss_fs_state = fs_st' |> in
(s0,new_dh))
(*-------------------------------*)
(* os_close *)
(*-------------------------------*)
(* [os_close env pid fd s0] closed file-descriptor [fd] or process [pid] in state [s0]. *)
(* FIXME os_close is a complete hack currently - just to get open tests to go through *)
val os_close: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_fd ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_close env pid fd s0 = (
let ppstate = lookup_per_process_state s0 pid in
(* check that fd is valid *)
match fmap_lookup ppstate.pps_fd_table fd with
| Nothing -> (
let ppstate = <| ppstate with pps_pid_run_state=PENDING_RETURN(Error EBADF) |> in
let s0 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,ppstate)) |> in
finset_singleton (OS_normal s0)) (* we assume ppstate has not been altered before being passed in *)
| Just fds -> (
let ppstate = <| ppstate with pps_pid_run_state=PENDING_RETURN(Value RV_none) |> in
let new_fdt = fmap_remove (ppstate.pps_fd_table) fd in
let ppstate = <| ppstate with pps_fd_table=new_fdt |> in
let s0 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,ppstate)) |> in
finset_singleton (OS_normal s0)) end)
(*-------------------------------*)
(* os_open *)
(*-------------------------------*)
val os_open: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
res_name 'dir_ref 'file_ref ->
int_open_flags ->
maybe file_perm ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_open env pid rpath oflag mode_opt s0 = (
(* run fs-level open *)
let rs = begin
let fs0 = s0.oss_fs_state in
let f0 = fsop_open env rpath oflag mode_opt in
run_fsmonad f0 fs0
end in
(* For each resulting monad_state, we need to construct
an os-state *)
let process_fs_result st = (match st with
| Special_state(ss,msg) -> (* just forward special results *) (OS_special(ss,msg)) (* coverage:linux:irrelevant *)
| Error_state (fs_st, e) ->
(* if an error occured, just forward the error and fs_state (which should not have been changed, though) *)
OS_normal (update_pending_return_and_fs_state s0 pid (Error e) fs_st)
| Normal_state (fs_st, (entry,oflags)) -> (begin
(* for a normal result, create a corresponding fd and return it *)
(* put fs_state in things into the os_state *)
let s0 = <| s0 with oss_fs_state=fs_st |> in
(* create fd, open fid, handle O_CLOEXEC *)
let (s0,fd,fid) = create_fd env.env_ops pid entry oflags s0 in
(* return value - an int corresponding to the fd *)
let ppstate = lookup_per_process_state s0 pid in
let ev = Value (RV_num (dest_FD fd)) in
let ppstate' = <| ppstate with pps_pid_run_state = PENDING_RETURN(ev) |> in
let s0 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,ppstate')) |> in
(OS_normal s0)
end)
end) in
finset_image process_fs_result rs)
(*-------------------------------*)
(* os_read *)
(*-------------------------------*)
(* todo: - indicates that the flag is not applicable
ACCMODE
X O_APPEND
X O_CLOEXEC
X O_CREAT
-O_DSYNC
-O_NOCTTY
-O_NONBLOCK "the O_NONBLOCK flag shall not cause an error, but it is unspecified whether the file status flags will include the O_NONBLOCK flag"
-O_RSYNC
-O_SYNC
X O_TRUNC
-O_TTY_INIT *)
val os_read: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_fd ->
size_t ->
maybe off_t ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_read env pid fd sz ofsopt s0 =
(* lookup the fd and fid we want to read from *)
(match lookup_fid_of_fd s0 pid fd with
| Nothing -> (* if it does not exist, raise EBADF *)
finset_singleton (OS_normal (update_pending_return s0 pid (Error EBADF))) (* posix/read.md EBADF:1 *)
| Just (fid, fid_st) -> (
(* check that fid is open for reading *)
let oflags = fid_st.fids_oflags in
if not (finset_mem O_RDONLY oflags || finset_mem O_RDWR oflags) then
finset_singleton (OS_normal (update_pending_return s0 pid (Error EBADF))) (* posix/read.md EBADF:1 *)
else (begin
(* we have a fd, which we are allowed to read from, so
execute the fs-read operation *)
let rs = (begin
let ofs = (match ofsopt with | Nothing -> intFromNat fid_st.fids_offset | Just ofs -> ofs end) in
let read_op = fsop_pread env fid_st.fids_entry (sz:nat) ofs in
run_fsmonad read_op s0.oss_fs_state
end) in
(* For each resulting monad_state, we need to construct
an os-state *)
let process_fs_result st = (match st with
| Special_state(ss,msg) -> (* just forward special results *) (OS_special(ss,msg)) (* coverage:impossible -this cannot be reached since we do not have architectures with the field arch_allows_dir set to true (only with this set to true we could have a special state returned by pread and forwarded by os_read) *)
| Error_state (fs_st, e) -> (* just forward errors, *)
OS_normal (update_pending_return_and_fs_state s0 pid (Error e) fs_st)
| Normal_state(fs_st, RV_bytes bs) -> (* a successful read *) (begin
(* forward results *)
let s0 = update_pending_return_and_fs_state s0 pid (Value (RV_bytes bs)) fs_st in
(* update fids_offset with bytes read, but only if we model read, i.e. no offset was given *)
let fid_st = (match ofsopt with | Just _ -> fid_st | Nothing ->
<| fid_st with fids_offset=(fid_st.fids_offset+(T_list_array.dim bs)) |> end) in
let s0 = <| s0 with oss_fid_table=(fmap_update s0.oss_fid_table (fid,fid_st)) |> in
OS_normal s0
end)
| Normal_state(fs_st, _) -> (failwith "os_read: impossible, value from fsop_read is RV_bytes") (* coverage:impossible *)
end) in
finset_image process_fs_result rs
end))
end)
(*-------------------------------*)
(* os_write *)
(*-------------------------------*)
val os_write: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_fd ->
ty_bytes ->
size_t ->
maybe off_t ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_write env pid fd bs sz ofsopt s0 =
(* lookup the fd and fid we want to write to *)
(match lookup_fid_of_fd s0 pid fd with
| Nothing -> (* if it does not exist, raise EBADF *)
finset_singleton (OS_normal (update_pending_return s0 pid (Error EBADF))) (* posix/write.md EBADF:1 *)
| Just (fid, fid_st) -> (
(* check that fid is open for writing *)
let oflags = fid_st.fids_oflags in
if not (finset_mem O_WRONLY oflags || finset_mem O_RDWR oflags) then
finset_singleton (OS_normal (update_pending_return s0 pid (Error EBADF))) (* posix/write.md EBADF:1 *)
else (* handle pwrite with append and negative offset *)
if (finset_mem O_APPEND oflags && (match ofsopt with | Just ofs -> ofs < 0 | Nothing -> false end)) then
finset_singleton (OS_normal (update_pending_return s0 pid (Error EINVAL)))
else (
(* compute offset *)
let ofs = ((* handle O_APPEND *)
if not (finset_mem O_APPEND oflags) then
(match ofsopt with | Just ofs -> ofs | Nothing -> intFromNat fid_st.fids_offset end)
else (* jump to very end of file *)
(match fid_st.fids_entry with
| Dir_ref_entry _ -> intFromNat fid_st.fids_offset (* will fail anyhow, so value unimportant *) (* coverage:impossible - this spec does not support opening directories with a write flag, so this case is never reached *)
| File_ref_entry i0_ref -> (intFromNat (file_get_size env.env_ops s0.oss_fs_state i0_ref))
end))
in
(* execute fs-level operation *)
let rs = (
let write_op = fsop_pwrite env.env_ops fid_st.fids_entry bs sz ofs in
run_fsmonad write_op s0.oss_fs_state
) in
(* For each resulting monad_state, we need to construct
an os-state *)
let process_fs_result st = (match st with
| Special_state(ss,msg) -> (* just forward special results *) (OS_special(ss,msg)) (* coverage:impossible - it is impossible to return a special state from fsop_pwrite *)
| Error_state (fs_st, e) -> (* just forward errors *)
OS_normal (update_pending_return_and_fs_state s0 pid (Error e) fs_st)
| Normal_state(fs_st, RV_num len_written) -> (* a successful write *) (begin
(* forward results *)
let s0 = update_pending_return_and_fs_state s0 pid (Value (RV_num len_written)) fs_st in
(* update fids_offset with bytes written, but only if we model write, i.e. no offset was given *)
let fid_st = (match ofsopt with | Just _ -> fid_st | Nothing ->
<| fid_st with fids_offset=((natFromInt ofs)+len_written) |> end) in
let s0 = <| s0 with oss_fid_table=(fmap_update s0.oss_fid_table (fid,fid_st)) |> in
OS_normal s0
end)
| Normal_state(fs_st, _) -> (failwith "os_write: impossible, value from fsop_write is RV_num") (* coverage:impossible *)
end) in
finset_image process_fs_result rs
))
end)
(*-------------------------------*)
(* os_lseek *)
(*-------------------------------*)
val os_lseek : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_fd ->
off_t ->
int_seek_command ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_lseek env pid fd (ofs:off_t) (int_command : int_seek_command) s0 = (
(* check fid *)
let fid_eov = (
(* check that fd is a valid fd *)
match (lookup_fid_of_fd s0 pid fd) with
| Nothing -> Error EBADF (* posix/lseek.md EBADF:1 *)
| Just (fid, fid_st) -> Value (fid, fid_st)
end
) in
(* check int_command *)
let seek_c_eov = (begin
let arch = architecture_of_ty_arch env.env_arch in
(match arch.arch_seek_command_of_int int_command with
| Nothing -> Error EINVAL (* posix/lseek.md EINVAL:1 *)
| Just seek_c -> Value seek_c
end)
end) in
(* raise errors of fd and int_command *)
(match (fid_eov, seek_c_eov) with
| (Error e1, Error e2) ->
finset_from_list [OS_normal (update_pending_return s0 pid (Error e1));
OS_normal (update_pending_return s0 pid (Error e2))]
| (Error e1, Value _) ->
finset_singleton (OS_normal (update_pending_return s0 pid (Error e1)))
| (Value _, Error e2) ->
finset_singleton (OS_normal (update_pending_return s0 pid (Error e2)))
| (Value (fid, fid_st), Value seek_c) -> (begin
if ((seek_c = SEEK_DATA) || (seek_c = SEEK_HOLE)) then
finset_singleton (OS_special (FIXME, "lseek: SEEK_DATA and SEEK_HOLE are unsupported by this spec")) (* coverage:mac_os_x:posix:irrelevant -there is no int code for SEEK_DATA and SEEK_HOLE so seek_c_eov returns always EINVAL and this match case is never entered *)
else (
(* checks successful, we can execute lseek *)
(* compute new offset *)
let (new_ofs_o_e : error_or_value off_t) = (match seek_c with
| SEEK_SET -> Value ofs
| SEEK_CUR -> Value ((intFromNat fid_st.fids_offset) + ofs)
| SEEK_END -> (match fid_st.fids_entry with
| Dir_ref_entry _ -> Error EOVERFLOW
| File_ref_entry i0_ref -> Value ((intFromNat (file_get_size env.env_ops s0.oss_fs_state i0_ref)) + ofs)
end)
| SEEK_DATA -> failwith "impossible: checked before" (* coverage:impossible *)
| SEEK_HOLE -> failwith "impossible: checked before" (* coverage:impossible *)
end) in
(match new_ofs_o_e with
| Error e -> finset_singleton (OS_normal (update_pending_return s0 pid (Error e)))
| Value new_ofs -> (
if (new_ofs < 0) then
finset_singleton (OS_normal (update_pending_return s0 pid (Error EINVAL))) (* posix/lseek.md EINVAL:2 *)
else begin (* put new offset in data-structure and return new state *)
let new_ofs_nat = natFromInt new_ofs in
let s1 = update_pending_return s0 pid (Value (RV_num new_ofs_nat)) in
let fid_st = <| fid_st with fids_offset=new_ofs_nat |> in
let s2 = <| s1 with oss_fid_table=(fmap_update s0.oss_fid_table (fid,fid_st)) |> in
finset_singleton (OS_normal s2)
end)
end))
end)
end)
)
(*-------------------------------*)
(* os_add_user_to_group *)
(*-------------------------------*)
val os_add_user_to_group: forall 'dir_ref 'file_ref 'impl.
ty_pid ->
uid -> gid ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_add_user_to_group pid uid gid s0 = (
#ifdef aspect_perms
let s0 = add_uid_to_gid s0 uid gid in
#endif
let s0 = update_pending_return s0 pid (Value (RV_none)) in
finset_singleton (OS_normal s0)
)
(*-------------------------------*)
(* os_umask *)
(*-------------------------------*)
val os_umask: forall 'dir_ref 'file_ref 'impl.
ty_pid ->
file_perm ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_umask pid new_mask s0 = (
let ppstate = lookup_per_process_state s0 pid in
let old_mask = ppstate.pps_file_creation_mask in
let ppstate' = <| ppstate with pps_file_creation_mask = new_mask;
pps_pid_run_state = PENDING_RETURN(Value(RV_file_perm old_mask)) |> in
let s0' = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,ppstate')) |> in
finset_singleton (OS_normal s0')
)
(*-------------------------------*)
(* os_chdir *)
(*-------------------------------*)
val os_chdir: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
res_name 'dir_ref 'file_ref ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_chdir env pid path s0 = (
let (cwd'_opt, ret) = match path with
| RN_error(e,_) -> (Nothing, Error e)
| RN_none _ -> (Nothing, Error ENOENT)
| RN_file _ -> (Nothing, Error ENOTDIR)
| RN_dir(d0_ref, _) -> (
#ifdef aspect_perms
let perm_checks = env.env_prms.cp_has_dir_search_permission s0.oss_fs_state d0_ref in
#else
let perm_checks = true in
#endif
if perm_checks then
(Just d0_ref, Value RV_none)
else
(Nothing, Error EACCES)
)
end in
let ppstate = lookup_per_process_state s0 pid in
let new_cwd = fromMaybe ppstate.pps_cwd cwd'_opt in
let ppstate' = <| ppstate with pps_cwd = new_cwd;
pps_pid_run_state = PENDING_RETURN(ret) |> in
let s0' = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,ppstate')) |> in
finset_singleton (OS_normal s0')
)
(*-------------------------------*)
(* os_opendir *)
(*-------------------------------*)
val os_opendir: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
res_name 'dir_ref 'file_ref ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_opendir env pid rpath s0 = (
(* run fs-level open *)
let rs = begin
let fs0 = s0.oss_fs_state in
let f0 = fsop_opendir env rpath in
run_fsmonad f0 fs0
end in
(* For each resulting monad_state, we need to construct
an os-state *)
let process_fs_result st = (match st with
| Special_state(ss,msg) -> (* just forward special results *) (OS_special(ss,msg)) (* coverage:linux:irrelevant *)
| Error_state (fs_st, e) -> (* just forward errors *)
OS_normal (update_pending_return_and_fs_state s0 pid (Error e) fs_st)
| Normal_state (fs_st, d0_ref) -> (begin
(* for a normal result, create a corresponding dir-handle and return it *)
(* put fs_state in things into the os_state *)
let s0 = <| s0 with oss_fs_state=fs_st |> in
(* create fd, open fid, handle O_CLOEXEC *)
let (s0,dh) = create_dh env.env_ops pid d0_ref s0 in
(* return value - an int corresponding to the fd *)
OS_normal (update_pending_return s0 pid (Value (RV_num (dest_DH dh))))
end)
end) in
finset_image process_fs_result rs)
(*-------------------------------*)
(* os_readdir *)
(*-------------------------------*)
val os_readdir: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_dh ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_readdir env pid dh s0 =
(* lookup the dh and fid we want to read from *)
let pps = lookup_per_process_state s0 pid in
(match fmap_lookup pps.pps_dh_table dh with
| Nothing -> (* if it does not exist, raise EBADF *)
finset_singleton (OS_normal (update_pending_return s0 pid (Error EBADF))) (* posix/readdir.md EBADF:1 *)
| Just dh_st -> (
(* get the changes to the directory since last readdir *)
let (fs_st', changes) = env.env_ops.fops_observe_dir s0.oss_fs_state dh_st.dhs_observe_handle in
let s1 = <| s0 with oss_fs_state = fs_st' |> in
(* incorparate the changes into the current state *)
let apply_change dhs ode = (match ode with
| OD_added n ->
(* If file n was newly added add it to the list that might be reported on.
Do this, even if the file is in there already or definitely needs reporting.
This is important in case of multiple delete / add events when a file actually
might be reported several times. *)
<| dhs with dhs_may_report = n :: dhs.dhs_may_report |>
| OD_removed n ->
(* if [n] needed to be reported, weaken that need into a maybe report *)
if (List.elem n dhs.dhs_must_report) then
<| dhs with dhs_must_report = List.delete n dhs.dhs_must_report;
dhs_may_report = n :: dhs.dhs_may_report |>
else dhs
end ) in
let dh_st' = List.foldl apply_change dh_st changes in
(* prepare a list of all possible return values / notice none is added later *)
let ret_names = removeDuplicates (dh_st'.dhs_must_report ++ dh_st'.dhs_may_report) in
let ret_state_from_name n = (
(* we need to remove the name we are returning from the list *)
let dh_st'' = if (List.elem n dh_st'.dhs_must_report) then
<| dh_st' with dhs_must_report = List.delete n dh_st'.dhs_must_report |>
else
<| dh_st' with dhs_may_report = List.delete n dh_st'.dhs_may_report |>
in
let pps' = <| pps with pps_dh_table=(fmap_update pps.pps_dh_table (dh,dh_st'')) |> in
let s2 = <| s1 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,pps')) |> in
OS_normal (update_pending_return s2 pid (Value (RV_bytes (T_list_array.of_string n))))
) in
let ret_name_states = List.map ret_state_from_name ret_names in
(* if there is nothing left we definitely have to report, add RV_none *)
let ret_none_state = (
(* If we return None, we could set some flag that from now on, only None is returned.
But I don't think this is enforced behaviour, although this is most likely what
happens in a real implementation *)
let pps' = <| pps with pps_dh_table=(fmap_update pps.pps_dh_table (dh,dh_st')) |> in
let s2 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,pps')) |> in
OS_normal (update_pending_return s1 pid (Value RV_none))
) in
(* do the return *)
let ret_states = if (List.null dh_st'.dhs_must_report) then ret_none_state :: ret_name_states else ret_name_states in
finset_from_list ret_states
)
end)
(*-------------------------------*)
(* os_closedir *)
(*-------------------------------*)
val os_closedir: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_dh ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_closedir env pid dh s0 =
(* lookup the dh and fid we want to read from *)
let pps = lookup_per_process_state s0 pid in
(match fmap_lookup pps.pps_dh_table dh with
| Nothing -> (* if it does not exist, raise EBADF *)
finset_singleton (OS_normal (update_pending_return s0 pid (Error EBADF))) (* posix/closedir.md EBADF:1 *)
| Just dh_st -> (
(* unregister the observe_handle *)
let fs_st' = env.env_ops.fops_observe_dir_unregister s0.oss_fs_state dh_st.dhs_observe_handle in
(* update the state s0 *)
let pps' = <| pps with pps_pid_run_state=PENDING_RETURN (Value RV_none);
pps_dh_table=(fmap_remove pps.pps_dh_table dh) |> in
let s1 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,pps')); oss_fs_state = fs_st' |> in
finset_singleton (OS_normal s1)
)
end)
(*-------------------------------*)
(* os_rewinddir *)
(*-------------------------------*)
val os_rewinddir: forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_dh ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_rewinddir env pid dh s0 =
(* lookup the dh and fid we want to read from *)
let pps = lookup_per_process_state s0 pid in
(match fmap_lookup pps.pps_dh_table dh with
| Nothing -> (* if it does not exist, raise EBADF *)
finset_singleton (OS_normal (update_pending_return s0 pid (Error EBADF))) (* guessing here *)
| Just dh_st -> (
(* reset the observe handle *)
let (dh_st', fs_st') = rewind_dhs env.env_ops dh_st s0.oss_fs_state in
(* update the state s0 *)
let pps' = <| pps with pps_pid_run_state=PENDING_RETURN (Value RV_none);
pps_dh_table=(fmap_update pps.pps_dh_table (dh, dh_st')) |> in
let s1 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,pps')); oss_fs_state = fs_st' |> in
finset_singleton (OS_normal s1)
)
end)
(*-------------------------------*)
(* os_determinise *)
(*-------------------------------*)
(* For some operations like read and write are non-deterministic, but it would
in some situations be nice to pick a peticular result. In the case of write
for example ensure that all of the data is written. The following function
achieves this in a general way.
[os_determinise select_fun ss] tries to pick only one state from state set
[ss] using [rv_less] to choose which one. If the state set contains
states that are
- special or
- aren't in run state PENDING_RETURN or
- are not about to return a value,
the full set is returned. Otherwise one of these states is picked and
and a singleton set is returned. [rv_cmp] is used to determine,
which state is picked. [rv_less] encodes a partial order on return-values.
A state that returns a maximum according to [rv_less] is picked. *)
val os_determinise : forall 'dir_ref 'file_ref 'impl.
(ret_value -> ret_value -> bool) ->
ty_pid ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl) ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_determinise rv_less pid ss = begin
let extract_rv sos = (match sos with
| OS_special _ -> Nothing (* coverage:impossible -we would need to receive a special state from os_read and os_write, only funcitons that use determinise, and they cannot be reached (view os_write and os_read) *)
| OS_normal s -> (match (get_run_state s pid) with
| PENDING_RETURN (Value v) -> Just v
| _ -> Nothing
end)
end) in
if ((finset_is_empty ss) || (finset_any (fun sos -> isNothing (extract_rv sos)) ss)) then
(* we have a set of states we can't determinise; so do nothing with it *)
ss
else (
(* The set is not empty and all states have a value pending to be returned.
So select the best one. *)
let sl = list_from_finset ss in
let picked_s = foldl1 (fun s1 s2 -> (
match (extract_rv s1, extract_rv s2) with
| (Just rv1, Just rv2) ->
if (rv_less rv1 rv2)
then s2
else s1 (* coverage:impossible -using fsm_choose_nat in both os_read and os_write we end up creating return values (fsm_choose_nat len_max) in increasing order *)
| _ -> (* should not happen as tested before, but degenerate gracefully *) s1 (* coverage:impossible *)
end)) sl in
(* return a singleton set of the picked state *)
finset_singleton picked_s
)
end
(* The comparison function for the read and write functions. It maximises the
read/written data. *)
val os_determinise_less_read_write : ret_value -> ret_value -> bool
let os_determinise_less_read_write rv1 rv2 = (match (rv1, rv2) with
| (RV_num n1, RV_num n2) -> (n1 < n2)
| (RV_bytes bs1, RV_bytes bs2) ->
(T_list_array.dim bs1 < T_list_array.dim bs2)
| _ -> (* should not happen for read and write *) false (* coverage:impossible *)
end)
end
(******************************************************************************)
(* Os_transition system *)
(* *)
(* The model of transitions at the operating system level is: *)
(* - A call gets made with OS_CALL cmd *)
(* - The process gets moved to a blocked state *)
(* - Further steps process the call *)
(* - A return transition occurs with OS_RETURN; *)
(* at this point, the process is unblocked *)
(******************************************************************************)
module Os_transition_system = struct
open Fs_types
open Fs_arch
open Resolve (* for process_path *)
open Fs_transition_system
#ifdef aspect_perms
open Fs_permissions
#endif
open Os_operations
(*-------------------------------*)
(* os_trans_pid *)
(*-------------------------------*)
(* run fs-level commands *)
val os_run_fs_command : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_fs_command 'dir_ref 'file_ref ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_run_fs_command env pid cmd s0 = begin
let rs = fs_trans env s0.oss_fs_state cmd in
let monad_state_to_os_state (ms : monad_state 'impl ret_value) = (match ms with
| Normal_state(fs_st,v) ->
OS_normal (update_pending_return_and_fs_state s0 pid (Value v) fs_st)
| Error_state(fs_st,e) ->
OS_normal (update_pending_return_and_fs_state s0 pid (Error e) fs_st)
| Special_state(spcial,s) -> ( OS_special(spcial,s))
end) in
finset_image monad_state_to_os_state rs
end
(* run an OS-level_command *)
val os_run_os_command : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_os_command ->
ty_os_state 'dir_ref 'file_ref 'impl ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_run_os_command env pid cmd s0 = begin
let ppstate = lookup_per_process_state s0 pid in
let pp path = (
process_path env s0.oss_fs_state ppstate.pps_cwd cmd path
) in
let run_fs_cmd fs_cmd = os_run_fs_command env pid fs_cmd s0 in
(* determinise output of read or write commands *)
let det_rw ss = os_determinise os_determinise_less_read_write pid ss in
let run_os_cmd (cmd : ty_os_command) = (
match cmd with
(* real os-commands *)
| OS_CLOSE fd -> (os_close env pid fd s0)
| OS_OPEN (p,fs,mo) -> (os_open env pid (pp p) fs mo s0)
| OS_UMASK p -> (os_umask pid p s0)
| OS_CHDIR s -> (os_chdir env pid (pp s) s0)
| OS_LSEEK (fd,ofs,c) -> (os_lseek env pid fd ofs c s0)
| OS_OPENDIR p -> (os_opendir env pid (pp p) s0)
| OS_READDIR dh -> (os_readdir env pid dh s0)
| OS_CLOSEDIR dh -> (os_closedir env pid dh s0)
| OS_REWINDDIR dh -> (os_rewinddir env pid dh s0)
(* read and write commands *)
| OS_PREAD (fd,sz,ofs) -> (os_read env pid fd sz (Just ofs) s0)
| OS_EXTENDED_CMD (OS_DET_PREAD (fd,sz,ofs)) -> det_rw (os_read env pid fd sz (Just ofs) s0)
| OS_READ (fd,sz) -> (os_read env pid fd sz Nothing s0)
| OS_EXTENDED_CMD (OS_DET_READ (fd,sz)) -> det_rw (os_read env pid fd sz Nothing s0)
| OS_PWRITE (fd,bs,sz,ofs) -> (os_write env pid fd bs sz (Just ofs) s0)
| OS_EXTENDED_CMD (OS_DET_PWRITE (fd,bs,sz,ofs)) -> det_rw (os_write env pid fd bs sz (Just ofs) s0)
| OS_WRITE (fd,bs,sz) -> (os_write env pid fd bs sz Nothing s0)
| OS_EXTENDED_CMD (OS_DET_WRITE (fd,bs,sz)) -> det_rw (os_write env pid fd bs sz Nothing s0)
(* extended commands *)
| OS_EXTENDED_CMD (OS_ADD_USER_TO_GROUP (u, g)) -> os_add_user_to_group pid u g s0
| OS_EXTENDED_CMD (OS_OPEN_CLOSE (p,fs,p')) -> run_fs_cmd (FS_EXTENDED_CMD (FS_OPEN_CLOSE(pp p, fs, p')))
(* direct mapping to fs-commands *)
| OS_LINK (s,d) -> (run_fs_cmd (FS_LINK(pp s, pp d)))
| OS_MKDIR (s,p) -> (run_fs_cmd (FS_MKDIR(pp s, p)))
| OS_READLINK p -> (run_fs_cmd (FS_READLINK(pp p)))
| OS_RENAME (s,d) -> (run_fs_cmd (FS_RENAME(pp s, pp d)))
| OS_RMDIR p -> (run_fs_cmd (FS_RMDIR(pp p)))
| OS_STAT p -> (run_fs_cmd (FS_STAT(pp p)))
| OS_LSTAT p -> (run_fs_cmd (FS_LSTAT(pp p)))
| OS_SYMLINK (s,d) -> (run_fs_cmd (FS_SYMLINK(bytes_of_cstring s, pp d)))
| OS_TRUNCATE (p,l) -> (run_fs_cmd (FS_TRUNCATE(pp p,l)))
| OS_UNLINK p -> (run_fs_cmd (FS_UNLINK(pp p)))
| OS_CHMOD (s, p) -> (run_fs_cmd (FS_CHMOD (pp s, p)))
| OS_CHOWN (s, u, g) -> (run_fs_cmd (FS_CHOWN (pp s, u, g)))
end) in
run_os_cmd cmd
(* (match cmd with
| OS_POSIX_CMD cmd' -> run_os_cmd false cmd'
| OS_DETERMINISTIC_CMD cmd' -> run_os_cmd true cmd'
end) *)
end
(* [update_env_permissions_for_pid s0 pid env] changes the permission record
field [env_prms] in [env] to be appropriate for running commands for process
[pid] in state [s0]. *)
val update_env_permissions_for_pid : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
environment 'dir_ref 'file_ref 'impl ->
environment 'dir_ref 'file_ref 'impl
let update_env_permissions_for_pid s0 pid env = (
#ifdef aspect_perms
let ppstate = lookup_per_process_state s0 pid in
let uid = ppstate.pps_effective_uid in
let gid = ppstate.pps_effective_gid in
let prms =
if (env.env_perm_ops.pops_uid_is_superuser s0.oss_fs_state uid)
then superuser_permissions env.env_ops uid gid ppstate.pps_file_creation_mask (* coverage:fixme - this will be solved once we run some traces with the --root *)
else uid_permissions env (is_uid_in_gid s0) uid gid ppstate.pps_file_creation_mask
in
<| env with env_prms = prms |>
#else
env
#endif
)
(* [os_trans_pid_core] is the core of [os_trans_pid] it is run, if the process is
blocked and a tau-transition occurs. It is the operation that actually runs the
OS-commands *)
val os_trans_pid_core : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
ty_os_command ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_trans_pid_core env s0 pid cmd = (
(* check that none of the paths in the command starts with exactly two slashes *)
let unsupported_double_slash = (
let archi = architecture_of_ty_arch env.env_arch in
((List.any path_starts_with_exactly_two_slashes (paths_of_ty_os_command cmd))
&& not(archi.arch_abs_path_slash_slash))
) in
if unsupported_double_slash then
finset_singleton (OS_special(Implementation_defined,"path starts with exactly two slashes")) (* coverage:impossible - no supported architecture has arch_abs_path_slash_slash field set to false *)
else (
(* update environment for process FIXME this really needs to be
fixed - the environment should be fixed for a trace, but
unfortunately the per-process permissions are accessed from the
environment (!); better to access the per-process permissions
from the per-process state *)
let env = update_env_permissions_for_pid s0 pid env in
(* do the real work *)
os_run_os_command env pid cmd s0
)
)
val os_trans_pid : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_os_state 'dir_ref 'file_ref 'impl ->
ty_pid ->
os_label ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_trans_pid env s0 (pid:ty_pid) cmd = (
let ppstate = lookup_per_process_state s0 pid in
match (ppstate.pps_pid_run_state,cmd) with
| (RUNNING,(OS_CALL(pid',cmd))) ->
if (pid' <> pid) then
finset_empty ()
else (
finset_singleton (OS_normal (update_run_state s0 pid (BLOCKED_CALL cmd)))
)
| (BLOCKED_CALL(cmd),OS_TAU) -> (os_trans_pid_core env s0 pid cmd)
| (PENDING_RETURN(ev),(OS_RETURN(pid',ev'))) -> (
let success = finset_singleton (OS_normal (update_run_state s0 pid RUNNING)) in
let failure = finset_empty () in
(* if the label is for pid', then we cannot do a transition for process pid *)
if (pid' <> pid) then
failure
else (
if (ev' = ev) then
success
else (
(* we would typically not allow a transition; however,
sometimes we are very nondeterministic (eg size of a
stat'ed directory), in which case we allow the
transition *)
match (ev,ev') with
| (Value(RV_stats s),Value(RV_stats s')) -> (
(* for a file, we are not interested in st_dev, st_ino (FIXME), st_rdev *)
let mask_file s = (<| s with st_dev=0; st_rdev=0; st_ino=(Inode 0) |>) in
(match s.st_kind with
| S_IFREG -> (
if mask_file s = mask_file s' then
success (* allow the transition if the only differences are things we are not interested in *)
else
failure)
| S_IFLNK -> (
if mask_file s = mask_file s' then
success (* allow the transition if the only differences are things we are not interested in *)
else
failure)
| S_IFDIR -> (
let mask_dir s = <| (mask_file s) with st_size=0 |> in
if mask_dir s = mask_dir s' then
success
else
failure)
| _ -> failure end))
| (_,_) -> failure end)))
| (_,_) -> finset_empty ()
end)
(*-------------------------------*)
(* os_trans_pcreate_destroy *)
(*-------------------------------*)
(* a default file-descriptor table that contains dummy file-descriptors for
stdin, stdout and stderr. This means that the next free FD is 3.
These are all mapped to [FID 0]. The os_state should have this fid! *)
val default_pps_fd_table : fmap ty_fd fd_state
let default_pps_fd_table = begin
let stdin_etc = [FD 0 (* stdin *); FD 1 (* stout *); FD 2 (* stderr *)] in
let dummy_fds = <| fds_fid=(FID 0); fds_FD_CLOEXEC=true |> in
let pps_fd_table = List.foldl (fun fdt fd -> fmap_update fdt (fd,dummy_fds)) (fmap_empty ()) stdin_etc in
pps_fd_table
end
(* create a default per_process_state. The cwd needs
to be provided explicitly, because directory refs are
polymorphic. *)
val default_pps : forall 'dir_ref.
uid -> gid -> 'dir_ref -> per_process_state 'dir_ref
let default_pps uid gid cwd = <|
pps_cwd=cwd;
pps_fd_table=default_pps_fd_table;
pps_dh_table=fmap_empty ();
pps_pid_run_state=RUNNING;
(* 022 seems to be the default on most unix systems.
Since the default perms for dirs is 777 and for files are 666
this means permissions rw-r--r-- for files and
rwxr-x-r-x for dirs. Another sometimes used value is 002, which
gives write permissions to the group as well by default. *)
pps_file_creation_mask= File_perm 0O022;
pps_effective_uid = uid;
pps_real_uid = uid;
pps_saved_uid = uid;
pps_effective_gid = gid;
pps_real_gid = gid;
pps_saved_gid = gid;
|>
val create_pps_for_pid : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
uid -> gid -> 'impl -> ty_pid -> per_process_state 'dir_ref
let create_pps_for_pid env uid gid s0 pid = default_pps uid gid (fromJust (env.env_ops.fops_get_root s0))
val os_trans_pcreate_destroy : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_os_state 'dir_ref 'file_ref 'impl ->
os_label ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_trans_pcreate_destroy env s0 lbl = (
match lbl with
| OS_CREATE(pid, uid, gid) -> (
if finset_mem pid (fmap_dom s0.oss_pid_table) then
finset_empty ()
else (
let s0 = <| s0 with oss_pid_table=(fmap_update s0.oss_pid_table (pid,create_pps_for_pid env uid gid s0.oss_fs_state pid)) |> in
finset_singleton (OS_normal s0)))
| OS_DESTROY(pid) ->
if not (finset_mem pid (fmap_dom s0.oss_pid_table)) then
finset_empty ()
else (
let ppstate = fromJust (fmap_lookup s0.oss_pid_table pid) in
(match ppstate.pps_pid_run_state with
| RUNNING -> (
let s0 = <| s0 with oss_pid_table=(fmap_remove s0.oss_pid_table pid) |> in
finset_singleton (OS_normal s0))
| _ -> finset_empty () (* we don't allow processes to be destroyed if they are in kernel *) end)) (* coverage:fixme -we can test this only in a os trace (we need to destroy a process while it is executing) *)
| _ -> finset_empty () end)
(*-------------------------------*)
(* os_trans_tau *)
(*-------------------------------*)
val os_trans_tau : forall 'dir_ref 'file_ref 'impl.
environment 'dir_ref 'file_ref 'impl ->
ty_os_state 'dir_ref 'file_ref 'impl ->
os_label ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_trans_tau env s0 lbl = (
match lbl with
| OS_TAU -> finset_empty () (* (finset_singleton s0) FIXME for testing we want to limit nondet - Tau steps represent internal actions only *)
| _ -> finset_empty () end)
(*-------------------------------*)
(* os_trans *)
(*-------------------------------*)
val os_trans : forall 'dir_ref 'file_ref 'impl.
ty_os_state 'dir_ref 'file_ref 'impl ->
os_label ->
finset (os_state_or_special 'dir_ref 'file_ref 'impl)
let os_trans s0 lbl = (
let env = s0.oss_env in
(* process transitions *)
let pids = fmap_dom s0.oss_pid_table in
let ss = finset_bigunion_image (fun pid -> os_trans_pid env s0 pid lbl) pids in
(* create/ destroy transitions *)
let ss = finset_union ss (os_trans_pcreate_destroy env s0 lbl) in
(* tau transitions *)
let ss = finset_union ss (os_trans_tau env s0 lbl) in
ss)
(*-------------------------------*)
(* os_init_state *)
(*-------------------------------*)
(* convenience initial state with a single process *)
val os_init_state : forall 'dir_ref 'file_ref 'impl.
bool -> (* no root *)
environment 'dir_ref 'file_ref 'impl ->
ty_os_state 'dir_ref 'file_ref 'impl
let os_init_state no_root env = (
let fs0 = env.env_ops.fops_get_init_state() in
let root = fromJust(env.env_ops.fops_get_root fs0) in
(* dummy fid table used by fds for stdin, stdout, stderr*)
let dummy_fid_state = <|
fids_offset=0;
fids_entry=Dir_ref_entry root;
fids_oflags=(finset_empty ());
fids_open_or_closed=FID_OPEN |>
in
let fid_table = fmap_update (fmap_empty ()) (FID 0,dummy_fid_state) in
(* dummy per-process state *)
let ppstate = (
if no_root then
(* create process 1 with "normal" user uid and gid &*)
default_pps (User_id 1) (Group_id 1) root
else
default_pps root_uid root_gid root)
in
(* dummy pid table *)
let pid_table = fmap_update (fmap_empty ()) (Pid 1,ppstate) in
let s0 = <|
oss_pid_table=pid_table;
oss_fid_table=fid_table;
oss_group_table=fmap_empty();
oss_fs_state=fs0;
oss_env=env
|>
in
s0)
(** allowed_results_for_pid is a convenience function used by the testing code *)
(* FIXME not clear what this means when we are nondet on eg size of
a directory; it should be understood that this is the allowable
results "up to some notion of equivalence", where this notion is
defined eg in os_trans_pid_core *)
let allowed_results_for_pid pid s0 = (
let pps_opt = fmap_lookup s0.oss_pid_table pid in
(match pps_opt with
| Nothing -> finset_empty ()
| Just pps -> (match pps.pps_pid_run_state with
| PENDING_RETURN(ev) -> finset_singleton ev
| _ -> finset_empty () end) end))
end