Skip to content

Commit

Permalink
[wasm] First version of System.v3 for WALI
Browse files Browse the repository at this point in the history
  • Loading branch information
titzer committed Dec 27, 2023
1 parent 80e44d9 commit 4d1ed36
Show file tree
Hide file tree
Showing 9 changed files with 715 additions and 142 deletions.
2 changes: 1 addition & 1 deletion aeneas/src/main/Version.v3
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,6 @@

// Updated by VCS scripts. DO NOT EDIT.
component Version {
def version: string = "III-7.1677";
def version: string = "III-7.1678";
var buildData: string;
}
4 changes: 3 additions & 1 deletion aeneas/src/wasm/WasmTarget.v3
Original file line number Diff line number Diff line change
Expand Up @@ -588,7 +588,9 @@ class WasmProgram(mach: MachProgram, gcTypes: bool, context: SsaContext) {
var ri_init = mach.runtime.getRiInit();
var ri_exit = mach.runtime.getRiExit();
if (ri_init != null || ri_exit != null) {
var sig = if(ri_init != null, ri_init.sig, Signature.new(null, [], [Int.TYPE]));
var params: Array<Type> = if(ri_init != null, ri_init.sig.paramTypes, TypeUtil.NO_TYPES);
var results: Array<Type> = if(ri_exit != null, ri_exit.sig.returnTypes, [Int.TYPE]);
var sig = Signature.new(null, params, results);
sigIndex_entryStub = int.!(addSig(Void.TYPE, sig));
entryStubFuncIndex = numFunctions++;
}
Expand Down
9 changes: 9 additions & 0 deletions bin/dev/v3c-wali
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#!/bin/bash
HERE=$(dirname ${BASH_SOURCE[0]})
BIN=$(cd $HERE/../ && pwd)
RT=$(cd $BIN/../rt/ && pwd)
V3C=${V3C:=$BIN/v3c}
N="$RT/native/"
W="$RT/wali/"
RT_FILES=$(echo $W/*.v3 $N/NativeGlobalsScanner.v3 $N/NativeFileStream.v3 $RT/gc/*.v3)
exec $V3C -entry-export="_start" -heap-size=100m -target=wasm -rt.gc -rt.gctables -rt.files="$RT_FILES" "$@"
322 changes: 322 additions & 0 deletions rt/wali/LinuxConst.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,322 @@
// Copyright 2021 Ben L. Titzer, Virgil Authors. All rights reserved.
// See LICENSE for details of Apache 2.0 license.

// Defines constants associated with (x86-64) Linux system calls.
// XXX: some duplication with constants from other platforms.
component LinuxConst {
// Standard file descriptors.
def STDIN = 0;
def STDOUT = 1;
def STDERR = 2;
// Maximum length of a path.
def MAXPATHLEN = 1024;
// Constants associated with open().
def O_RDONLY = 0; // open read-only
def O_WRONLY = 1; // open write-only
def O_RDWR = 2; // open read-write
def O_NONBLOCK = 0x0800; // no delay
def O_APPEND = 0x0400; // set append mode
def O_SYNC = 0x1000; // synch I/O file integrity
def O_ASYNC = 0x2000; // signal pgrp when data ready
def O_CREAT = 0x0040; // create if nonexistent
def O_TRUNC = 0x0200; // truncate to zero length
def O_EXCL = 0x0080; // error if already exists
def O_NOCTTY = 0x0100; // don't assign controlling terminal

// Constants for networking
def AF_UNSPEC = 0x0;
def AF_UNIX = 0x1;
def AF_INET = 0x2;
def AF_INET6 = 0xA;
def SOCK_STREAM = 0x1;
def SOCK_DGRAM = 0x2;
def SOCK_NONBLOCK = 0x0800;
def SOCK_CLOEXEC = 0x8000;
def SOCKADDR_V4_SIZE = 16;
def SOCKADDR_V6_SIZE = 28;
def SOCKADDR_UNIX_SIZE = 110;
def SOCKADDR_STORAGE_SIZE = 128;

// Constants for lseek().
def SEEK_SET = 0;
def SEEK_CUR = 1;
def SEEK_END = 2;
// Constants for mmap.
def PROT_READ = 0x1;
def PROT_WRITE = 0x2;
def PROT_EXEC = 0x4;
def PROT_NONE = 0x0;
def MAP_SHARED = 0x1;
def MAP_PRIVATE = 0x2;
def MAP_FIXED = 0x10;
def MAP_ANONYMOUS = 0x20;

// TODO: word offset of st_size in statbuf
def STAT_BUF_SIZE = 144;
def STAT_WOFF_ST_SIZE = 6;

def error(val: int, description: string) -> int {
// TODO: record the description in a table
return val;
}

// Linux definitions of errno
// Operation not permitted
def EPERM = 1;
// No such file or directory
def ENOENT = 2;
// No such process
def ESRCH = 3;
// Interrupted system call
def EINTR = 4;
// I/O error
def EIO = 5;
// No such device or address
def ENXIO = 6;
// Argument list too long
def E2BIG = 7;
// Exec format error
def ENOEXEC = 8;
// Bad file number
def EBADF = 9;
// No child processes
def ECHILD = 10;
// Try again
def EAGAIN = 11;
// Out of memory
def ENOMEM = 12;
// Permission denied
def EACCES = 13;
// Bad address
def EFAULT = 14;
// Block device required
def ENOTBLK = 15;
// Device or resource busy
def EBUSY = 16;
// File exists
def EEXIST = 17;
// Cross-device link
def EXDEV = 18;
// No such device
def ENODEV = 19;
// Not a directory
def ENOTDIR = 20;
// Is a directory
def EISDIR = 21;
// Invalid argument
def EINVAL = 22;
// File table overflow
def ENFILE = 23;
// Too many open files
def EMFILE = 24;
// Not a typewriter
def ENOTTY = 25;
// Text file busy
def ETXTBSY = 26;
// File too large
def EFBIG = 27;
// No space left on device
def ENOSPC = 28;
// Illegal seek
def ESPIPE = 29;
// Read-only file system
def EROFS = 30;
// Too many links
def EMLINK = 31;
// Broken pipe
def EPIPE = 32;
// Math argument out of domain of func
def EDOM = 33;
// Math result not representable
def ERANGE = 34;
// Resource deadlock would occur
def EDEADLK = 35;
// File name too long
def ENAMETOOLONG = 36;
// No record locks available
def ENOLCK = 37;
// Function not implemented
def ENOSYS = 38;
// Directory not empty
def ENOTEMPTY = 39;
// Too many symbolic links encountered
def ELOOP = 40;
// No message of desired type
def ENOMSG = 42;
// Identifier removed
def EIDRM = 43;
// Channel number out of range
def ECHRNG = 44;
// Level 2 not synchronized
def EL2NSYNC = 45;
// Level 3 halted
def EL3HLT = 46;
// Level 3 reset
def EL3RST = 47;
// Link number out of range
def ELNRNG = 48;
// Protocol driver not attached
def EUNATCH = 49;
// No CSI structure available
def ENOCSI = 50;
// Level 2 halted
def EL2HLT = 51;
// Invalid exchange
def EBADE = 52;
// Invalid request descriptor
def EBADR = 53;
// Exchange full
def EXFULL = 54;
// No anode
def ENOANO = 55;
// Invalid request code
def EBADRQC = 56;
// Invalid slot
def EBADSLT = 57;
// Bad font file format
def EBFONT = 59;
// Device not a stream
def ENOSTR = 60;
// No data available
def ENODATA = 61;
// Timer expired
def ETIME = 62;
// Out of streams resources
def ENOSR = 63;
// Machine is not on the network
def ENONET = 64;
// Package not installed
def ENOPKG = 65;
// Object is remote
def EREMOTE = 66;
// Link has been severed
def ENOLINK = 67;
// Advertise error
def EADV = 68;
// Srmount error
def ESRMNT = 69;
// Communication error on send
def ECOMM = 70;
// Protocol error
def EPROTO = 71;
// Multihop attempted
def EMULTIHOP = 72;
// RFS specific error
def EDOTDOT = 73;
// Not a data message
def EBADMSG = 74;
// Value too large for defined data type
def EOVERFLOW = 75;
// Name not unique on network
def ENOTUNIQ = 76;
// File descriptor in bad state
def EBADFD = 77;
// Remote address changed
def EREMCHG = 78;
// Can not access a needed shared library
def ELIBACC = 79;
// Accessing a corrupted shared library
def ELIBBAD = 80;
// .lib section in a.out corrupted
def ELIBSCN = 81;
// Attempting to link in too many shared libraries
def ELIBMAX = 82;
// Cannot exec a shared library directly
def ELIBEXEC = 83;
// Illegal byte sequence
def EILSEQ = 84;
// Interrupted system call should be restarted
def ERESTART = 85;
// Streams pipe error
def ESTRPIPE = 86;
// Too many users
def EUSERS = 87;
// Socket operation on non-socket
def ENOTSOCK = 88;
// Destination address required
def EDESTADDRREQ = 89;
// Message too long
def EMSGSIZE = 90;
// Protocol wrong type for socket
def EPROTOTYPE = 91;
// Protocol not available
def ENOPROTOOPT = 92;
// Protocol not supported
def EPROTONOSUPPORT = 93;
// Socket type not supported
def ESOCKTNOSUPPORT = 94;
// Operation not supported on transport endpoint
def EOPNOTSUPP = 95;
// Protocol family not supported
def EPFNOSUPPORT = 96;
// Address family not supported by protocol
def EAFNOSUPPORT = 97;
// Address already in use
def EADDRINUSE = 98;
// Cannot assign requested address
def EADDRNOTAVAIL = 99;
// Network is down
def ENETDOWN = 100;
// Network is unreachable
def ENETUNREACH = 101;
// Network dropped connection because of reset
def ENETRESET = 102;
// Software caused connection abort
def ECONNABORTED = 103;
// Connection reset by peer
def ECONNRESET = 104;
// No buffer space available
def ENOBUFS = 105;
// Transport endpoint is already connected
def EISCONN = 106;
// Transport endpoint is not connected
def ENOTCONN = 107;
// Cannot send after transport endpoint shutdown
def ESHUTDOWN = 108;
// Too many references: cannot splice
def ETOOMANYREFS = 109;
// Connection timed out
def ETIMEDOUT = 110;
// Connection refused
def ECONNREFUSED = 111;
// Host is down
def EHOSTDOWN = 112;
// No route to host
def EHOSTUNREACH = 113;
// Operation already in progress
def EALREADY = 114;
// Operation now in progress
def EINPROGRESS = 115;
// Stale NFS file handle
def ESTALE = 116;
// Structure needs cleaning
def EUCLEAN = 117;
// Not a XENIX named type file
def ENOTNAM = 118;
// No XENIX semaphores available
def ENAVAIL = 119;
// Is a named type file
def EISNAM = 120;
// Remote I/O error
def EREMOTEIO = 121;
// Quota exceeded
def EDQUOT = 122;
// No medium found
def ENOMEDIUM = 123;
// Wrong medium type
def EMEDIUMTYPE = 124;
// Operation Canceled
def ECANCELED = 125;
// Required key not available
def ENOKEY = 126;
// Key has expired
def EKEYEXPIRED = 127;
// Key has been revoked
def EKEYREVOKED = 128;
// Key was rejected by service
def EKEYREJECTED = 129;
// Owner died
def EOWNERDEAD = 130;
// State not recoverable
def ENOTRECOVERABLE = 131;
}
39 changes: 39 additions & 0 deletions rt/wali/RiRuntime.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
// Copyright 2023 Virgil authors. All rights reserved.
// See LICENSE for details of Apache 2.0 license.

component RiRuntime {
var gcInit: void -> void;
var gcCollect: (int, Pointer, Pointer) -> Pointer;
// Called from the exported, generated "entry" stub and used to
// construct the arguments to pass to main.
def init() -> Array<string> {
if (gcInit != null) gcInit();
// Allocate strings for arguments
var argc = wali.cl_get_argc();
var args = Array<string>.new(int.!(argc - 1u));
for (i = 1u; i < argc; i++) {
var len = wali.cl_get_argv_len(i);
var str = Array<byte>.new(int.!(len));
wali.cl_copy_argv(Pointer.atContents(str), i);
args[i - 1u] = str;
}
return args;
}
// Called from the generated allocation stub upon allocation failure.
def gc(size: int, ip: Pointer, sp: Pointer) -> Pointer {
var shadowStackStart = Pointer.NULL, shadowStackEnd = Pointer.NULL; // TODO(titzer)
if (gcCollect != null) return gcCollect(size, shadowStackStart, shadowStackEnd);
System.error("HeapOverflow", "no garbage collector installed");
return Pointer.NULL; // unreachable
}
// Called when main() returns
def exit(code: int) {
wali.SYS_exit(code);
}
def fatalException(ex: string, msg: string, ip: Pointer, sp: Pointer) {
System.err.putc('!').puts(ex);
if (msg != null) System.err.puts(": ").puts(msg).ln();
else System.err.ln();
System.error(ex, msg);
}
}
Loading

0 comments on commit 4d1ed36

Please sign in to comment.