(* $Header: /users/lal/black/hol/Disser/RCS/syscalls.sml,v 1.33 1997/07/16 22:54:54 black Exp $ *)
(* *created  "Wed Aug 16 12:58:43 1995" *by "Paul E. Black" *)
(* *modified "Wed Jul 16 16:28:16 1997" *by "Paul E. Black" *)

(*----------------------------------------------------------------------------
	Semantics of system calls

	These are taken from HP-UX Release 9.0 (August 1992)
 ----------------------------------------------------------------------------*)

(* for description of file system *)
use "state.sml" handle _ => ();

(*----------------------------------------------------------------------------
	Miscellaneous axioms about construction functions.
 ----------------------------------------------------------------------------*)

new_constant{Name = "inodeOf", Ty = ==`:'FILE -> num`==};

(* inodeOf a handle of an inode is that inode *)
(* NOTE: by definition FOPEN_handlefn *always* returns a handle.
   Postconditions should use it only in the "success" branch. *)
val inOf_deref_fopenHndl_I =
    mk_thm([], (--`!(inode:num) (type:string).
			inodeOf (deref (FOPEN_handlefn inode type):'FILE)
								= inode`--));

(* fopen never returns stdout *)
val fopenHandle_not_stdout =
    mk_thm([], (--`!(inode:num) (type:string).
			~(inodeOf (deref (FOPEN_handlefn inode type):'FILE)
							= SYS_stdout)`--));

new_constant{Name = "inodeOfFileDes", Ty = ==`:num -> num`==};

(* file descriptor 1 is stdout *)
val fd_1_stdout =
    mk_thm([], (--`inodeOfFileDes 1 = SYS_stdout`--));

(*---------------------------- int_neg -------------------------------------*)

(* SKIMP - int_neg should return integers *)
new_constant{Name = "int_neg", Ty = ==`:num -> num`==};

(* int_neg is one-to-one *)
val int_neg_one_one =
    mk_thm([], (--`!(i:num) (i':num) .
		(int_neg i:num = int_neg i') = (i = i')`--));

(* int_neg only returns 0 for 0 *)
val int_neg_zero =
    mk_thm([], (--`int_neg 0 = 0`--));

(* int_neg is never greater than 0 *)
val int_neg_nge_zero =
    mk_thm([], (--`!a.~(int_neg a > 0)`--));

(* a useful lemma *)
val int_neg_1_not_0_LEMMA = prove((--`~(int_neg 1 = 0)`--),
	ONCE_REWRITE_TAC [GSYM int_neg_zero] THEN
	REWRITE_TAC [int_neg_one_one] THEN
	ARITH_TAC);

(*--------------------- relative paths in Unix -----------------------------*)

(* resolvePath does all the path stuff: "." means cwd, ".." is cwd's parent
   unless cwd is root, /... starts from root, etc.  resPathRest and dirParent
   are place holders for the rest of the functionality which I don't need to
   define now. *)

new_constant{Name = "resPathRest", Ty = ==`:string->string->string->string`==};

new_constant{Name = "dirParent", Ty = ==`:string->string`==};

val resolvePath = new_definition (
   "resolvePath",
   (--`! (root:string) cwd path .
	resolvePath root cwd path = (
		(path = ".") => cwd |
		(path = "..") =>
			((cwd = root) => root | dirParent cwd)
		| resPathRest root cwd path)`--)
);

(*======================== function axioms =================================*)

(*----------------------------------------------------------------------------
 SYNOPSIS
      int chdir(const char *path);

 DESCRIPTION
      chdir() causes a directory pointed to by path to become the current 
      working directory.

 RETURN VALUE
      Upon successful completion, a value of 0 is returned.  Otherwise, a
      value of -1 is returned and errno is set to indicate the error.

 ERRORS
      chdir() fails and the current working directory remains unchanged if
      one or more of the following are true . . .
 ----------------------------------------------------------------------------*)

val logpath = mk_var{Name="^path",Ty=(==`:string`==)};
val logSYS_cwd = mk_var{Name="^SYS_cwd",Ty=(==`:string`==)};

(* last modified 10Jul97 *)
val SYS_chdir = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "chdir" 0 Int) [Var "path" 0 (Ptr Char)]
     [Var "errno" 0 Int; Var "SYS_cwd" 0 (Ptr Char)] NOBody)
    ((C_Result = 0) /\ (SYS_cwd=^logpath) \/
     (C_Result = int_neg 1) /\ (SYS_cwd=^logSYS_cwd)
				/\ (?CHDIR_errno.errno:num=CHDIR_errno))
`--));

(*----------------------------------------------------------------
	chdir(path) is somewhat equivalent to
		if (nondeterministic==0)
		    C_Result=0;
		else
		    C_Result=1;
		if (C_Result==0)
		    SYS_cwd=path;
		else
		    errno=CHDIR_errno;

    (Func (Var "chdir" 0 Int) [Var "path" 0 (Ptr Char)]
     [Var "errno" 0 Int; Var "SYS_cwd" 0 (Ptr Char);
      Var "nondeterministic" 0 Int]
    (SOMEBody (Block []
    (Seq
     (IfElse (Binary (Lval (Vref (Var "nondeterministic" 0 Int))) Eq
			(Const (CCint 0) Int))
      (Simple (Assign (Vref (Var "C_Result" 0 Int))  (Const (CCint 0) Int)))
      (Simple (Assign (Vref (Var "C_Result" 0 Int))  (Const (CCid "-1") Int))))
     (IfElse (Binary (Lval (Vref (Var "C_Result" 0 Int))) Eq
			(Const (CCint 0) Int))
      (Simple (Assign (Vref (Var "SYS_cwd" 0 (Ptr Char)))
		      (Lval (Vref (Var "path" 0 (Ptr Char))))))
      (Simple (Assign (Vref (Var "errno" 0 Int))
		      (Lval (Vref (Var "CHDIR_errno" 0 (Int)))))))
    ))))

 ----------------------------------------------------------------*)


(*----------------------------------------------------------------------------
 SYNOPSIS
      int chroot(const char *path);

 DESCRIPTION
      chroot() causes the named directory to become the root directory.

      The effective user ID must be a user having appropriate privileges.

 RETURN VALUE
      Upon successful completion, a value of 0 is returned.  Otherwise, a
      value of -1 is returned and errno is set to indicate the error.

 ERRORS
      chroot() fails and the root directory remains unchanged if one or
      more of the following are true . . .
 ----------------------------------------------------------------------------*)

val logSYS_root = mk_var{Name="^SYS_root",Ty=(==`:string`==)};
val logSYS_euid = mk_var{Name="^SYS_euid",Ty=(==`:num`==)};

(* last modified 10Jul97 *)
val SYS_chroot = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "chroot" 0 Int) [Var "path" 0 (Ptr Char)]
     [Var "errno" 0 Int; Var "SYS_cwd" 0 (Ptr Char);
      Var "SYS_root" 0 (Ptr Char); Var "SYS_euid" 0 Int] NOBody)
    (((C_Result = 0) /\
		(SYS_root=resolvePath ^logSYS_root ^logSYS_cwd ^logpath) \/
      (C_Result = int_neg 1) /\ (SYS_root=^logSYS_root)
				/\ (?CHROOT_errno.errno:num=CHROOT_errno)) /\
     (SYS_cwd=^logSYS_cwd) /\ (SYS_euid=^logSYS_euid))
`--));

(*----------------------------------------------------------------------------
 SYNOPSIS
      uid_t geteuid(void);

 DESCRIPTION
      geteuid() returns the effective user ID of the process.
 ----------------------------------------------------------------------------*)

(* last modified 21Mar97 *)
val SYS_geteuid = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "geteuid" 0 Int) [] [] NOBody)
    (C_Result = ^logSYS_euid)
`--));

(* SKIMP - should return uid_t, not num *)


(*----------------------------------------------------------------------------
 SYNOPSIS
      int setuid(uid_t uid);

 DESCRIPTION
      setuid() sets the real user ID, effective user ID, and/or saved
      user ID.

      Summary: if setuid() succeeds, the effective user ID is the uid
      passed.  The real and saved user ID's are set depending on
      complicated conditions.

 RETURN VALUE
      Upon successful completion, setuid() returns 0.  Otherwise it
      returns -1 and sets errno.
 ----------------------------------------------------------------------------*)

val logSYS_ruid = mk_var{Name="^SYS_ruid",Ty=(==`:num`==)};
val logSYS_suid = mk_var{Name="^SYS_suid",Ty=(==`:num`==)};

val loguid = mk_var{Name="^uid",Ty=(==`:num`==)};

(* last modified 11Jul97 *)
val SYS_setuid = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "setuid" 0 Int) [Var "uid" 0 Int]
     [Var "errno" 0 Int; Var "SYS_euid" 0 Int;
      Var "SYS_ruid" 0 Int; Var "SYS_suid" 0 Int] NOBody)
    ((C_Result = int_neg 1) /\ (?SETEUID_errno.errno:num=SETEUID_errno) \/
     (C_Result = 0) /\
     (SYS_euid = ^loguid) /\
     ((SYS_ruid = ^logSYS_ruid) \/ (SYS_ruid = ^loguid)) /\
     ((SYS_suid = ^logSYS_suid) \/ (SYS_suid = ^loguid)))
`--));

(* SKIMP - should take uid_t, not int *)


(*----------------------------------------------------------------------------
 SYNOPSIS
      void exit(int status);

 DESCRIPTION
      exit() terminates the calling process and passes status to the system
      for inspection, ...
 ----------------------------------------------------------------------------*)

(* last modified 17Jan97 *)
val SYS_exit = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "exit" 0 Void) [Var "status" 0 Int] [] NOBody)
    (F)
`--));

(* SKIMP - this should just transfer control (to the end of the program),
   not produce a totally undefined state. *)

(*----------------------------------------------------------------------------
 SYNOPSIS
      int fclose(FILE *stream);

 DESCRIPTION
      fclose() causes any buffered data for the named stream to be written
      out, and the stream to be closed.

 RETURN VALUE
      Upon successful completion, fclose() returns 0.  Otherwise, EOF is
      returned and errno is set to indicate the error.
 ----------------------------------------------------------------------------*)

(* last modified 17Jan97 *)
val SYS_fclose = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "fclose" 0 Int) [Var "stream" 0 (Ptr(Struct "FILE"))]
     [Var "errno" 0 Int] NOBody)
    (T)
`--));


(*----------------------------------------------------------------------------
 SYNOPSIS
      FILE *fopen(const char *pathname, const char *type);

 DESCRIPTION
      fopen() opens the file named by pathname and returns a pointer to it.

 RETURN VALUE
      Upon successful completion, a FILE pointer is returned.  Otherwise, 
      NULL is returned and errno is set to indicate the error.
 ----------------------------------------------------------------------------*)

(* if I enter NULL directly in a term, the parser assumes it is the "empty
  list tester."  So I have to enter NULL indirectly *)
val fpnull = mk_var{Name="NULL",Ty=(==`:'FILE ptr`==)};

val logpathname = mk_var{Name="^pathname",Ty=(==`:string`==)};
val logtype = mk_var{Name="^type",Ty=(==`:string`==)};

(* last modified 11Mar97 *)
val SYS_fopen = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "fopen" 0 (Ptr(Struct "FILE")))
     [Var "pathname" 0 (Ptr Char); Var "type" 0 (Ptr Char)]
     [Var "errno" 0 Int; Var "SYS_cwd" 0 (Ptr Char);
      Var "SYS_root" 0 (Ptr Char)] NOBody)
    ((C_Result = ^fpnull) /\ (?FOPEN_errno.errno:num=FOPEN_errno) \/
     (?FOPEN_handlefn.C_Result =
			FOPEN_handlefn (inodeNamed ^logpathname) ^logtype))
`--));

(*----------------------------------------------------------------
	fopen(pathname, type) is somewhat equivalent to
		if (nondeterministic==0)
		    C_Result=NULL;
		else
		    C_Result=handle(pathname, type);
		if (C_Result==NULL) {
		    errno=FOPEN_errno;
		}
----------------------------------------------------------------*)


(*----------------------------------------------------------------------------
 SYNOPSIS
      int fprintf(FILE *stream, const char *format, ...)

 DESCRIPTION
      fprintf() writes arguments to the named output stream.

 RETURN VALUE
      Return the number of bytes written, or a negative value if
      an output error was encountered.  In some cases, errno is set.

 ----------------------------------------------------------------------------*)

val logformat = mk_var{Name="^format",Ty=(==`:string`==)};
val logstream = mk_var{Name="^stream",Ty=(==`:('FILE)ptr`==)};

(* last modified 30Jun97 *)
val SYS_fprintf = mk_thm ([],
(--`WF_fnp
    (SoFS preFSS ^SYS_FileSystem)
    (Func (Var "fprintf" 0 Int)
     (CONS (Var "stream" 0 (Ptr(Struct "FILE")))
      (CONS (Var "format" 0 (Ptr Char)) varargs))
     [Var "SYS_FileSystem" 0 
		(Struct "(((permission,fscontents)unixFile,num)prod)CArray");
      Var "errno" 0 Int] NOBody)
    ((?FPRINTF_error:num.C_Result = int_neg FPRINTF_error) 
	/\ (inSomeCasesOf C_Result (?FPRINTF_errno.errno:num=FPRINTF_errno)) 
	/\ (SoFS preFSS ^SYS_FileSystem) \/
     (C_Result:num = 0) /\ (SoFS preFSS ^SYS_FileSystem) \/
     C_Result > 0
	/\ (SoFS (\inode fcontents .
		(inode = inodeOf (deref ^logstream)) =>
		    (?prev. preFSS inode prev /\
			(appendFile
			    (printfSpec ^logformat (vargs:'a list):string)
			    prev = fcontents)) |
		    (preFSS inode fcontents))		^SYS_FileSystem))
`--));


(*----------------------------------------------------------------------------
 SYNOPSIS
      int printf(const char *format, ...)

 DESCRIPTION
      printf() writes arguments to the standard output.
 ----------------------------------------------------------------------------*)

(* last modified 30Jun97 *)
val SYS_printf = mk_thm ([],
(--`WF_fnp
    (SoFS preFSS ^SYS_FileSystem)
    (Func (Var "printf" 0 Int) 
     (CONS (Var "format" 0 (Ptr Char)) varargs)
     [Var "SYS_FileSystem" 0 
		(Struct "(((permission,fscontents)unixFile,num)prod)CArray");
      Var "errno" 0 Int] NOBody)
    ((?PRINTF_error:num.C_Result = int_neg PRINTF_error) 
	/\ (inSomeCasesOf C_Result (?PRINTF_errno.errno:num=PRINTF_errno)) 
	/\ (SoFS preFSS ^SYS_FileSystem) \/
     (C_Result = 0) /\ (SoFS preFSS ^SYS_FileSystem) \/
     C_Result > 0
	/\ (SoFS (\inode fcontents .
		(inode = SYS_stdout) =>
		    (?prev. preFSS inode prev /\
			(appendFile
			    (printfSpec ^logformat (vargs:'a list):string)
			    prev = fcontents)) |
		    (preFSS inode fcontents))		^SYS_FileSystem))
`--));


(*----------------------------------------------------------------------------
 SYNOPSIS
      int close(int fildes);

 DESCRIPTION
      close() closes the file descriptor.

 RETURN VALUE
      Upon successful completion, close() returns 0; otherwise, it
      returns -1 and sets errno to indicate the error.
 ----------------------------------------------------------------------------*)

(* last modified 17Jan97 *)
val SYS_close = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "close" 0 Int) [Var "fildes" 0 Int]
     [Var "errno" 0 Int] NOBody)
    ((C_Result = int_neg 1) /\ (?CLOSE_errno.errno:num=CLOSE_errno) \/
     (C_Result = 0))
`--));


(*----------------------------------------------------------------------------
 SYNOPSIS
      int open(const char *pathname, int oflag);

 DESCRIPTION
      open() opens the file named by pathname in the given mode.

 RETURN VALUE
      Upon successful completion, a file descriptor is returned.  Otherwise, 
      -1 is returned and errno is set to indicate the error.
 ----------------------------------------------------------------------------*)

val logoflag = mk_var{Name="^oflag",Ty=(==`:num`==)};

(* last modified 1July97 *)
val SYS_open = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "open" 0 Int) [Var "pathname" 0 (Ptr Char); Var "oflag" 0 Int]
     [Var "errno" 0 Int;
      Var "SYS_cwd" 0 (Ptr Char); Var "SYS_root" 0 (Ptr Char)] NOBody)
    ((C_Result:num = int_neg 1) /\ (?OPEN_errno.errno:num=OPEN_errno) \/
      (?OPEN_fildesfn.C_Result =
	      OPEN_fildesfn (^logpathname) (^logoflag)
						^logSYS_cwd ^logSYS_root))
`--));


(*----------------------------------------------------------------------------
 SYNOPSIS
      size_t read(int fildes, void *buf, size_t nbyte);

 DESCRIPTION
      read() tries to read nbyte bytes from the file descriptor into buf.

 RETURN VALUE
      Upon successful completion, read() returns the number of bytes
      actually read and placed in the buffer; this may be less than nbyte.
      When an end-of-file is reached, a value of 0 is returned.  Otherwise,
      a -1 is returned and errno is set to indicate the error.
 ----------------------------------------------------------------------------*)

val logfildes = mk_var{Name="^fildes", Ty=(==`:num`==)};
val logbuf = mk_var{Name="^buf", Ty=(==`:string`==)};
val lognbyte = mk_var{Name="^nbyte", Ty=(==`:num`==)};

(* the last clause in the postcondition says that if the read 
   succeeded, the file descriptor couldn't have been -1 *)

(* last modified 2July97 *)
val SYS_read = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "read" 0 Int)
     [Var "fildes" 0 Int; Var "buf" 0 (Ptr Char); Var "nbyte" 0 Int]
     [Var "errno" 0 Int] NOBody)
    ((C_Result = int_neg 1) /\ (?READ_errno.errno:num=READ_errno) \/
     (C_Result = 0) \/
     ~(^logfildes = int_neg 1) /\ (C_Result > 0) /\
		(C_Result = readSpec(^logfildes, (^logbuf:string), ^lognbyte)))
`--));


(*----------------------------------------------------------------------------
 SYNOPSIS
      int sscanf(const char *s, const char *format, /* [pointer,] */ ...);

 DESCRIPTION
      sscanf() reads characters from s, interprets them according to the
      format, and stores any results the pointers.

 RETURN VALUE
      If the input ends prematurely, EOF is returned.  Otherwise, sscanf()
      returns the number of successfully assigned input items.
 ----------------------------------------------------------------------------*)

val consteof = mk_var{Name="EOF",Ty=(==`:num`==)};

(* last modified 21Mar97 *)
val SYS_sscanf = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "sscanf" 0 Int)
     (CONS (Var "s" 0 (Ptr Char)) (CONS (Var "format" 0 (Ptr Char)) varargs))
     [] NOBody)
    ((C_Result = ^consteof) \/
     (C_Result = sscanfSpecNum(^logformat)))
`--));

(* SKIMP - this may change memory indicated by pointers *)

(*----------------------------------------------------------------------------
 SYNOPSIS
      ssize_t write(int fildes, const void *buf, size_t nbyte);

 DESCRIPTION
      write() tries to write nbyte bytes from buf into the file descriptor.

 RETURN VALUE
      Upon successful completion, write() returns the number of bytes actually
      written.  Otherwise, -1 is returned and errno is set to indicate the
      error.
 ----------------------------------------------------------------------------*)

(* last modified 3July97 *)
val SYS_write = mk_thm ([],
(--`WF_fnp
    (SoFS preFSS ^SYS_FileSystem)
    (Func (Var "write" 0 Int)
     [Var "fildes" 0 Int; Var "buf" 0 (Ptr Char); Var "nbyte" 0 Int]
     [Var "SYS_FileSystem" 0 
		(Struct "(((permission,fscontents)unixFile,num)prod)CArray");
      Var "errno" 0 Int] NOBody)
    ((C_Result:num = int_neg 1) /\ (?WRITE_errno.errno:num=WRITE_errno)
	/\ (SoFS preFSS ^SYS_FileSystem) \/
     (?WRITE_res.(C_Result=WRITE_res) /\ WRITE_res >= 0 /\ WRITE_res <= nbyte)
	/\ (SoFS (\inode fcontents .
		(inode = inodeOfFileDes ^logfildes) =>
		    (?prev. preFSS inode prev /\
			(appendFile
			    ((writeSpec (^logbuf:string) ^lognbyte):string)
			    prev = fcontents)) |
		    (preFSS inode fcontents))		^SYS_FileSystem))
`--));


(*----------------------------------------------------------------------------
 SYNOPSIS
	struct tm *localtime(time_t *time)

 DESCRIPTION
	Correct for the time zone according to the TZ environment variable
	and convert to (local static?) tm structure.

 RETURN VALUE
	Return a pointer to the tm structure.
 ----------------------------------------------------------------------------*)

(* last modified 17Jan97 *)
val SYS_localtime = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "localtime" 0 (Ptr(Struct "tm"))) [Var "time" 0 (Ptr Int)]
     [Var "TZ" 0 (Struct "TZstruct")] NOBody)
    (?tsptr.C_Result:('tm)ptr = tsptr)
`--));

(* SKIMP - should take (Ptr(Struct `time_t`)) not (Ptr Int) *)

(*----------------------------------------------------------------
	localtime(& time) is somewhat equivalent to
	    static struct tm ts;
	    time_t c = *time;
	    ts.tm_wday = (c/(60*60*24) + 4) MOD 7;	/* day of week */
	    ts.tm_year = c/(60*60*24*365.24) + 1970;
	    c -= (ts.tm_year-1970) * (60*60*24*365.24);
	    ts.tm_yday = c/(60*60*24);			/* day of year */
	    ts.tm_month = c/(60*60*24*30.44);
	    c -= ts.tm_month * (60*60*24*30.44);
	    ts.tm_mday = c/(60*60*24);
	    c -= ts.tm_mday * (60*60*24);
	    ts.tm_hour = c/(60*60);
	    c -= ts.tm_hour * (60*60);
	    ts.tm_min = c/60;
	    c -= ts.tm_min * 60;
	    ts.tm_sec = c;
	    ts.tm_isdst = magic(getenv("TZ"));		/* is DST on? */
	    return &ts;
 ----------------------------------------------------------------*)


(*----------------------------------------------------------------------------
 SYNOPSIS
	size_t strftime(
           char *s,
           size_t maxsize,
           const char *format,
           const struct tm *timeptr
	)

 DESCRIPTION
	Convert the contents of a tm structure to a formatted date 
	and time string.

 RETURN VALUE
	Return the length of the string put in s.  If the string exceeds
	maxsize, return zero; the contents of s are indeterminate.
 ----------------------------------------------------------------------------*)

(* last modified 17Jan97 *)
val SYS_strftime = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "strftime" 0 Int)
     [Var "s" 0 (Ptr Char); Var "maxsize" 0 Int; Var "format" 0 (Ptr Char);
      Var "timeptr" 0 (Ptr (Struct "tm"))]
     [] NOBody)
    ((strlen(strftimeSpec(format:string,(timeptr:('tm)ptr)):string)<maxsize =>
	((C_Result=strlen(s)) /\ (strcmp(s, strftimeSpec(format,timeptr)) = 0))
	| (C_Result = 0))
     /\ (!index.accessed(s, index) ==> index >= 0 /\ index < maxsize))
`--));

(* SKIMP - return value and maxsize should be size_t, not int *)

(*----------------------------------------------------------------------------
 SYNOPSIS
      time_t time(time_t *tloc);

 DESCRIPTION
      time() returns the value of time in seconds since the Epoch.

      If tloc is not a null pointer, the return value is also assigned to
      the object to which it points.

 RETURN VALUE
      Upon successful completion, time() returns the value of time.
      Otherwise, a value of (time_t)-1 is returned and errno is set to
      indicate the error.
 ----------------------------------------------------------------------------*)

(* if I enter NULL directly in a term, the parser assumes it is the "empty
  list tester."  So I have to enter NULL indirectly *)
val npnull = mk_var{Name="NULL", Ty=(==`:num ptr`==)};

val logtloc = mk_var{Name="^tloc", Ty=(==`:num ptr`==)};

(* last modified 27Feb97 *)
val SYS_time = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "time" 0 Int) [Var "tloc" 0 (Ptr Int)]
     [Var "errno" 0 Int] NOBody)
    ((C_Result = int_neg 1) /\ (?TIME_errno.errno:num=TIME_errno) \/
      (?some_time.(C_Result = some_time) /\ C_Result > 0 /\
       (~(^logtloc=^npnull)==>(deref ^logtloc = some_time))))
`--));

(* SKIMP - should return time_t, not num, ie,
	(C_Result = (-1:*time_t) ...
	  should take (Var `tloc` (Ptr(Struct `time_t`))) not (Ptr Int)
*)

(*----------------------------------------------------------------
	time(tloc) is somewhat equivalent to
		if (nondeterministic==0) {
		    C_Result=int_neg 1;
		    errno=TIME_errno;
		} else {
		    some_time = t_o_d+1; /* +1 so some_time is nonzero */
		    C_Result=some_time;
		    if (tloc != NULL)
			*tloc = C_Result;
		}
 ----------------------------------------------------------------*)


(*----------------------------------------------------------------------------
 SYNOPSIS
      int stat(const char *path, struct stat *buf);

 DESCRIPTION
      stat() obtains information about the named file and puts it
      in buf.

 RETURN VALUE
      Upon successful completion, 0 is returned.  Otherwise, -1 is 
      returned and errno is set to indicate the error.
 ----------------------------------------------------------------------------*)

val logpath = mk_var{Name="^path", Ty=(==`:string`==)};
val logbuf = mk_var{Name="^buf", Ty=(==`:'stat ptr`==)};

(* last modified 10July97 *)
val SYS_stat = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "stat" 0 Int)
     [Var "path" 0 (Ptr Char); Var "buf" 0  (Ptr (Struct "stat"))]
     [Var "errno" 0 Int;
      Var "SYS_cwd" 0 (Ptr Char); Var "SYS_root" 0 (Ptr Char)] NOBody)
    (((C_Result = 0) /\
		(deref ^logbuf = statSpec ^logpath ^logSYS_cwd ^logSYS_root) \/
      (C_Result = int_neg 1) /\ (?STAT_errno.errno:num=STAT_errno)) /\
     (SYS_cwd = ^logSYS_cwd) /\ (SYS_root = ^logSYS_root))
`--));

(*----------------------------------------------------------------
	stat(path, &buf) is somewhat equivalent to
		if (nondeterministic==0)
		    C_Result=0;
		else
		    C_Result=1;
		if (C_Result==0)
		    buf = &(statSpec path SYS_cwd SYS_root);
		else
		    errno=STAT_errno;
 ----------------------------------------------------------------*)


(*----------------------------------------------------------------------------
 SYNOPSIS
      int S_ISREG(ushort st_mode);

 DESCRIPTION
      S_ISREG returns true if the file mode indicates a regular file (vs.
      directory, pipe, or special).
 ----------------------------------------------------------------------------*)

(* last modified 17Jan97 *)
val SYS_S_ISREG = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "S_ISREG" 0 Int) [Var "st_mode" 0 Int] [] NOBody)
    ((C_Result = 0) \/ (C_Result = 1))
`--));

(*============================================================================

			   String handling

 ============================================================================*)

val logs1 = mk_var{Name="^s1", Ty=(==`:string`==)};
val logs1Contents = mk_var{Name="^s1Contents", Ty=(==`:ascii list`==)};
val logs2 = mk_var{Name="^s2", Ty=(==`:string`==)};
val logs2Contents = mk_var{Name="^s2Contents", Ty=(==`:ascii list`==)};

(* this probably isn't want we ultimately want, but it will do for now *)
val strderef = new_definition (
    "strderef",
    (--`! s. strderef s = EXPLODE s`--)
);

(*----------------------------------------------------------------------------
 SYNOPSIS
	char *strcat(char *s1, const char *s2)

 DESCRIPTION
	Append s2 to the end of s1.

 RETURN VALUE
        Return a pointer to s1.
 ----------------------------------------------------------------------------*)

(* last modified 10July97 *)
val SYS_strcat = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "strcat" 0 (Ptr Char))
     [Var "s1" 0 (Ptr Char); Var "s2" 0 (Ptr Char)]
     [] NOBody)
    ((C_Result = ^logs1) /\
     strEq(strderef ^logs1:ascii list,
		(strcatSpec(^logs1Contents, ^logs2Contents):ascii list)) /\
     (strderef ^logs2 = ^logs2Contents))
`--));

(*----------------------------------------------------------------------------
 SYNOPSIS
	int strncasecmp(const char *s1, const char *s2, size_t n)

 DESCRIPTION
	Return an integer less than, equal to, or greater than zero,
	depending on whether s1 is less than, equal to, or greater than s2.
	Examine a maximum of n characters.  Null pointers are the same as
	pointers to empty strings.  Characters are folded by _tolower()
	prior to comparison.
 ----------------------------------------------------------------------------*)

(* last modified 10July97 *)
val SYS_strncasecmp = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "strncasecmp" 0 Int)
     [Var "s1" 0 (Ptr Char); Var "s2" 0 (Ptr Char); Var "n" 0 Int]
     [] NOBody)
    ((C_Result:num = strncasecmpSpec((strderef ^logs1:ascii list),
				 (strderef ^logs2:ascii list), (n:num))) /\
     (strderef ^logs1 = ^logs1Contents) /\
     (strderef ^logs2 = ^logs2Contents))
`--));

(*----------------------------------------------------------------------------
 SYNOPSIS
	char *strcpy(char *s1, const char *s2)

 DESCRIPTION
	Copy s2 to s1.

 RETURN VALUE
	Returns a pointer to s1.
 ----------------------------------------------------------------------------*)

(* last modified 10July97 *)
val SYS_strcpy = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "strcpy" 0 (Ptr Char))
     [Var "s1" 0 (Ptr Char); Var "s2" 0 (Ptr Char)]
     [] NOBody)
    ((C_Result = ^logs1) /\
     strEq(strderef ^logs1:ascii list,
		(strcpySpec(^logs1Contents, ^logs2Contents):ascii list)) /\
     (strderef ^logs2 = ^logs2Contents))
`--));

(*----------------------------------------------------------------------------
 SYNOPSIS
	char *strncpy(char *s1, const char *s2, size_t n)

 DESCRIPTION
	Copy exactly n character of s2 to s1.

 RETURN VALUE
	Returns a pointer to s1.
 ----------------------------------------------------------------------------*)

val logn = mk_var{Name="^n", Ty=(==`:num`==)};

(* last modified 10July97 *)
val SYS_strncpy = mk_thm ([],
(--`WF_fnp
    (T)
    (Func (Var "strncpy" 0 (Ptr Char))
     [Var "s1" 0 (Ptr Char); Var "s2" 0 (Ptr Char); Var "n" 0 Int]
     [] NOBody)
    ((C_Result = ^logs1) /\
     strEq(strderef ^logs1:ascii list,
		(strncpySpec(^logs2Contents, ^logn):ascii list)) /\
     (strderef ^logs2 = ^logs2Contents))
`--));

(*----------------------------------------------------------------------------
 SYNOPSIS
	size_t strlen(const char *s)

 DESCRIPTION
	Return the number of characters in s.
 ----------------------------------------------------------------------------*)

val logs = mk_var{Name="^s", Ty=(==`:string`==)};
val logsContents = mk_var{Name="^sContents", Ty=(==`:ascii list`==)};

(* last modified 30May97 *)
val SYS_strlen = mk_thm ([],
(--`WF_fnp
    T
    (Func (Var "strlen" 0 Int)
     [Var "s" 0 (Ptr Char)]
     [] NOBody)
    (C_Result:num = strlenSpec(strderef ^logs:ascii list))
`--));

(* end of $Source: /users/lal/black/hol/Disser/RCS/syscalls.sml,v $ *)