summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64/Makefile2
-rw-r--r--language/bytecode.ott9
-rw-r--r--lib/arith.sail4
-rw-r--r--lib/elf.c390
-rw-r--r--lib/elf.h5
-rw-r--r--lib/rts.c329
-rw-r--r--lib/rts.h116
-rw-r--r--lib/sail.c1003
-rw-r--r--lib/sail.h1408
-rw-r--r--lib/smt.sail4
-rw-r--r--lib/vector_dec.sail9
-rw-r--r--mips/Makefile2
-rw-r--r--mips/main.sail5
-rw-r--r--mips/prelude.sail6
-rw-r--r--riscv/platform_impl.ml2
-rw-r--r--src/bitfield.ml79
-rw-r--r--src/bytecode_util.ml21
-rw-r--r--src/c_backend.ml528
-rw-r--r--src/sail.ml3
-rw-r--r--src/sail_lib.ml4
-rw-r--r--src/value.ml3
-rw-r--r--test/c/assign_rename_bug.expect28
-rw-r--r--test/c/assign_rename_bug.sail35
-rw-r--r--test/c/read_write_ram.expect1
-rw-r--r--test/c/read_write_ram.sail29
-rwxr-xr-xtest/c/run_tests.sh2
-rwxr-xr-xtest/ocaml/run_tests.sh2
27 files changed, 2640 insertions, 1389 deletions
diff --git a/aarch64/Makefile b/aarch64/Makefile
index 58281dc7..07bc67ae 100644
--- a/aarch64/Makefile
+++ b/aarch64/Makefile
@@ -8,7 +8,7 @@ aarch64.c: no_vector.sail
$(SAIL) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c
aarch64_c: aarch64.c
- gcc -O2 $^ -o aarch64_c -lgmp -L $(SAIL_DIR)/lib
+ gcc -O2 $^ -o aarch64_c -lgmp -I $(SAIL_DIR)/lib
aarch64: no_vector.sail
$(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
diff --git a/language/bytecode.ott b/language/bytecode.ott
index 704bda83..895ac34b 100644
--- a/language/bytecode.ott
+++ b/language/bytecode.ott
@@ -65,11 +65,11 @@ fragment :: 'F_' ::=
ctyp :: 'CT_' ::=
{{ com C type }}
- | mpz_t :: :: mpz
+ | mpz_t :: :: int
% Arbitrary precision GMP integer, mpz_t in C. }}
- | bv_t ( bool ) :: :: bv
+ | bv_t ( bool ) :: :: bits
% Variable length bitvector - flag represents direction, true - dec or false - inc }}
- | 'uint64_t' ( nat , bool ) :: :: uint64
+ | 'uint64_t' ( nat , bool ) :: :: bits64
% Fixed length bitvector that fits within a 64-bit word. - int
% represents length, and flag is the same as CT_bv. }}
| 'int64_t' :: :: int64
@@ -122,7 +122,6 @@ iannot :: 'IA_' ::=
instr :: 'I_' ::=
{{ aux _ iannot }}
| ctyp id :: :: decl
- | alloc ctyp id :: :: alloc
| ctyp id = cval :: :: init
| if ( cval ) { instr0 ; ... ; instrn }
else { instr0 ; ... ; instrm } : ctyp :: :: if
@@ -150,8 +149,6 @@ cdef :: 'CDEF_' ::=
| ctype_def :: :: type
| let nat ( id0 : ctyp0 , ... , idn : ctypn ) = {
instr0 ; ... ; instrm
- } {
- instr0 ; ... ; instri
} :: :: let
% The first list of instructions creates up the global letbinding, the
% second kills it.
diff --git a/lib/arith.sail b/lib/arith.sail
index f713805a..e5d2d6ea 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -54,7 +54,7 @@ val div_int = {
smt: "div",
ocaml: "quotient",
lem: "integerDiv",
- c: "div_int",
+ c: "tdiv_int",
coq: "Z.quot"
} : (int, int) -> int
@@ -64,7 +64,7 @@ val mod_int = {
smt: "mod",
ocaml: "modulus",
lem: "integerMod",
- c: "mod_int",
+ c: "tmod_int",
coq: "Z.rem"
} : (int, int) -> int
diff --git a/lib/elf.c b/lib/elf.c
new file mode 100644
index 00000000..566ca96a
--- /dev/null
+++ b/lib/elf.c
@@ -0,0 +1,390 @@
+////////////////////////////////////////////////////////////////
+// ELF Loader
+////////////////////////////////////////////////////////////////
+
+// Header files for simulator
+#include "elf.h"
+#include "rts.h"
+#include "sail.h"
+
+// Use the zlib library to uncompress ELF.gz files
+#include <zlib.h>
+
+// Define ELF constants/types. These come from the
+// Tool Interface Standard Executable and Linking Format Specification 1.2
+
+typedef uint32_t Elf32_Addr;
+typedef uint16_t Elf32_Half;
+typedef uint32_t Elf32_Off;
+typedef uint32_t Elf32_Word;
+
+typedef uint64_t Elf64_Addr;
+typedef uint16_t Elf64_Half;
+typedef uint64_t Elf64_Off;
+typedef uint32_t Elf64_Word;
+typedef uint64_t Elf64_Xword;
+
+/* Type for section indices, which are 16-bit quantities. */
+typedef uint16_t Elf32_Section;
+typedef uint16_t Elf64_Section;
+
+/* Type for version symbol information. */
+typedef Elf32_Half Elf32_Versym;
+typedef Elf64_Half Elf64_Versym;
+
+// Big-Endian support functions which reverse values
+
+uint16_t rev16(uint16_t x) {
+ uint16_t a = (x >> 0) & 0xff;
+ uint16_t b = (x >> 8) & 0xff;
+ return (a << 8) | (b << 0);
+}
+
+uint32_t rev32(uint32_t x) {
+ uint32_t a = (x >> 0) & 0xff;
+ uint32_t b = (x >> 8) & 0xff;
+ uint32_t c = (x >> 16) & 0xff;
+ uint32_t d = (x >> 24) & 0xff;
+ return (a << 24) | (b << 16) | (c << 8) | (d << 0);
+}
+
+uint64_t rev64(uint64_t x) {
+ uint64_t a = (x >> 0) & 0xff;
+ uint64_t b = (x >> 8) & 0xff;
+ uint64_t c = (x >> 16) & 0xff;
+ uint64_t d = (x >> 24) & 0xff;
+ uint64_t e = (x >> 32) & 0xff;
+ uint64_t f = (x >> 40) & 0xff;
+ uint64_t g = (x >> 48) & 0xff;
+ uint64_t h = (x >> 56) & 0xff;
+ return (a << 56) | (b << 48) | (c << 40) | (d << 32) | (e << 24) | (f << 16) | (g << 8) | (h << 0);
+}
+
+// Endian support macros which reverse values on big-endian machines
+// (We assume that the host machine is little-endian)
+
+#define rdAddr32(le, x) ((le) ? (x) : rev32(x))
+#define rdHalf32(le, x) ((le) ? (x) : rev16(x))
+#define rdOff32(le, x) ((le) ? (x) : rev32(x))
+#define rdWord32(le, x) ((le) ? (x) : rev32(x))
+
+#define rdAddr64(le, x) ((le) ? (x) : rev64(x))
+#define rdHalf64(le, x) ((le) ? (x) : rev16(x))
+#define rdOff64(le, x) ((le) ? (x) : rev64(x))
+#define rdWord64(le, x) ((le) ? (x) : rev32(x))
+#define rdXword64(le, x) ((le) ? (x) : rev64(x))
+
+
+#define EI_NIDENT 16 /* Size of e_ident */
+
+#define EI_MAG0 0 /* Offsets in e_ident */
+#define EI_MAG1 1
+#define EI_MAG2 2
+#define EI_MAG3 3
+#define EI_CLASS 4
+#define EI_DATA 5
+
+#define ELFMAG0 0x7f /* Magic string */
+#define ELFMAG1 'E'
+#define ELFMAG2 'L'
+#define ELFMAG3 'F'
+
+#define ELFCLASS32 1 /* 32-bit ELF */
+#define ELFCLASS64 2 /* 64-bit ELF */
+
+#define ELFDATA2LSB 1 /* Little-endian ELF */
+
+#define ET_EXEC 2 /* Executable file */
+
+#define EM_ARM 0x0028 /* 32-bit ARM */
+#define EM_AARCH64 0x00B7 /* 64-bit ARM */
+
+#define PT_LOAD 1 /* Loadable segment */
+
+#define SHT_SYMTAB 2 /* Symbol table type */
+
+/* How to extract and insert information held in the st_info field. */
+
+#define ELF32_ST_BIND(val) (((unsigned char) (val)) >> 4)
+#define ELF32_ST_TYPE(val) ((val) & 0xf)
+#define ELF32_ST_INFO(bind, type) (((bind) << 4) + ((type) & 0xf))
+
+/* Both Elf32_Sym and Elf64_Sym use the same one-byte st_info field. */
+#define ELF64_ST_BIND(val) ELF32_ST_BIND (val)
+#define ELF64_ST_TYPE(val) ELF32_ST_TYPE (val)
+#define ELF64_ST_INFO(bind, type) ELF32_ST_INFO ((bind), (type))
+
+
+/* Legal values for ST_TYPE subfield of st_info (symbol type). */
+
+#define STT_NOTYPE 0 /* Symbol type is unspecified */
+#define STT_OBJECT 1 /* Symbol is a data object */
+#define STT_FUNC 2 /* Symbol is a code object */
+#define STT_SECTION 3 /* Symbol associated with a section */
+#define STT_FILE 4 /* Symbol's name is file name */
+#define STT_COMMON 5 /* Symbol is a common data object */
+#define STT_TLS 6 /* Symbol is thread-local data object*/
+#define STT_NUM 7 /* Number of defined types. */
+#define STT_LOOS 10 /* Start of OS-specific */
+#define STT_GNU_IFUNC 10 /* Symbol is indirect code object */
+#define STT_HIOS 12 /* End of OS-specific */
+#define STT_LOPROC 13 /* Start of processor-specific */
+#define STT_HIPROC 15 /* End of processor-specific */
+
+
+typedef struct
+{
+ uint8_t e_ident[EI_NIDENT]; /* ELF file identifier */
+ Elf32_Half e_type; /* Object file type */
+ Elf32_Half e_machine; /* Processor architecture */
+ Elf32_Word e_version; /* Object file version */
+ Elf32_Addr e_entry; /* Entry point (loader jumps to this virtual address if != 0) */
+ Elf32_Off e_phoff; /* Program header table offset */
+ Elf32_Off e_shoff; /* Section header table offset */
+ Elf32_Word e_flags; /* Processor-specific flags */
+ Elf32_Half e_ehsize; /* ELF header size */
+ Elf32_Half e_phentsize; /* Size of a single program header */
+ Elf32_Half e_phnum; /* Number of program headers in table */
+ Elf32_Half e_shensize; /* Size of a single section header */
+ Elf32_Half e_shnum; /* Number of section headers in table */
+ Elf32_Half e_shtrndx; /* Index of string table in section header table */
+} Elf32_Ehdr;
+
+typedef struct
+{
+ Elf32_Word p_type; /* Segment type */
+ Elf32_Off p_offset; /* Segment offset in file */
+ Elf32_Addr p_vaddr; /* Segment load virtual address */
+ Elf32_Addr p_paddr; /* Segment load physical address */
+ Elf32_Word p_filesz; /* Segment size in file */
+ Elf32_Word p_memsz; /* Segment size in memory. Must be >= p_filesz. If > p_filesz, zero pad */
+ Elf32_Word p_flags; /* Segment flags */
+ Elf32_Word p_align; /* Segment alignment */
+} Elf32_Phdr;
+
+typedef struct
+{
+ uint8_t e_ident[EI_NIDENT]; /* ELF file identifier */
+ Elf64_Half e_type; /* Object file type */
+ Elf64_Half e_machine; /* Processor architecture */
+ Elf64_Word e_version; /* Object file version */
+ Elf64_Addr e_entry; /* Entry point (loader jumps to this virtual address if != 0) */
+ Elf64_Off e_phoff; /* Program header table offset */
+ Elf64_Off e_shoff; /* Section header table offset */
+ Elf64_Word e_flags; /* Processor-specific flags */
+ Elf64_Half e_ehsize; /* ELF header size */
+ Elf64_Half e_phentsize; /* Size of a single program header */
+ Elf64_Half e_phnum; /* Number of program headers in table */
+ Elf64_Half e_shensize; /* Size of a single section header */
+ Elf64_Half e_shnum; /* Number of section headers in table */
+ Elf64_Half e_shtrndx; /* Index of string table in section header table */
+} Elf64_Ehdr;
+
+typedef struct
+{
+ Elf64_Word p_type; /* Segment type */
+ Elf64_Word p_flags; /* Segment flags */
+ Elf64_Off p_offset; /* Segment offset in file */
+ Elf64_Addr p_vaddr; /* Segment load virtual address */
+ Elf64_Addr p_paddr; /* Segment load physical address */
+ Elf64_Xword p_filesz; /* Segment size in file */
+ Elf64_Xword p_memsz; /* Segment size in memory. Must be >= p_filesz.
+ If > p_filesz, zero pad memory */
+ Elf64_Xword p_align; /* Segment alignment */
+} Elf64_Phdr;
+
+typedef struct
+{
+ Elf32_Word sh_name; /* Section name (string tbl index) */
+ Elf32_Word sh_type; /* Section type */
+ Elf32_Word sh_flags; /* Section flags */
+ Elf32_Addr sh_addr; /* Section virtual addr at execution */
+ Elf32_Off sh_offset; /* Section file offset */
+ Elf32_Word sh_size; /* Section size in bytes */
+ Elf32_Word sh_link; /* Link to another section */
+ Elf32_Word sh_info; /* Additional section information */
+ Elf32_Word sh_addralign; /* Section alignment */
+ Elf32_Word sh_entsize; /* Entry size if section holds table */
+} Elf32_Shdr;
+
+typedef struct
+{
+ Elf64_Word sh_name; /* Section name (string tbl index) */
+ Elf64_Word sh_type; /* Section type */
+ Elf64_Xword sh_flags; /* Section flags */
+ Elf64_Addr sh_addr; /* Section virtual addr at execution */
+ Elf64_Off sh_offset; /* Section file offset */
+ Elf64_Xword sh_size; /* Section size in bytes */
+ Elf64_Word sh_link; /* Link to another section */
+ Elf64_Word sh_info; /* Additional section information */
+ Elf64_Xword sh_addralign; /* Section alignment */
+ Elf64_Xword sh_entsize; /* Entry size if section holds table */
+} Elf64_Shdr;
+
+/* Symbol table entry. */
+
+typedef struct
+{
+ Elf32_Word st_name; /* Symbol name (string tbl index) */
+ Elf32_Addr st_value; /* Symbol value */
+ Elf32_Word st_size; /* Symbol size */
+ uint8_t st_info; /* Symbol type and binding */
+ uint8_t st_other; /* Symbol visibility */
+ Elf32_Section st_shndx; /* Section index */
+} Elf32_Sym;
+
+typedef struct
+{
+ Elf64_Word st_name; /* Symbol name (string tbl index) */
+ uint8_t st_info; /* Symbol type and binding */
+ uint8_t st_other; /* Symbol visibility */
+ Elf64_Section st_shndx; /* Section index */
+ Elf64_Addr st_value; /* Symbol value */
+ Elf64_Xword st_size; /* Symbol size */
+} Elf64_Sym;
+
+void loadBlock32(const char* buffer, Elf32_Off off, Elf32_Addr addr, Elf32_Word filesz, Elf32_Word memsz) {
+ //// std::cout << "Loading block from " << off << " to " << addr << "+:" << filesz << std::endl;
+ for(Elf32_Off i = 0; i < filesz; ++i) {
+ //// std::cout << "Writing " << (int)buffer[off+i] << " to " << addr+i << std::endl;
+ write_mem(addr+i, 0xff & buffer[off+i]);
+ }
+ // Zero fill if p_memsz > p_filesz
+ for(Elf32_Off i = filesz; i < memsz; ++i) {
+ write_mem(addr+i, 0);
+ }
+}
+
+void loadProgHdr32(bool le, const char* buffer, Elf32_Off off, const int total_file_size) {
+ //// std::cout << "Loading program header at " << off << std::endl;
+ if (off > total_file_size - sizeof(Elf32_Phdr)) {
+ // // std::cout << "Invalid ELF file, section header overruns end of file" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+ Elf32_Phdr *phdr = (Elf32_Phdr*) &buffer[off];
+ // Only PT_LOAD segments should be loaded;
+ if (rdWord32(le, phdr->p_type) == PT_LOAD) {
+ Elf32_Off off = rdOff32(le, phdr->p_offset);
+ Elf32_Word filesz = rdWord32(le, phdr->p_filesz);
+ if (filesz > total_file_size - off) {
+ // // std::cout << "Invalid ELF file, section overruns end of file" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+ loadBlock32(buffer, off, rdAddr32(le, phdr->p_paddr), filesz, rdWord32(le, phdr->p_memsz));
+ }
+}
+
+void loadBlock64(const char* buffer, Elf64_Off off, Elf64_Addr addr, Elf64_Word filesz, Elf64_Word memsz) {
+ //// std::cout << "Loading block from " << off << " to " << addr << "+:" << filesz << std::endl;
+ for(Elf64_Off i = 0; i < filesz; ++i) {
+ //// std::cout << "Writing " << (int)buffer[off+i] << " to " << addr+i << std::endl;
+ write_mem(addr+i, 0xff & buffer[off+i]);
+ }
+ // Zero fill if p_memsz > p_filesz
+ for(Elf64_Off i = filesz; i < memsz; ++i) {
+ write_mem(addr+i, 0);
+ }
+}
+
+void loadProgHdr64(bool le, const char* buffer, Elf64_Off off, const int total_file_size) {
+ //// std::cout << "Loading program header at " << off << std::endl;
+ if (off > total_file_size - sizeof(Elf64_Phdr)) {
+ //// std::cout << "Invalid ELF file, section header overruns end of file" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+ Elf64_Phdr *phdr = (Elf64_Phdr*) &buffer[off];
+ // Only PT_LOAD segments should be loaded;
+ if (rdWord64(le, phdr->p_type) == PT_LOAD) {
+ Elf64_Off off = rdOff64(le, phdr->p_offset);
+ Elf64_Word filesz = rdXword64(le, phdr->p_filesz);
+ if (filesz > total_file_size - off) {
+ // // std::cout << "Invalid ELF file, section overruns end of file" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+ loadBlock64(buffer, off, rdAddr64(le, phdr->p_paddr), filesz, rdXword64(le, phdr->p_memsz));
+ }
+}
+
+void loadELFHdr(const char* buffer, const int total_file_size) {
+ if (total_file_size < sizeof(Elf32_Ehdr)) {
+ // std::cout << "File too small, not big enough even for 32-bit ELF header" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+ Elf32_Ehdr *hdr = (Elf32_Ehdr*) &buffer[0]; // both Elf32 and Elf64 have same magic
+ if (hdr->e_ident[EI_MAG0] != ELFMAG0 ||
+ hdr->e_ident[EI_MAG1] != ELFMAG1 ||
+ hdr->e_ident[EI_MAG2] != ELFMAG2 ||
+ hdr->e_ident[EI_MAG3] != ELFMAG3) {
+ // std::cout << "Invalid ELF magic bytes. Not an ELF file?" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+
+ if (hdr->e_ident[EI_CLASS] == ELFCLASS32) {
+ bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+ Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0];
+ if (rdHalf32(le, ehdr->e_type) != ET_EXEC ||
+ rdHalf32(le, ehdr->e_machine) != EM_ARM) {
+ // std::cout << "Invalid ELF type or machine for class (32-bit)" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+
+ for(int i = 0; i < rdHalf32(le, ehdr->e_phnum); ++i) {
+ loadProgHdr32(le, buffer, rdOff32(le, ehdr->e_phoff) + i * rdHalf32(le, ehdr->e_phentsize), total_file_size);
+ }
+
+ return;
+ } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) {
+ if (total_file_size < sizeof(Elf64_Ehdr)) {
+ // std::cout << "File too small, specifies 64-bit ELF but not big enough for 64-bit ELF header" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+ bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+ Elf64_Ehdr *ehdr = (Elf64_Ehdr*) &buffer[0];
+ if (rdHalf64(le, ehdr->e_type) != ET_EXEC ||
+ rdHalf64(le, ehdr->e_machine) != EM_AARCH64) {
+ // std::cout << "Invalid ELF type or machine for class (64-bit)" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+
+ for(int i = 0; i < rdHalf64(le, ehdr->e_phnum); ++i) {
+ loadProgHdr64(le, buffer, rdOff64(le, ehdr->e_phoff) + i * rdHalf64(le, ehdr->e_phentsize), total_file_size);
+ }
+
+ return;
+ } else {
+ // std::cout << "Unrecognized ELF file format" << std::endl;
+ exit(EXIT_FAILURE);
+ }
+}
+
+void load_elf(char *filename) {
+ // Read input file into memory
+ char* buffer = NULL;
+ int size = 0;
+ int chunk = (1<<24); // increments output buffer this much
+ int read = 0;
+ gzFile in = gzopen(filename, "rb");
+ if (in == NULL) { goto fail; }
+ while (!gzeof(in)) {
+ size = read + chunk;
+ buffer = (char*)realloc(buffer, size);
+ if (buffer == NULL) { goto fail; }
+
+ int s = gzread(in, buffer+read, size - read);
+ if (s < 0) { goto fail; }
+ read += s;
+ }
+
+ loadELFHdr(buffer, read);
+ free(buffer);
+ return;
+
+fail:
+ // std::cout << "Unable to read file " << filename << std::endl;
+ exit(EXIT_FAILURE);
+}
+
+////////////////////////////////////////////////////////////////
+// ELF Loader
+////////////////////////////////////////////////////////////////
+
diff --git a/lib/elf.h b/lib/elf.h
new file mode 100644
index 00000000..e5f90365
--- /dev/null
+++ b/lib/elf.h
@@ -0,0 +1,5 @@
+#pragma once
+
+#include<string.h>
+
+void load_elf(char *filename);
diff --git a/lib/rts.c b/lib/rts.c
new file mode 100644
index 00000000..563d11e2
--- /dev/null
+++ b/lib/rts.c
@@ -0,0 +1,329 @@
+#include<string.h>
+
+#include"sail.h"
+#include"rts.h"
+#include"elf.h"
+
+void sail_match_failure(sail_string msg)
+{
+ fprintf(stderr, "Pattern match failure in %s\n", msg);
+ exit(EXIT_FAILURE);
+}
+
+unit sail_assert(bool b, sail_string msg)
+{
+ if (b) return UNIT;
+ fprintf(stderr, "Assertion failed: %s\n", msg);
+ exit(EXIT_FAILURE);
+}
+
+unit sail_exit(unit u)
+{
+ exit(EXIT_SUCCESS);
+ return UNIT;
+}
+
+unit sleep_request(const unit u)
+{
+ fprintf(stderr, "Sail model going to sleep\n");
+ return UNIT;
+}
+
+/* ***** Sail memory builtins ***** */
+
+/*
+ * We organise memory available to the sail model into a linked list
+ * of dynamically allocated MASK + 1 size blocks.
+ */
+struct block {
+ uint64_t block_id;
+ uint8_t *mem;
+ struct block *next;
+};
+
+struct block *sail_memory = NULL;
+
+/*
+ * Must be one less than a power of two.
+ */
+uint64_t MASK = 0xFFFFFFul;
+
+/*
+ * All sail vectors are at least 64-bits, but only the bottom 8 bits
+ * are used in the second argument.
+ */
+void write_mem(uint64_t address, uint64_t byte)
+{
+ //printf("ADDR: %lu, BYTE: %lu\n", address, byte);
+
+ uint64_t mask = address & ~MASK;
+ uint64_t offset = address & MASK;
+
+ struct block *current = sail_memory;
+
+ while (current != NULL) {
+ if (current->block_id == mask) {
+ current->mem[offset] = (uint8_t) byte;
+ return;
+ } else {
+ current = current->next;
+ }
+ }
+
+ /*
+ * If we couldn't find a block matching the mask, allocate a new
+ * one, write the byte, and put it at the front of the block list.
+ */
+ fprintf(stderr, "[Sail] Allocating new block 0x%" PRIx64 "\n", mask);
+ struct block *new_block = malloc(sizeof(struct block));
+ new_block->block_id = mask;
+ new_block->mem = calloc(MASK + 1, sizeof(uint8_t));
+ new_block->mem[offset] = (uint8_t) byte;
+ new_block->next = sail_memory;
+ sail_memory = new_block;
+}
+
+uint64_t read_mem(uint64_t address)
+{
+ uint64_t mask = address & ~MASK;
+ uint64_t offset = address & MASK;
+
+ struct block *current = sail_memory;
+
+ while (current != NULL) {
+ if (current->block_id == mask) {
+ return (uint64_t) current->mem[offset];
+ } else {
+ current = current->next;
+ }
+ }
+
+ return 0x00;
+}
+
+void kill_mem()
+{
+ while (sail_memory != NULL) {
+ struct block *next = sail_memory->next;
+
+ free(sail_memory->mem);
+ free(sail_memory);
+
+ sail_memory = next;
+ }
+}
+
+// ***** Memory builtins *****
+
+unit write_ram(const mpz_t addr_size, // Either 32 or 64
+ const mpz_t data_size_mpz, // Number of bytes
+ const sail_bits hex_ram, // Currently unused
+ const sail_bits addr_bv,
+ const sail_bits data)
+{
+ uint64_t addr = mpz_get_ui(*addr_bv.bits);
+ uint64_t data_size = mpz_get_ui(data_size_mpz);
+
+ mpz_t buf;
+ mpz_init_set(buf, *data.bits);
+
+ uint64_t byte;
+ for(uint64_t i = 0; i < data_size; ++i) {
+ // Take the 8 low bits of buf and write to addr.
+ byte = mpz_get_ui(buf) & 0xFF;
+ write_mem(addr + i, byte);
+
+ // Then shift buf 8 bits right.
+ mpz_fdiv_q_2exp(buf, buf, 8);
+ }
+
+ mpz_clear(buf);
+ return UNIT;
+}
+
+void read_ram(sail_bits *data,
+ const mpz_t addr_size,
+ const mpz_t data_size_mpz,
+ const sail_bits hex_ram,
+ const sail_bits addr_bv)
+{
+ uint64_t addr = mpz_get_ui(*addr_bv.bits);
+ uint64_t data_size = mpz_get_ui(data_size_mpz);
+
+ mpz_set_ui(*data->bits, 0);
+ data->len = data_size * 8;
+
+ mpz_t byte;
+ mpz_init(byte);
+ for(uint64_t i = data_size; i > 0; --i) {
+ mpz_set_ui(byte, read_mem(addr + (i - 1)));
+ mpz_mul_2exp(*data->bits, *data->bits, 8);
+ mpz_add(*data->bits, *data->bits, byte);
+ }
+
+ mpz_clear(byte);
+}
+
+unit load_raw(mach_bits addr, const sail_string file)
+{
+ FILE *fp = fopen(file, "r");
+
+ uint64_t byte;
+ while ((byte = (uint64_t)fgetc(fp)) != EOF) {
+ write_mem(addr, byte);
+ addr++;
+ }
+
+ return UNIT;
+}
+
+void load_image(char *file)
+{
+ FILE *fp = fopen(file, "r");
+
+ if (!fp) {
+ fprintf(stderr, "Image file %s could not be loaded\n", file);
+ exit(EXIT_FAILURE);
+ }
+
+ char *addr = NULL;
+ char *data = NULL;
+ size_t len = 0;
+
+ while (true) {
+ ssize_t addr_len = getline(&addr, &len, fp);
+ if (addr_len == -1) break;
+ ssize_t data_len = getline(&data, &len, fp);
+ if (data_len == -1) break;
+
+ if (!strcmp(addr, "elf_entry\n")) {
+ if (sscanf(data, "%" PRIu64 "\n", &g_elf_entry) != 1) {
+ fprintf(stderr, "Failed to parse elf_entry\n");
+ exit(EXIT_FAILURE);
+ };
+ printf("Elf entry point: %" PRIx64 "\n", g_elf_entry);
+ } else {
+ write_mem((uint64_t) atoll(addr), (uint64_t) atoll(data));
+ }
+ }
+
+ free(addr);
+ free(data);
+ fclose(fp);
+}
+
+// ***** Tracing support *****
+
+unit enable_tracing(const unit u)
+{
+ g_trace_depth = 0;
+ g_trace_enabled = true;
+ return UNIT;
+}
+
+unit disable_tracing(const unit u)
+{
+ g_trace_depth = 0;
+ g_trace_enabled = false;
+ return UNIT;
+}
+
+bool is_tracing(const unit u)
+{
+ return g_trace_enabled;
+}
+
+void trace_mach_bits(const mach_bits x) {
+ if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x);
+}
+
+void trace_unit(const unit u) {
+ if (g_trace_enabled) fputs("()", stderr);
+}
+
+void trace_sail_string(const sail_string str) {
+ if (g_trace_enabled) fputs(str, stderr);
+}
+
+void trace_sail_int(const sail_int op) {
+ if (g_trace_enabled) mpz_out_str(stderr, 10, op);
+}
+
+void trace_sail_bits(const sail_bits op) {
+ if (g_trace_enabled) fprint_bits("", op, "", stderr);
+}
+
+void trace_bool(const bool b) {
+ if (g_trace_enabled) {
+ if (b) {
+ fprintf(stderr, "true");
+ } else {
+ fprintf(stderr, "false");
+ }
+ }
+}
+
+void trace_unknown(void) {
+ if (g_trace_enabled) fputs("?", stderr);
+}
+
+void trace_argsep(void) {
+ if (g_trace_enabled) fputs(", ", stderr);
+}
+
+void trace_argend(void) {
+ if (g_trace_enabled) fputs(")\n", stderr);
+}
+
+void trace_retend(void) {
+ if (g_trace_enabled) fputs("\n", stderr);
+}
+
+void trace_start(char *name)
+{
+ if (g_trace_enabled) {
+ fprintf(stderr, "[TRACE] ");
+ for (int64_t i = 0; i < g_trace_depth; ++i) {
+ fprintf(stderr, "%s", "| ");
+ }
+ fprintf(stderr, "%s(", name);
+ g_trace_depth++;
+ }
+}
+
+void trace_end(void)
+{
+ if (g_trace_enabled) {
+ fprintf(stderr, "[TRACE] ");
+ for (int64_t i = 0; i < g_trace_depth; ++i) {
+ fprintf(stderr, "%s", "| ");
+ }
+ g_trace_depth--;
+ }
+}
+
+/* ***** ELF functions ***** */
+
+void elf_entry(mpz_t *rop, const unit u)
+{
+ mpz_set_ui(*rop, g_elf_entry);
+}
+
+void elf_tohost(mpz_t *rop, const unit u)
+{
+ mpz_set_ui(*rop, 0x0ul);
+}
+
+/* ***** Setup and cleanup functions for RTS ***** */
+
+void setup_rts(void)
+{
+ disable_tracing(UNIT);
+ setup_library();
+}
+
+void cleanup_rts(void)
+{
+ cleanup_library();
+ kill_mem();
+}
diff --git a/lib/rts.h b/lib/rts.h
new file mode 100644
index 00000000..7f26df4e
--- /dev/null
+++ b/lib/rts.h
@@ -0,0 +1,116 @@
+#pragma once
+
+#include<inttypes.h>
+#include<stdlib.h>
+#include<stdio.h>
+
+#include"sail.h"
+
+/*
+ * This function should be called whenever a pattern match failure
+ * occurs. Pattern match failures are always fatal.
+ */
+void sail_match_failure(sail_string msg);
+
+/*
+ * sail_assert implements the assert construct in Sail. If any
+ * assertion fails we immediately exit the model.
+ */
+unit sail_assert(bool b, sail_string msg);
+
+unit sail_exit(unit);
+
+/*
+ * ASL->Sail model has an EnterLowPowerState() function that calls a
+ * sleep request builtin. If it gets called we print a message and
+ * exit the model.
+ */
+unit sleep_request(const unit u);
+
+/* ***** Memory builtins ***** */
+
+void write_mem(uint64_t, uint64_t);
+uint64_t read_mem(uint64_t);
+
+// These memory builtins are intended to match the semantics for the
+// __ReadRAM and __WriteRAM functions in ASL.
+
+unit write_ram(const mpz_t addr_size, // Either 32 or 64
+ const mpz_t data_size_mpz, // Number of bytes
+ const sail_bits hex_ram, // Currently unused
+ const sail_bits addr_bv,
+ const sail_bits data);
+
+void read_ram(sail_bits *data,
+ const mpz_t addr_size,
+ const mpz_t data_size_mpz,
+ const sail_bits hex_ram,
+ const sail_bits addr_bv);
+
+unit load_raw(mach_bits addr, const sail_string file);
+
+void load_image(char *);
+
+/* ***** Tracing ***** */
+
+static int64_t g_trace_depth;
+static int64_t g_trace_max_depth;
+static bool g_trace_enabled;
+
+/*
+ * Bind these functions in Sail to enable and disable tracing (see
+ * lib/trace.sail):
+ *
+ * val "enable_tracing" : unit -> unit
+ * val "disable_tracing" : unit -> unit
+ * val "is_tracing" : unit -> bool
+ *
+ * Compile with sail -c -c_trace.
+ */
+unit enable_tracing(const unit);
+unit disable_tracing(const unit);
+
+bool is_tracing(const unit);
+
+/*
+ * Tracing is implemented by void trace_TYPE functions, each of which
+ * takes the Sail value to print as the first argument, and prints it
+ * directly to stderr with no linebreaks.
+ *
+ * For types that don't have printing function we have trace_unknown,
+ * which simply prints '?'. trace_argsep, trace_argend, and
+ * trace_retend are used for formatting function arguments. They won't
+ * overlap with user defined types because the type names used for
+ * TYPE are zencoded. trace_start(NAME) and trace_end() are called
+ * before printing the function arguments and return value
+ * respectively.
+*/
+void trace_sail_int(const sail_int);
+void trace_bool(const bool);
+void trace_unit(const unit);
+void trace_sail_string(const sail_string);
+void trace_mach_bits(const mach_bits);
+void trace_sail_bits(const sail_bits);
+
+void trace_unknown(void);
+void trace_argsep(void);
+void trace_argend(void);
+void trace_retend(void);
+void trace_start(char *);
+void trace_end(void);
+
+/*
+ * Functions to get info from ELF files.
+ */
+
+static uint64_t g_elf_entry;
+
+void elf_entry(sail_int *rop, const unit u);
+void elf_tohost(sail_int *rop, const unit u);
+
+/*
+ * setup_rts and cleanup_rts are responsible for calling setup_library
+ * and cleanup_library in sail.h.
+ */
+void setup_rts(void);
+void cleanup_rts(void);
diff --git a/lib/sail.c b/lib/sail.c
new file mode 100644
index 00000000..66321590
--- /dev/null
+++ b/lib/sail.c
@@ -0,0 +1,1003 @@
+#include<inttypes.h>
+#include<stdbool.h>
+#include<stdio.h>
+#include<stdlib.h>
+#include<string.h>
+
+#include"sail.h"
+
+/*
+ * Temporary mpzs for use in functions below. To avoid conflicts, only
+ * use in functions that do not call other functions in this file.
+ */
+static sail_int sail_lib_tmp1, sail_lib_tmp2;
+
+#define FLOAT_PRECISION 255
+
+void setup_library(void)
+{
+ mpz_init(sail_lib_tmp1);
+ mpz_init(sail_lib_tmp2);
+ mpf_set_default_prec(FLOAT_PRECISION);
+}
+
+void cleanup_library(void)
+{
+ mpz_clear(sail_lib_tmp1);
+ mpz_clear(sail_lib_tmp2);
+}
+
+bool eq_unit(const unit a, const unit b)
+{
+ return true;
+}
+
+unit UNDEFINED(unit)(const unit u)
+{
+ return UNIT;
+}
+
+unit skip(const unit u)
+{
+ return UNIT;
+}
+
+/* ***** Sail bit type ***** */
+
+bool eq_bit(const mach_bits a, const mach_bits b)
+{
+ return a == b;
+}
+
+/* ***** Sail booleans ***** */
+
+bool not(const bool b) {
+ return !b;
+}
+
+bool eq_bool(const bool a, const bool b) {
+ return a == b;
+}
+
+bool UNDEFINED(bool)(const unit u) {
+ return false;
+}
+
+/* ***** Sail strings ***** */
+
+void CREATE(sail_string)(sail_string *str)
+{
+ char *istr = (char *) malloc(1 * sizeof(char));
+ istr[0] = '\0';
+ *str = istr;
+}
+
+void RECREATE(sail_string)(sail_string *str)
+{
+ free(*str);
+ char *istr = (char *) malloc(1 * sizeof(char));
+ istr[0] = '\0';
+ *str = istr;
+}
+
+void COPY(sail_string)(sail_string *str1, const sail_string str2)
+{
+ size_t len = strlen(str2);
+ *str1 = realloc(*str1, len + 1);
+ *str1 = strcpy(*str1, str2);
+}
+
+void KILL(sail_string)(sail_string *str)
+{
+ free(*str);
+}
+
+void dec_str(sail_string *str, const mpz_t n)
+{
+ free(*str);
+ gmp_asprintf(str, "%Zd", n);
+}
+
+void hex_str(sail_string *str, const mpz_t n)
+{
+ free(*str);
+ gmp_asprintf(str, "0x%Zx", n);
+}
+
+bool eq_string(const sail_string str1, const sail_string str2)
+{
+ return strcmp(str1, str2) == 0;
+}
+
+void undefined_string(sail_string *str, const unit u) {}
+
+void concat_str(sail_string *stro, const sail_string str1, const sail_string str2)
+{
+ *stro = realloc(*stro, strlen(str1) + strlen(str2) + 1);
+ (*stro)[0] = '\0';
+ strcat(*stro, str1);
+ strcat(*stro, str2);
+}
+
+/* ***** Sail integers ***** */
+
+#ifndef USE_INT128
+
+inline
+void COPY(sail_int)(sail_int *rop, const sail_int op)
+{
+ mpz_set(*rop, op);
+}
+
+inline
+void CREATE(sail_int)(sail_int *rop)
+{
+ mpz_init(*rop);
+}
+
+inline
+void RECREATE(sail_int)(sail_int *rop)
+{
+ mpz_set_ui(*rop, 0);
+}
+
+inline
+void KILL(sail_int)(sail_int *rop)
+{
+ mpz_clear(*rop);
+}
+
+inline
+void CREATE_OF(sail_int, mach_int)(sail_int *rop, mach_int op)
+{
+ mpz_init_set_si(*rop, op);
+}
+
+inline
+void RECREATE_OF(sail_int, mach_int)(sail_int *rop, mach_int op)
+{
+ mpz_set_si(*rop, op);
+}
+
+inline
+void CREATE_OF(sail_int, sail_string)(sail_int *rop, sail_string str)
+{
+ mpz_init_set_str(*rop, str, 10);
+}
+
+inline
+void RECREATE_OF(sail_int, sail_string)(mpz_t *rop, sail_string str)
+{
+ mpz_set_str(*rop, str, 10);
+}
+
+inline
+mach_int CONVERT_OF(mach_int, sail_int)(const sail_int op)
+{
+ return mpz_get_si(op);
+}
+
+inline
+void CONVERT_OF(sail_int, mach_int)(sail_int *rop, const mach_int op)
+{
+ mpz_set_si(*rop, op);
+}
+
+inline
+bool eq_int(const sail_int op1, const sail_int op2)
+{
+ return !abs(mpz_cmp(op1, op2));
+}
+
+inline
+bool lt(const sail_int op1, const sail_int op2)
+{
+ return mpz_cmp(op1, op2) < 0;
+}
+
+inline
+bool gt(const mpz_t op1, const mpz_t op2)
+{
+ return mpz_cmp(op1, op2) > 0;
+}
+
+inline
+bool lteq(const mpz_t op1, const mpz_t op2)
+{
+ return mpz_cmp(op1, op2) <= 0;
+}
+
+inline
+bool gteq(const mpz_t op1, const mpz_t op2)
+{
+ return mpz_cmp(op1, op2) >= 0;
+}
+
+inline
+void shl_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_mul_2exp(*rop, op1, mpz_get_ui(op2));
+}
+
+inline
+void shr_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2));
+}
+
+inline
+void undefined_int(sail_int *rop, const int n)
+{
+ mpz_set_ui(*rop, (uint64_t) n);
+}
+
+inline
+void undefined_range(sail_int *rop, const sail_int l, const sail_int u)
+{
+ mpz_set(*rop, l);
+}
+
+inline
+void add_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_add(*rop, op1, op2);
+}
+
+inline
+void sub_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_sub(*rop, op1, op2);
+}
+
+inline
+void mult_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_mul(*rop, op1, op2);
+}
+
+inline
+void tdiv_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_tdiv_q(*rop, op1, op2);
+}
+
+inline
+void tmod_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_tdiv_r(*rop, op1, op2);
+}
+
+inline
+void fdiv_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_fdiv_q(*rop, op1, op2);
+}
+
+inline
+void fmod_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ mpz_fdiv_r(*rop, op1, op2);
+}
+
+void max_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ if (lt(op1, op2)) {
+ mpz_set(*rop, op2);
+ } else {
+ mpz_set(*rop, op1);
+ }
+}
+
+void min_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+ if (gt(op1, op2)) {
+ mpz_set(*rop, op2);
+ } else {
+ mpz_set(*rop, op1);
+ }
+}
+
+inline
+void neg_int(sail_int *rop, const sail_int op)
+{
+ mpz_neg(*rop, op);
+}
+
+inline
+void abs_int(sail_int *rop, const sail_int op)
+{
+ mpz_abs(*rop, op);
+}
+
+void pow2(sail_int *rop, const sail_int exp) {
+ /* Assume exponent is never more than 2^64... */
+ uint64_t exp_ui = mpz_get_ui(exp);
+ mpz_t base;
+ mpz_init_set_ui(base, 2ul);
+ mpz_pow_ui(*rop, base, exp_ui);
+ mpz_clear(base);
+}
+
+#endif
+
+/* ***** Sail bitvectors ***** */
+
+void CREATE(sail_bits)(sail_bits *rop)
+{
+ rop->bits = malloc(sizeof(mpz_t));
+ rop->len = 0;
+ mpz_init(*rop->bits);
+}
+
+void RECREATE(sail_bits)(sail_bits *rop)
+{
+ rop->len = 0;
+ mpz_set_ui(*rop->bits, 0);
+}
+
+void COPY(sail_bits)(sail_bits *rop, const sail_bits op)
+{
+ rop->len = op.len;
+ mpz_set(*rop->bits, *op.bits);
+}
+
+void KILL(sail_bits)(sail_bits *rop)
+{
+ mpz_clear(*rop->bits);
+ free(rop->bits);
+}
+
+void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
+{
+ rop->bits = malloc(sizeof(mpz_t));
+ rop->len = len;
+ mpz_init_set_ui(*rop->bits, op);
+}
+
+void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
+{
+ rop->len = len;
+ mpz_set_ui(*rop->bits, op);
+}
+
+mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits op)
+{
+ return mpz_get_ui(*op.bits);
+}
+
+void CONVERT_OF(sail_bits, mach_bits)(sail_bits *rop, const mach_bits op, const uint64_t len)
+{
+ rop->len = len;
+ // use safe_rshift to correctly handle the case when we have a 0-length vector.
+ mpz_set_ui(*rop->bits, op & safe_rshift(UINT64_MAX, 64 - len));
+}
+
+void UNDEFINED(sail_bits)(sail_bits *rop, const sail_int len, const mach_bits bit)
+{
+ zeros(rop, len);
+}
+
+mach_bits UNDEFINED(mach_bits)(const unit u) { return 0; }
+
+mach_bits safe_rshift(const mach_bits x, const mach_bits n)
+{
+ if (n >= 64) {
+ return 0ul;
+ } else {
+ return x >> n;
+ }
+}
+
+void normalize_sail_bits(sail_bits *rop) {
+ /* TODO optimisation: keep a set of masks of various sizes handy */
+ mpz_set_ui(sail_lib_tmp1, 1);
+ mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, rop->len);
+ mpz_sub_ui(sail_lib_tmp1, sail_lib_tmp1, 1);
+ mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1);
+}
+
+void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk)
+{
+ rop->len = rop->len + 64ul;
+ mpz_mul_2exp(*rop->bits, *op.bits, 64ul);
+ mpz_add_ui(*rop->bits, *rop->bits, chunk);
+}
+
+void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len;
+ mpz_add(*rop->bits, *op1.bits, *op2.bits);
+ normalize_sail_bits(rop);
+}
+
+void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len;
+ mpz_sub(*rop->bits, *op1.bits, *op2.bits);
+ normalize_sail_bits(rop);
+}
+
+void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+{
+ rop->len = op1.len;
+ mpz_add(*rop->bits, *op1.bits, op2);
+ normalize_sail_bits(rop);
+}
+
+void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+{
+ rop->len = op1.len;
+ mpz_sub(*rop->bits, *op1.bits, op2);
+ normalize_sail_bits(rop);
+}
+
+void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len;
+ mpz_and(*rop->bits, *op1.bits, *op2.bits);
+}
+
+void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len;
+ mpz_ior(*rop->bits, *op1.bits, *op2.bits);
+}
+
+void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len;
+ mpz_xor(*rop->bits, *op1.bits, *op2.bits);
+}
+
+void not_bits(sail_bits *rop, const sail_bits op)
+{
+ rop->len = op.len;
+ mpz_set(*rop->bits, *op.bits);
+ for (mp_bitcnt_t i = 0; i < op.len; i++) {
+ mpz_combit(*rop->bits, i);
+ }
+}
+
+void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ mpz_t op1_int, op2_int;
+ mpz_init(op1_int);
+ mpz_init(op2_int);
+ sail_signed(&op1_int, op1);
+ sail_signed(&op2_int, op2);
+ rop->len = op1.len * 2;
+ mpz_mul(*rop->bits, op1_int, op2_int);
+ normalize_sail_bits(rop);
+ mpz_clear(op1_int);
+ mpz_clear(op2_int);
+}
+
+void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len * 2;
+ mpz_mul(*rop->bits, *op1.bits, *op2.bits);
+ normalize_sail_bits(rop); /* necessary? */
+}
+
+
+void zeros(sail_bits *rop, const sail_int op)
+{
+ rop->len = mpz_get_ui(op);
+ mpz_set_ui(*rop->bits, 0);
+}
+
+void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len)
+{
+ rop->len = mpz_get_ui(len);
+ mpz_set(*rop->bits, *op.bits);
+}
+
+void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len)
+{
+ rop->len = mpz_get_ui(len);
+ if(mpz_tstbit(*op.bits, op.len - 1)) {
+ mpz_set(*rop->bits, *op.bits);
+ for(mp_bitcnt_t i = rop->len - 1; i >= op.len; i--) {
+ mpz_setbit(*rop->bits, i);
+ }
+ } else {
+ mpz_set(*rop->bits, *op.bits);
+ }
+}
+
+void length_sail_bits(sail_int *rop, const sail_bits op)
+{
+ mpz_set_ui(*rop, op.len);
+}
+
+bool eq_bits(const sail_bits op1, const sail_bits op2)
+{
+ for (mp_bitcnt_t i = 0; i < op1.len; i++) {
+ if (mpz_tstbit(*op1.bits, i) != mpz_tstbit(*op2.bits, i)) return false;
+ }
+ return true;
+}
+
+void vector_subrange_sail_bits(sail_bits *rop,
+ const sail_bits op,
+ const sail_int n_mpz,
+ const sail_int m_mpz)
+{
+ uint64_t n = mpz_get_ui(n_mpz);
+ uint64_t m = mpz_get_ui(m_mpz);
+
+ rop->len = n - (m - 1ul);
+ mpz_fdiv_q_2exp(*rop->bits, *op.bits, m);
+ normalize_sail_bits(rop);
+}
+
+void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len)
+{
+ rop->len = mpz_get_ui(len);
+ mpz_set(*rop->bits, *op.bits);
+ normalize_sail_bits(rop);
+}
+
+mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz)
+{
+ uint64_t n = mpz_get_ui(n_mpz);
+ return (mach_bits) mpz_tstbit(*op.bits, n);
+}
+
+void sail_unsigned(sail_int *rop, const sail_bits op)
+{
+ /* Normal form of bv_t is always positive so just return the bits. */
+ mpz_set(*rop, *op.bits);
+}
+
+void sail_signed(sail_int *rop, const sail_bits op)
+{
+ if (op.len == 0) {
+ mpz_set_ui(*rop, 0);
+ } else {
+ mp_bitcnt_t sign_bit = op.len - 1;
+ mpz_set(*rop, *op.bits);
+ if (mpz_tstbit(*op.bits, sign_bit) != 0) {
+ /* If sign bit is unset then we are done,
+ otherwise clear sign_bit and subtract 2**sign_bit */
+ mpz_set_ui(sail_lib_tmp1, 1);
+ mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, sign_bit); /* 2**sign_bit */
+ mpz_combit(*rop, sign_bit); /* clear sign_bit */
+ mpz_sub(*rop, *rop, sail_lib_tmp1);
+ }
+ }
+}
+
+void append(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len + op2.len;
+ mpz_mul_2exp(*rop->bits, *op1.bits, op2.len);
+ mpz_ior(*rop->bits, *rop->bits, *op2.bits);
+}
+
+void replicate_bits(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+{
+ uint64_t op2_ui = mpz_get_ui(op2);
+ rop->len = op1.len * op2_ui;
+ mpz_set(*rop->bits, *op1.bits);
+ for (int i = 1; i < op2_ui; i++) {
+ mpz_mul_2exp(*rop->bits, *rop->bits, op1.len);
+ mpz_ior(*rop->bits, *rop->bits, *op1.bits);
+ }
+}
+
+uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64_t times)
+{
+ uint64_t r = v;
+ for (int i = 1; i < times; ++i) {
+ r |= (r << shift);
+ }
+ return r;
+}
+
+// Takes a slice of the (two's complement) binary representation of
+// integer n, starting at bit start, and of length len. With the
+// argument in the following order:
+//
+// get_slice_int(len, n, start)
+//
+// For example:
+//
+// get_slice_int(8, 1680, 4) =
+//
+// 11 0
+// V V
+// get_slice_int(8, 0b0110_1001_0000, 4) = 0b0110_1001
+// <-------^
+// (8 bit) 4
+//
+void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz)
+{
+ uint64_t start = mpz_get_ui(start_mpz);
+ uint64_t len = mpz_get_ui(len_mpz);
+
+ mpz_set_ui(*rop->bits, 0ul);
+ rop->len = len;
+
+ for (uint64_t i = 0; i < len; i++) {
+ if (mpz_tstbit(n, i + start)) mpz_setbit(*rop->bits, i);
+ }
+}
+
+// Set slice uses the same indexing scheme as get_slice_int, but it
+// puts a bitvector slice into an integer rather than returning it.
+void set_slice_int(sail_int *rop,
+ const sail_int len_mpz,
+ const sail_int n,
+ const sail_int start_mpz,
+ const sail_bits slice)
+{
+ uint64_t start = mpz_get_ui(start_mpz);
+
+ mpz_set(*rop, n);
+
+ for (uint64_t i = 0; i < slice.len; i++) {
+ if (mpz_tstbit(*slice.bits, i)) {
+ mpz_setbit(*rop, i + start);
+ } else {
+ mpz_clrbit(*rop, i + start);
+ }
+ }
+}
+
+void vector_update_subrange_sail_bits(sail_bits *rop,
+ const sail_bits op,
+ const sail_int n_mpz,
+ const sail_int m_mpz,
+ const sail_bits slice)
+{
+ uint64_t n = mpz_get_ui(n_mpz);
+ uint64_t m = mpz_get_ui(m_mpz);
+
+ mpz_set(*rop->bits, *op.bits);
+
+ for (uint64_t i = 0; i < n - (m - 1ul); i++) {
+ if (mpz_tstbit(*slice.bits, i)) {
+ mpz_setbit(*rop->bits, i + m);
+ } else {
+ mpz_clrbit(*rop->bits, i + m);
+ }
+ }
+}
+
+void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz)
+{
+ uint64_t start = mpz_get_ui(start_mpz);
+ uint64_t len = mpz_get_ui(len_mpz);
+
+ mpz_set_ui(*rop->bits, 0ul);
+ rop->len = len;
+
+ for (uint64_t i = 0; i < len; i++) {
+ if (mpz_tstbit(*op.bits, i + start)) mpz_setbit(*rop->bits, i);
+ }
+}
+
+void set_slice(sail_bits *rop,
+ const sail_int len_mpz,
+ const sail_int slen_mpz,
+ const sail_bits op,
+ const sail_int start_mpz,
+ const sail_bits slice)
+{
+ uint64_t start = mpz_get_ui(start_mpz);
+
+ mpz_set(*rop->bits, *op.bits);
+ rop->len = op.len;
+
+ for (uint64_t i = 0; i < slice.len; i++) {
+ if (mpz_tstbit(*slice.bits, i)) {
+ mpz_setbit(*rop->bits, i + start);
+ } else {
+ mpz_clrbit(*rop->bits, i + start);
+ }
+ }
+}
+
+void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len;
+ mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
+ normalize_sail_bits(rop);
+}
+
+void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len;
+ mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
+}
+
+/* FIXME */
+void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+ rop->len = op1.len;
+ mp_bitcnt_t shift_amt = mpz_get_ui(*op2.bits);
+ mp_bitcnt_t sign_bit = op1.len - 1;
+ mpz_fdiv_q_2exp(*rop->bits, *op1.bits, shift_amt);
+ if(mpz_tstbit(*op1.bits, sign_bit) != 0) {
+ /* */
+ for(; shift_amt > 0; shift_amt--) {
+ mpz_setbit(*rop->bits, sign_bit - shift_amt + 1);
+ }
+ }
+}
+
+void reverse_endianness(sail_bits *rop, const sail_bits op)
+{
+ rop->len = op.len;
+ if (rop->len == 64ul) {
+ uint64_t x = mpz_get_ui(*op.bits);
+ x = (x & 0xFFFFFFFF00000000) >> 32 | (x & 0x00000000FFFFFFFF) << 32;
+ x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16;
+ x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8;
+ mpz_set_ui(*rop->bits, x);
+ } else if (rop->len == 32ul) {
+ uint64_t x = mpz_get_ui(*op.bits);
+ x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16;
+ x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8;
+ mpz_set_ui(*rop->bits, x);
+ } else if (rop->len == 16ul) {
+ uint64_t x = mpz_get_ui(*op.bits);
+ x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8;
+ mpz_set_ui(*rop->bits, x);
+ } else if (rop->len == 8ul) {
+ mpz_set(*rop->bits, *op.bits);
+ } else {
+ /* For other numbers of bytes we reverse the bytes.
+ * XXX could use mpz_import/export for this. */
+ mpz_set_ui(sail_lib_tmp1, 0xff); // byte mask
+ mpz_set_ui(*rop->bits, 0); // reset accumulator for result
+ for(mp_bitcnt_t byte = 0; byte < op.len; byte+=8) {
+ mpz_tdiv_q_2exp(sail_lib_tmp2, *op.bits, byte); // shift byte to bottom
+ mpz_and(sail_lib_tmp2, sail_lib_tmp2, sail_lib_tmp1); // and with mask
+ mpz_mul_2exp(*rop->bits, *rop->bits, 8); // shift result left 8
+ mpz_ior(*rop->bits, *rop->bits, sail_lib_tmp2); // or byte into result
+ }
+ }
+}
+
+/* ***** Sail Reals ***** */
+
+void CREATE(real)(real *rop)
+{
+ mpf_init(*rop);
+}
+
+void RECREATE(real)(real *rop)
+{
+ mpf_set_ui(*rop, 0);
+}
+
+void KILL(real)(real *rop)
+{
+ mpf_clear(*rop);
+}
+
+void COPY(real)(real *rop, const real op)
+{
+ mpf_set(*rop, op);
+}
+
+void UNDEFINED(real)(real *rop, unit u)
+{
+ mpf_set_ui(*rop, 0ul);
+}
+
+void neg_real(real *rop, const real op)
+{
+ mpf_neg(*rop, op);
+}
+
+void mult_real(real *rop, const real op1, const real op2) {
+ mpf_mul(*rop, op1, op2);
+}
+
+void sub_real(real *rop, const real op1, const real op2)
+{
+ mpf_sub(*rop, op1, op2);
+}
+
+void add_real(real *rop, const real op1, const real op2)
+{
+ mpf_add(*rop, op1, op2);
+}
+
+void div_real(real *rop, const real op1, const real op2)
+{
+ mpf_div(*rop, op1, op2);
+}
+
+void sqrt_real(real *rop, const real op)
+{
+ mpf_sqrt(*rop, op);
+}
+
+void abs_real(real *rop, const real op)
+{
+ mpf_abs(*rop, op);
+}
+
+void round_up(sail_int *rop, const real op)
+{
+ mpf_t x;
+ mpf_init(x);
+ mpf_ceil(x, op);
+ mpz_set_ui(*rop, mpf_get_ui(x));
+ mpf_clear(x);
+}
+
+void round_down(sail_int *rop, const real op)
+{
+ mpf_t x;
+ mpf_init(x);
+ mpf_floor(x, op);
+ mpz_set_ui(*rop, mpf_get_ui(x));
+ mpf_clear(x);
+}
+
+void to_real(real *rop, const sail_int op)
+{
+ mpf_set_z(*rop, op);
+}
+
+bool eq_real(const real op1, const real op2)
+{
+ return mpf_cmp(op1, op2) == 0;
+}
+
+bool lt_real(const real op1, const real op2)
+{
+ return mpf_cmp(op1, op2) < 0;
+}
+
+bool gt_real(const real op1, const real op2)
+{
+ return mpf_cmp(op1, op2) > 0;
+}
+
+bool lteq_real(const real op1, const real op2)
+{
+ return mpf_cmp(op1, op2) <= 0;
+}
+
+bool gteq_real(const real op1, const real op2)
+{
+ return mpf_cmp(op1, op2) >= 0;
+}
+
+void real_power(real *rop, const real base, const sail_int exp)
+{
+ uint64_t exp_ui = mpz_get_ui(exp);
+ mpf_pow_ui(*rop, base, exp_ui);
+}
+
+void CREATE_OF(real, sail_string)(real *rop, const sail_string op)
+{
+ mpf_init(*rop);
+ gmp_sscanf(op, "%Ff", *rop);
+}
+
+/* ***** Printing functions ***** */
+
+void string_of_int(sail_string *str, const sail_int i)
+{
+ gmp_asprintf(str, "%Zd", i);
+}
+
+void string_of_bits(sail_string *str, const sail_bits op)
+{
+ if ((op.len % 4) == 0) {
+ gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits);
+ } else {
+ gmp_asprintf(str, "0b%*0Zb", op.len, *op.bits);
+ }
+}
+
+void fprint_bits(const sail_string pre,
+ const sail_bits op,
+ const sail_string post,
+ FILE *stream)
+{
+ fputs(pre, stream);
+
+ if (op.len % 4 == 0) {
+ fputs("0x", stream);
+ mpz_t buf;
+ mpz_init_set(buf, *op.bits);
+
+ char *hex = malloc((op.len / 4) * sizeof(char));
+
+ for (int i = 0; i < op.len / 4; ++i) {
+ char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30);
+ hex[i] = (c < 0x3A) ? c : c + 0x7;
+ mpz_fdiv_q_2exp(buf, buf, 4);
+ }
+
+ for (int i = op.len / 4; i > 0; --i) {
+ fputc(hex[i - 1], stream);
+ }
+
+ free(hex);
+ mpz_clear(buf);
+ } else {
+ fputs("0b", stream);
+ for (int i = op.len; i > 0; --i) {
+ fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stream);
+ }
+ }
+
+ fputs(post, stream);
+}
+
+unit print_bits(const sail_string str, const sail_bits op)
+{
+ fprint_bits(str, op, "\n", stdout);
+ return UNIT;
+}
+
+unit prerr_bits(const sail_string str, const sail_bits op)
+{
+ fprint_bits(str, op, "\n", stderr);
+ return UNIT;
+}
+
+unit print(const sail_string str)
+{
+ printf("%s", str);
+ return UNIT;
+}
+
+unit print_endline(const sail_string str)
+{
+ printf("%s\n", str);
+ return UNIT;
+}
+
+unit prerr(const sail_string str)
+{
+ fprintf(stderr, "%s", str);
+ return UNIT;
+}
+
+unit prerr_endline(const sail_string str)
+{
+ fprintf(stderr, "%s\n", str);
+ return UNIT;
+}
+
+unit print_int(const sail_string str, const sail_int op)
+{
+ fputs(str, stdout);
+ mpz_out_str(stdout, 10, op);
+ putchar('\n');
+ return UNIT;
+}
+
+unit prerr_int(const sail_string str, const sail_int op)
+{
+ fputs(str, stderr);
+ mpz_out_str(stderr, 10, op);
+ fputs("\n", stderr);
+ return UNIT;
+}
+
+unit sail_putchar(const sail_int op)
+{
+ char c = (char) mpz_get_ui(op);
+ putchar(c);
+ return UNIT;
+}
+
+void get_time_ns(sail_int *rop, const unit u)
+{
+ struct timespec t;
+ clock_gettime(CLOCK_REALTIME, &t);
+ mpz_set_si(*rop, t.tv_sec);
+ mpz_mul_ui(*rop, *rop, 1000000000);
+ mpz_add_ui(*rop, *rop, t.tv_nsec);
+}
diff --git a/lib/sail.h b/lib/sail.h
index 99b57d8a..e3e21c92 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -1,1124 +1,332 @@
-#ifndef SAIL_LIB
-#define SAIL_LIB
+#pragma once
-#include<stdio.h>
#include<inttypes.h>
#include<stdlib.h>
+#include<stdio.h>
#include<stdbool.h>
-#include<string.h>
+
+#ifndef USE_INT128
#include<gmp.h>
+#endif
+
#include<time.h>
+/*
+ * Called by the RTS to initialise and clear any library state.
+ */
+void setup_library(void);
+void cleanup_library(void);
+
+/*
+ * The Sail compiler expects functions to follow a specific naming
+ * convention for allocation, deallocation, and (deep)-copying. These
+ * macros implement this naming convention.
+ */
+#define CREATE(type) create_ ## type
+#define RECREATE(type) recreate_ ## type
+#define CREATE_OF(type1, type2) create_ ## type1 ## _of_ ## type2
+#define RECREATE_OF(type1, type2) recreate_ ## type1 ## _of_ ## type2
+#define CONVERT_OF(type1, type2) convert_ ## type1 ## _of_ ## type2
+#define COPY(type) copy_ ## type
+#define KILL(type) kill_ ## type
+#define UNDEFINED(type) undefined_ ## type
+
+#define SAIL_BUILTIN_TYPE(type)\
+ void create_ ## type(type *);\
+ void recreate_ ## type(type *);\
+ void copy_ ## type(type *, const type);\
+ void kill_ ## type(type *);
+
+/* ***** Sail unit type ***** */
+
typedef int unit;
#define UNIT 0
-unit undefined_unit(const unit u) {
- return UNIT;
-}
+unit UNDEFINED(unit)(const unit);
+bool eq_unit(const unit, const unit);
+
+unit skip(const unit);
+
+/* ***** Sail booleans ***** */
+
+/*
+ * and_bool and or_bool are special-cased by the compiler to ensure
+ * short-circuiting evaluation.
+ */
+bool not(const bool);
+bool eq_bool(const bool, const bool);
+bool UNDEFINED(bool)(const unit);
+
+/* ***** Sail strings ***** */
+
+/*
+ * Sail strings are just C strings.
+ */
+typedef char *sail_string;
+
+SAIL_BUILTIN_TYPE(sail_string);
+
+void dec_str(sail_string *str, const mpz_t n);
+void hex_str(sail_string *str, const mpz_t n);
+
+void undefined_string(sail_string *str, const unit u);
+
+bool eq_string(const sail_string, const sail_string);
+
+void concat_str(sail_string *stro, const sail_string str1, const sail_string str2);
+
+/* ***** Sail integers ***** */
+
+typedef int64_t mach_int;
+
+/*
+ * Integers can be either stack-allocated as 128-bit integers if
+ * __int128 is available, or use GMP arbitrary precision
+ * integers. This affects the function signatures, so use a macro to
+ * paper over the differences.
+ */
+#ifndef USE_INT128
-bool eq_unit(const unit u1, const unit u2) {
- return true;
-}
+typedef mpz_t sail_int;
+
+#define SAIL_INT_FUNCTION(fname, rtype, ...) void fname(rtype*, __VA_ARGS__)
+
+SAIL_BUILTIN_TYPE(sail_int);
+
+void CREATE_OF(sail_int, mach_int)(sail_int *, const mach_int);
+void RECREATE_OF(sail_int, mach_int)(sail_int *, const mach_int);
+
+void CREATE_OF(sail_int, sail_string)(sail_int *, const sail_string);
+void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string);
+
+mach_int CONVERT_OF(mach_int, sail_int)(const sail_int);
+void CONVERT_OF(sail_int, mach_int)(sail_int *, const mach_int);
+
+#else
+
+typedef __int128 sail_int;
+#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__)
+
+#endif
+
+/*
+ * Comparison operators for integers
+ */
+bool eq_int(const sail_int, const sail_int);
+
+bool lt(const sail_int, const sail_int);
+bool gt(const sail_int, const sail_int);
+bool lteq(const sail_int, const sail_int);
+bool gteq(const sail_int, const sail_int);
+
+/*
+ * Left and right shift for integers
+ */
+SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int);
+
+/*
+ * undefined_int and undefined_range can't use the UNDEFINED(TYPE)
+ * macro, because they're slightly magical. They take extra parameters
+ * to ensure that no undefined int can violate any type-guaranteed
+ * constraints.
+ */
+SAIL_INT_FUNCTION(undefined_int, sail_int, const int);
+SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int);
+
+/*
+ * Arithmetic operations in integers. We include functions for both
+ * truncating towards zero, and rounding towards -infinity (floor) as
+ * fdiv/fmod and tdiv/tmod respectively.
+ */
+SAIL_INT_FUNCTION(add_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(sub_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(mult_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(tdiv_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(tmod_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(fdiv_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(fmod_int, sail_int, const sail_int, const sail_int);
+
+SAIL_INT_FUNCTION(max_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(min_int, sail_int, const sail_int, const sail_int);
+
+SAIL_INT_FUNCTION(neg_int, sail_int, const sail_int);
+SAIL_INT_FUNCTION(abs_int, sail_int, const sail_int);
+
+SAIL_INT_FUNCTION(pow2, sail_int, const sail_int);
+
+/* ***** Sail bitvectors ***** */
+
+typedef uint64_t mach_bits;
+
+bool eq_bit(const mach_bits a, const mach_bits b);
typedef struct {
mp_bitcnt_t len;
mpz_t *bits;
-} bv_t;
+} sail_bits;
-typedef char *sail_string;
+SAIL_BUILTIN_TYPE(sail_bits);
+
+void CREATE_OF(sail_bits, mach_bits)(sail_bits *,
+ const mach_bits op,
+ const mach_bits len,
+ const bool direction);
+
+void RECREATE_OF(sail_bits, mach_bits)(sail_bits *,
+ const mach_bits op,
+ const mach_bits len,
+ const bool direction);
+
+mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits);
+void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t);
+
+void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit);
+mach_bits UNDEFINED(mach_bits)(const unit);
+
+/*
+ * Wrapper around >> operator to avoid UB when shift amount is greater
+ * than or equal to 64.
+ */
+mach_bits safe_rshift(const mach_bits, const mach_bits);
+
+/*
+ * Used internally to construct large bitvector literals.
+ */
+void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk);
+
+void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+
+void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2);
+void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2);
-/* Temporary mpzs for use in functions below. To avoid conflicts, only
- * use in functions that do not call other functions in this file. */
-static mpz_t sail_lib_tmp1, sail_lib_tmp2;
-
-/* Wrapper around >> operator to avoid UB when shift amount is greater
- than or equal to 64. */
-uint64_t safe_rshift(const uint64_t x, const uint64_t n) {
- if (n >= 64) {
- return 0ul;
- } else {
- return x >> n;
- }
-}
-
-/* This function should be called whenever a pattern match failure
- occurs. Pattern match failures are always fatal. */
-void sail_match_failure(sail_string msg) {
- fprintf(stderr, "Pattern match failure in %s\n", msg);
- exit(EXIT_FAILURE);
-}
-
-/* sail_assert implements the assert construct in Sail. If any
- assertion fails we immediately exit the model. */
-unit sail_assert(bool b, sail_string msg) {
- if (b) return UNIT;
- fprintf(stderr, "Assertion failed: %s\n", msg);
- exit(EXIT_FAILURE);
-}
-
-/* If the sail model calls the exit() function we print a message and
- exit successfully. */
-unit sail_exit(const unit u) {
- fprintf(stderr, "Sail model exit\n");
- exit(EXIT_SUCCESS);
-}
-
-uint64_t g_elf_entry;
-
-void elf_entry(mpz_t *rop, const unit u) {
- mpz_set_ui(*rop, g_elf_entry);
-}
-
-void elf_tohost(mpz_t *rop, const unit u) {
- mpz_set_ui(*rop, 0x0ul);
-}
-
-/* ASL->Sail model has an EnterLowPowerState() function that calls a
- sleep request builtin. If it gets called we print a message and
- exit the model. */
-unit sleep_request(const unit u) {
- fprintf(stderr, "Sail model going to sleep\n");
- exit(EXIT_SUCCESS);
-}
-
-// Sail bits are mapped to uint64_t where bitzero = 0ul and bitone = 1ul
-bool eq_bit(const uint64_t a, const uint64_t b) {
- return a == b;
-}
-
-uint64_t undefined_bit(unit u) { return 0; }
-
-unit skip(const unit u) {
- return UNIT;
-}
-
-// ***** Sail booleans *****
-
-bool not(const bool b) {
- return !b;
-}
-
-bool and_bool(const bool a, const bool b) {
- return a && b;
-}
-
-bool or_bool(const bool a, const bool b) {
- return a || b;
-}
-
-bool eq_bool(const bool a, const bool b) {
- return a == b;
-}
-
-bool undefined_bool(const unit u) {
- return false;
-}
-
-// ***** Sail strings *****
-void init_sail_string(sail_string *str) {
- char *istr = (char *) malloc(1 * sizeof(char));
- istr[0] = '\0';
- *str = istr;
-}
-
-void reinit_sail_string(sail_string *str) {
- free(*str);
- char *istr = (char *) malloc(1 * sizeof(char));
- istr[0] = '\0';
- *str = istr;
-}
-
-void set_sail_string(sail_string *str1, const sail_string str2) {
- size_t len = strlen(str2);
- *str1 = realloc(*str1, len + 1);
- *str1 = strcpy(*str1, str2);
-}
-
-void dec_str(sail_string *str, const mpz_t n) {
- free(*str);
- gmp_asprintf(str, "%Zd", n);
-}
-
-void hex_str(sail_string *str, const mpz_t n) {
- free(*str);
- gmp_asprintf(str, "0x%Zx", n);
-}
-
-void clear_sail_string(sail_string *str) {
- free(*str);
-}
-
-bool eq_string(const sail_string str1, const sail_string str2) {
- return strcmp(str1, str2) == 0;
-}
-
-void concat_str(sail_string *stro, const sail_string str1, const sail_string str2) {
- *stro = realloc(*stro, strlen(str1) + strlen(str2) + 1);
- (*stro)[0] = '\0';
- strcat(*stro, str1);
- strcat(*stro, str2);
-}
-
-void undefined_string(sail_string *str, const unit u) {
-}
-
-unit print_endline(const sail_string str) {
- printf("%s\n", str);
- return UNIT;
-}
-
-unit print_string(const sail_string str1, const sail_string str2) {
- printf("%s%s\n", str1, str2);
- return UNIT;
-}
-
-unit prerr_endline(const sail_string str) {
- fprintf(stderr, "%s\n", str);
- return UNIT;
-}
-
-unit print_int(const sail_string str, const mpz_t op) {
- fputs(str, stdout);
- mpz_out_str(stdout, 10, op);
- putchar('\n');
- return UNIT;
-}
-
-unit print_int64(const sail_string str, const int64_t op) {
- printf("%s%" PRId64 "\n", str, op);
- return UNIT;
-}
-
-unit sail_putchar(const mpz_t op) {
- char c = (char) mpz_get_ui(op);
- putchar(c);
- return UNIT;
-}
-
-// ***** Arbitrary precision integers *****
-
-// We wrap around the GMP functions so they follow a consistent naming
-// scheme that is shared with the other builtin sail types.
-
-void set_mpz_t(mpz_t *rop, const mpz_t op) {
- mpz_set(*rop, op);
-}
-
-void init_mpz_t(mpz_t *op) {
- mpz_init(*op);
-}
-
-void reinit_mpz_t(mpz_t *op) {
- mpz_set_ui(*op, 0);
-}
-
-void clear_mpz_t(mpz_t *op) {
- mpz_clear(*op);
-}
-
-void init_mpz_t_of_int64_t(mpz_t *rop, int64_t op) {
- mpz_init_set_si(*rop, op);
-}
-
-void reinit_mpz_t_of_int64_t(mpz_t *rop, int64_t op) {
- mpz_set_si(*rop, op);
-}
-
-void init_mpz_t_of_sail_string(mpz_t *rop, sail_string str) {
- mpz_init_set_str(*rop, str, 10);
-}
-
-void reinit_mpz_t_of_sail_string(mpz_t *rop, sail_string str) {
- mpz_set_str(*rop, str, 10);
-}
-
-int64_t convert_int64_t_of_mpz_t(const mpz_t op) {
- return mpz_get_si(op);
-}
-
-void convert_mpz_t_of_int64_t(mpz_t *rop, const int64_t op) {
- mpz_set_si(*rop, op);
-}
-
-// ***** Sail builtins for integers *****
-
-bool eq_int(const mpz_t op1, const mpz_t op2) {
- return !abs(mpz_cmp(op1, op2));
-}
-
-bool lt(const mpz_t op1, const mpz_t op2) {
- return mpz_cmp(op1, op2) < 0;
-}
-
-bool gt(const mpz_t op1, const mpz_t op2) {
- return mpz_cmp(op1, op2) > 0;
-}
-
-bool lteq(const mpz_t op1, const mpz_t op2) {
- return mpz_cmp(op1, op2) <= 0;
-}
-
-bool gteq(const mpz_t op1, const mpz_t op2) {
- return mpz_cmp(op1, op2) >= 0;
-}
-
-void shl_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) {
- mpz_mul_2exp(*rop, op1, mpz_get_ui(op2));
-}
-
-void shr_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) {
- mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2));
-}
-
-void undefined_int(mpz_t *rop, const unit u) {
- mpz_set_ui(*rop, 0ul);
-}
-
-void undefined_range(mpz_t *rop, const mpz_t l, const mpz_t u) {
- mpz_set(*rop, l);
-}
-
-void add_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
- mpz_add(*rop, op1, op2);
-}
-
-void sub_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
- mpz_sub(*rop, op1, op2);
-}
-
-void mult_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
- mpz_mul(*rop, op1, op2);
-}
-
-void div_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
- mpz_tdiv_q(*rop, op1, op2);
-}
-
-void mod_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
- mpz_tdiv_r(*rop, op1, op2);
-}
-
-void max_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) {
- if (lt(op1, op2)) {
- mpz_set(*rop, op2);
- } else {
- mpz_set(*rop, op1);
- }
-}
-
-void min_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) {
- if (gt(op1, op2)) {
- mpz_set(*rop, op2);
- } else {
- mpz_set(*rop, op1);
- }
-}
-
-void neg_int(mpz_t *rop, const mpz_t op) {
- mpz_neg(*rop, op);
-}
-
-void abs_int(mpz_t *rop, const mpz_t op) {
- mpz_abs(*rop, op);
-}
-
-void pow2(mpz_t *rop, mpz_t exp) {
- uint64_t exp_ui = mpz_get_ui(exp);
- mpz_t base;
- mpz_init_set_ui(base, 2ul);
- mpz_pow_ui(*rop, base, exp_ui);
- mpz_clear(base);
-}
-
-void get_time_ns(mpz_t *rop, const unit u) {
- struct timespec t;
- clock_gettime(CLOCK_REALTIME, &t);
- mpz_set_si(*rop, t.tv_sec);
- mpz_mul_ui(*rop, *rop, 1000000000);
- mpz_add_ui(*rop, *rop, t.tv_nsec);
-}
-
-// ***** Sail bitvectors *****
-
-void string_of_int(sail_string *str, mpz_t i) {
- gmp_asprintf(str, "%Zd", i);
-}
-
-void string_of_bits(sail_string *str, const bv_t op) {
- if ((op.len % 4) == 0) {
- gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits);
- } else {
- gmp_asprintf(str, "0b%*0Zb", op.len, *op.bits);
- }
-}
-
-unit fprint_bits(const sail_string str, const bv_t op, FILE *stream)
-{
- fputs(str, stream);
-
- if (op.len % 4 == 0) {
- fputs("0x", stream);
- mpz_t buf;
- mpz_init_set(buf, *op.bits);
-
- char *hex = malloc((op.len / 4) * sizeof(char));
-
- for (int i = 0; i < op.len / 4; ++i) {
- char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30);
- hex[i] = (c < 0x3A) ? c : c + 0x7;
- mpz_fdiv_q_2exp(buf, buf, 4);
- }
-
- for (int i = op.len / 4; i > 0; --i) {
- fputc(hex[i - 1], stream);
- }
-
- free(hex);
- mpz_clear(buf);
- } else {
- fputs("0b", stream);
- for (int i = op.len; i > 0; --i) {
- fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stream);
- }
- }
-
- fputs("\n", stream);
- return UNIT;
-}
-
-unit print_bits(const sail_string str, const bv_t op)
-{
- return fprint_bits(str, op, stdout);
-}
-
-unit prerr_bits(const sail_string str, const bv_t op)
-{
- return fprint_bits(str, op, stderr);
-}
-
-void length_bv_t(mpz_t *rop, const bv_t op) {
- mpz_set_ui(*rop, op.len);
-}
-
-void init_bv_t(bv_t *rop) {
- rop->bits = malloc(sizeof(mpz_t));
- rop->len = 0;
- mpz_init(*rop->bits);
-}
-
-void reinit_bv_t(bv_t *rop) {
- rop->len = 0;
- mpz_set_ui(*rop->bits, 0);
-}
-
-void normalise_bv_t(bv_t *rop) {
- /* TODO optimisation: keep a set of masks of various sizes handy */
- mpz_set_ui(sail_lib_tmp1, 1);
- mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, rop->len);
- mpz_sub_ui(sail_lib_tmp1, sail_lib_tmp1, 1);
- mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1);
-}
-
-void init_bv_t_of_uint64_t(bv_t *rop, const uint64_t op, const uint64_t len, const bool direction) {
- rop->bits = malloc(sizeof(mpz_t));
- rop->len = len;
- mpz_init_set_ui(*rop->bits, op);
-}
-
-void reinit_bv_t_of_uint64_t(bv_t *rop, const uint64_t op, const uint64_t len, const bool direction) {
- rop->len = len;
- mpz_set_ui(*rop->bits, op);
-}
-
-void set_bv_t(bv_t *rop, const bv_t op) {
- rop->len = op.len;
- mpz_set(*rop->bits, *op.bits);
-}
-
-void append_64(bv_t *rop, const bv_t op, const uint64_t chunk) {
- rop->len = rop->len + 64ul;
- mpz_mul_2exp(*rop->bits, *op.bits, 64ul);
- mpz_add_ui(*rop->bits, *rop->bits, chunk);
-}
-
-void append(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len + op2.len;
- mpz_mul_2exp(*rop->bits, *op1.bits, op2.len);
- mpz_ior(*rop->bits, *rop->bits, *op2.bits);
-}
-
-void replicate_bits(bv_t *rop, const bv_t op1, const mpz_t op2) {
- uint64_t op2_ui = mpz_get_ui(op2);
- rop->len = op1.len * op2_ui;
- mpz_set(*rop->bits, *op1.bits);
- for (int i = 1; i < op2_ui; i++) {
- mpz_mul_2exp(*rop->bits, *rop->bits, op1.len);
- mpz_ior(*rop->bits, *rop->bits, *op1.bits);
- }
-}
-
-uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64_t times) {
- uint64_t r = v;
- for (int i = 1; i < times; ++i) {
- r |= (r << shift);
- }
- return r;
-}
-
-void slice(bv_t *rop, const bv_t op, const mpz_t start_mpz, const mpz_t len_mpz)
-{
- uint64_t start = mpz_get_ui(start_mpz);
- uint64_t len = mpz_get_ui(len_mpz);
-
- mpz_set_ui(*rop->bits, 0ul);
- rop->len = len;
-
- for (uint64_t i = 0; i < len; i++) {
- if (mpz_tstbit(*op.bits, i + start)) mpz_setbit(*rop->bits, i);
- }
-}
-
-uint64_t convert_uint64_t_of_bv_t(const bv_t op) {
- return mpz_get_ui(*op.bits);
-}
-
-void zeros(bv_t *rop, const mpz_t op) {
- rop->len = mpz_get_ui(op);
- mpz_set_ui(*rop->bits, 0ul);
-}
-
-void zero_extend(bv_t *rop, const bv_t op, const mpz_t len) {
- rop->len = mpz_get_ui(len);
- mpz_set(*rop->bits, *op.bits);
-}
-
-void sign_extend(bv_t *rop, const bv_t op, const mpz_t len) {
- rop->len = mpz_get_ui(len);
- if(mpz_tstbit(*op.bits, op.len - 1)) {
- mpz_set(*rop->bits, *op.bits);
- for(mp_bitcnt_t i = rop->len - 1; i >= op.len; i--) {
- mpz_setbit(*rop->bits, i);
- }
- } else {
- mpz_set(*rop->bits, *op.bits);
- }
-}
-
-void clear_bv_t(bv_t *rop) {
- mpz_clear(*rop->bits);
- free(rop->bits);
-}
-
-void undefined_bv_t(bv_t *rop, mpz_t len, int bit) {
- zeros(rop, len);
-}
-
-void mask(bv_t *rop) {
- if (mpz_sizeinbase(*rop->bits, 2) > rop->len) {
- mpz_t m;
- mpz_init(m);
- mpz_ui_pow_ui(m, 2ul, rop->len);
- mpz_sub_ui(m, m, 1ul);
- mpz_and(*rop->bits, *rop->bits, m);
- mpz_clear(m);
- }
-}
-
-void truncate(bv_t *rop, const bv_t op, const mpz_t len) {
- rop->len = mpz_get_ui(len);
- mpz_set(*rop->bits, *op.bits);
- mask(rop);
-}
-
-void and_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len;
- mpz_and(*rop->bits, *op1.bits, *op2.bits);
-}
-
-void or_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len;
- mpz_ior(*rop->bits, *op1.bits, *op2.bits);
-}
-
-void not_bits(bv_t *rop, const bv_t op) {
- rop->len = op.len;
- mpz_set(*rop->bits, *op.bits);
- for (mp_bitcnt_t i = 0; i < op.len; i++) {
- mpz_combit(*rop->bits, i);
- }
-}
-
-void xor_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len;
- mpz_xor(*rop->bits, *op1.bits, *op2.bits);
-}
-
-bool eq_bits(const bv_t op1, const bv_t op2)
-{
- for (mp_bitcnt_t i = 0; i < op1.len; i++) {
- if (mpz_tstbit(*op1.bits, i) != mpz_tstbit(*op2.bits, i)) return false;
- }
- return true;
-}
-
-void sail_uint(mpz_t *rop, const bv_t op) {
- /* Normal form of bv_t is always positive so just return the bits. */
- mpz_set(*rop, *op.bits);
-}
-
-void sint(mpz_t *rop, const bv_t op)
-{
- if (op.len == 0) {
- mpz_set_ui(*rop, 0);
- } else {
- mp_bitcnt_t sign_bit = op.len - 1;
- mpz_set(*rop, *op.bits);
- if (mpz_tstbit(*op.bits, sign_bit) != 0) {
- /* If sign bit is unset then we are done,
- otherwise clear sign_bit and subtract 2**sign_bit */
- mpz_set_ui(sail_lib_tmp1, 1);
- mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, sign_bit); /* 2**sign_bit */
- mpz_combit(*rop, sign_bit); /* clear sign_bit */
- mpz_sub(*rop, *rop, sail_lib_tmp1);
- }
- }
-}
-
-void add_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len;
- mpz_add(*rop->bits, *op1.bits, *op2.bits);
- normalise_bv_t(rop);
-}
-
-void sub_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len;
- mpz_sub(*rop->bits, *op1.bits, *op2.bits);
- normalise_bv_t(rop);
-}
-
-void add_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) {
- rop->len = op1.len;
- mpz_add(*rop->bits, *op1.bits, op2);
- normalise_bv_t(rop);
-}
-
-void sub_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) {
- rop->len = op1.len;
- mpz_sub(*rop->bits, *op1.bits, op2);
-}
-
-void mults_vec(bv_t *rop, const bv_t op1, const bv_t op2) {
- mpz_t op1_int, op2_int;
- mpz_init(op1_int);
- mpz_init(op2_int);
- sint(&op1_int, op1);
- sint(&op2_int, op2);
- rop->len = op1.len * 2;
- mpz_mul(*rop->bits, op1_int, op2_int);
- normalise_bv_t(rop);
- mpz_clear(op1_int);
- mpz_clear(op2_int);
-}
-
-void mult_vec(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len * 2;
- mpz_mul(*rop->bits, *op1.bits, *op2.bits);
- normalise_bv_t(rop); /* necessary? */
-}
-
-void shift_bits_left(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len;
- mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
- normalise_bv_t(rop);
-}
-
-void shift_bits_right(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len;
- mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
-}
-
-/* FIXME */
-void shift_bits_right_arith(bv_t *rop, const bv_t op1, const bv_t op2) {
- rop->len = op1.len;
- mp_bitcnt_t shift_amt = mpz_get_ui(*op2.bits);
- mp_bitcnt_t sign_bit = op1.len - 1;
- mpz_fdiv_q_2exp(*rop->bits, *op1.bits, shift_amt);
- if(mpz_tstbit(*op1.bits, sign_bit) != 0) {
- /* */
- for(; shift_amt > 0; shift_amt--) {
- mpz_setbit(*rop->bits, sign_bit - shift_amt + 1);
- }
- }
-}
-
-void reverse_endianness(bv_t *rop, const bv_t op) {
- rop->len = op.len;
- if (rop->len == 64ul) {
- uint64_t x = mpz_get_ui(*op.bits);
- x = (x & 0xFFFFFFFF00000000) >> 32 | (x & 0x00000000FFFFFFFF) << 32;
- x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16;
- x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8;
- mpz_set_ui(*rop->bits, x);
- } else if (rop->len == 32ul) {
- uint64_t x = mpz_get_ui(*op.bits);
- x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16;
- x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8;
- mpz_set_ui(*rop->bits, x);
- } else if (rop->len == 16ul) {
- uint64_t x = mpz_get_ui(*op.bits);
- x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8;
- mpz_set_ui(*rop->bits, x);
- } else if (rop->len == 8ul) {
- mpz_set(*rop->bits, *op.bits);
- } else {
- /* For other numbers of bytes we reverse the bytes.
- * XXX could use mpz_import/export for this. */
- mpz_set_ui(sail_lib_tmp1, 0xff); // byte mask
- mpz_set_ui(*rop->bits, 0); // reset accumulator for result
- for(mp_bitcnt_t byte = 0; byte < op.len; byte+=8) {
- mpz_tdiv_q_2exp(sail_lib_tmp2, *op.bits, byte); // shift byte to bottom
- mpz_and(sail_lib_tmp2, sail_lib_tmp2, sail_lib_tmp1); // and with mask
- mpz_mul_2exp(*rop->bits, *rop->bits, 8); // shift result left 8
- mpz_ior(*rop->bits, *rop->bits, sail_lib_tmp2); // or byte into result
- }
- }
-}
-
-// Takes a slice of the (two's complement) binary representation of
-// integer n, starting at bit start, and of length len. With the
-// argument in the following order:
-//
-// get_slice_int(len, n, start)
-//
-// For example:
-//
-// get_slice_int(8, 1680, 4) =
-//
-// 11 0
-// V V
-// get_slice_int(8, 0b0110_1001_0000, 4) = 0b0110_1001
-// <-------^
-// (8 bit) 4
-//
-void get_slice_int(bv_t *rop, const mpz_t len_mpz, const mpz_t n, const mpz_t start_mpz)
-{
- uint64_t start = mpz_get_ui(start_mpz);
- uint64_t len = mpz_get_ui(len_mpz);
-
- mpz_set_ui(*rop->bits, 0ul);
- rop->len = len;
-
- for (uint64_t i = 0; i < len; i++) {
- if (mpz_tstbit(n, i + start)) mpz_setbit(*rop->bits, i);
- }
-}
-
-// Set slice uses the same indexing scheme as get_slice_int, but it
-// puts a bitvector slice into an integer rather than returning it.
-void set_slice_int(mpz_t *rop,
- const mpz_t len_mpz,
- const mpz_t n,
- const mpz_t start_mpz,
- const bv_t slice)
-{
- uint64_t start = mpz_get_ui(start_mpz);
-
- mpz_set(*rop, n);
-
- for (uint64_t i = 0; i < slice.len; i++) {
- if (mpz_tstbit(*slice.bits, i)) {
- mpz_setbit(*rop, i + start);
- } else {
- mpz_clrbit(*rop, i + start);
- }
- }
-}
-
-void vector_update_subrange_bv_t(bv_t *rop,
- const bv_t op,
- const mpz_t n_mpz,
- const mpz_t m_mpz,
- const bv_t slice)
-{
- uint64_t n = mpz_get_ui(n_mpz);
- uint64_t m = mpz_get_ui(m_mpz);
-
- mpz_set(*rop->bits, *op.bits);
-
- for (uint64_t i = 0; i < n - (m - 1ul); i++) {
- if (mpz_tstbit(*slice.bits, i)) {
- mpz_setbit(*rop->bits, i + m);
- } else {
- mpz_clrbit(*rop->bits, i + m);
- }
- }
-}
-
-void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n_mpz, const mpz_t m_mpz)
-{
- uint64_t n = mpz_get_ui(n_mpz);
- uint64_t m = mpz_get_ui(m_mpz);
-
- mpz_set_ui(*rop->bits, 0ul);
- rop->len = n - (m - 1ul);
-
- for (uint64_t i = 0; i < rop->len; i++) {
- if (mpz_tstbit(*op.bits, i + m)) {
- mpz_setbit(*rop->bits, i);
- } else {
- mpz_clrbit(*rop->bits, i);
- }
- }
-}
-
-int bitvector_access(const bv_t op, const mpz_t n_mpz) {
- uint64_t n = mpz_get_ui(n_mpz);
- return mpz_tstbit(*op.bits, n);
-}
-
-// Like slice but slices from a hexadecimal string.
-void hex_slice (bv_t *rop, const sail_string hex, const mpz_t len_mpz, const mpz_t start_mpz) {
- mpz_t op;
- mpz_init_set_str(op, hex, 0);
- get_slice_int(rop, len_mpz, op, start_mpz);
- mpz_clear(op);
-}
-
-void set_slice (bv_t *rop,
- const mpz_t len_mpz,
- const mpz_t slen_mpz,
- const bv_t op,
- const mpz_t start_mpz,
- const bv_t slice)
-{
- uint64_t start = mpz_get_ui(start_mpz);
-
- mpz_set(*rop->bits, *op.bits);
- rop->len = op.len;
-
- for (uint64_t i = 0; i < slice.len; i++) {
- if (mpz_tstbit(*slice.bits, i)) {
- mpz_setbit(*rop->bits, i + start);
- } else {
- mpz_clrbit(*rop->bits, i + start);
- }
- }
-}
-
-// ***** Real number implementation *****
-
-#define REAL_FLOAT
-
-#ifdef REAL_FLOAT
+void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void not_bits(sail_bits *rop, const sail_bits op);
+
+void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+
+void zeros(sail_bits *rop, const sail_int op);
+
+void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len);
+void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len);
+
+void length_sail_bits(sail_int *rop, const sail_bits op);
+
+bool eq_bits(const sail_bits op1, const sail_bits op2);
+
+void vector_subrange_sail_bits(sail_bits *rop,
+ const sail_bits op,
+ const sail_int n_mpz,
+ const sail_int m_mpz);
+
+void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len);
+
+mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz);
+
+void sail_unsigned(sail_int *rop, const sail_bits op);
+void sail_signed(sail_int *rop, const sail_bits op);
+
+void append(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+
+void replicate_bits(sail_bits *rop, const sail_bits op1, const sail_int op2);
+mach_bits fast_replicate_bits(const mach_bits shift, const mach_bits v, const mach_int times);
+
+void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz);
+
+void set_slice_int(sail_int *rop,
+ const sail_int len_mpz,
+ const sail_int n,
+ const sail_int start_mpz,
+ const sail_bits slice);
+
+void vector_update_subrange_sail_bits(sail_bits *rop,
+ const sail_bits op,
+ const sail_int n_mpz,
+ const sail_int m_mpz,
+ const sail_bits slice);
+
+void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz);
+
+void set_slice(sail_bits *rop,
+ const sail_int len_mpz,
+ const sail_int slen_mpz,
+ const sail_bits op,
+ const sail_int start_mpz,
+ const sail_bits slice);
+
+
+void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+
+void reverse_endianness(sail_bits*, sail_bits);
+
+/* ***** Sail reals ***** */
typedef mpf_t real;
-#define FLOAT_PRECISION 255
-
-void init_real(real *rop) {
- mpf_init(*rop);
-}
-
-void reinit_real(real *rop) {
- mpf_set_ui(*rop, 0);
-}
-
-void clear_real(real *rop) {
- mpf_clear(*rop);
-}
-
-void set_real(real *rop, const real op) {
- mpf_set(*rop, op);
-}
-
-void undefined_real(real *rop, unit u) {
- mpf_set_ui(*rop, 0ul);
-}
-
-void neg_real(real *rop, const real op) {
- mpf_neg(*rop, op);
-}
-
-void mult_real(real *rop, const real op1, const real op2) {
- mpf_mul(*rop, op1, op2);
-}
-
-void sub_real(real *rop, const real op1, const real op2) {
- mpf_sub(*rop, op1, op2);
-}
-
-void add_real(real *rop, const real op1, const real op2) {
- mpf_add(*rop, op1, op2);
-}
-
-void div_real(real *rop, const real op1, const real op2) {
- mpf_div(*rop, op1, op2);
-}
-
-void sqrt_real(real *rop, const real op) {
- mpf_sqrt(*rop, op);
-}
-
-void abs_real(real *rop, const real op) {
- mpf_abs(*rop, op);
-}
-
-void round_up(mpz_t *rop, const real op) {
- mpf_t x;
- mpf_init(x);
- mpf_ceil(x, op);
- mpz_set_ui(*rop, mpf_get_ui(x));
- mpf_clear(x);
-}
-
-void round_down(mpz_t *rop, const real op) {
- mpf_t x;
- mpf_init(x);
- mpf_floor(x, op);
- mpz_set_ui(*rop, mpf_get_ui(x));
- mpf_clear(x);
-}
-
-void to_real(real *rop, const mpz_t op) {
- mpf_set_z(*rop, op);
-}
-
-bool eq_real(const real op1, const real op2) {
- return mpf_cmp(op1, op2) == 0;
-}
-
-bool lt_real(const real op1, const real op2) {
- return mpf_cmp(op1, op2) < 0;
-}
-
-bool gt_real(const real op1, const real op2) {
- return mpf_cmp(op1, op2) > 0;
-}
-
-bool lteq_real(const real op1, const real op2) {
- return mpf_cmp(op1, op2) <= 0;
-}
-
-bool gteq_real(const real op1, const real op2) {
- return mpf_cmp(op1, op2) >= 0;
-}
-
-void real_power(real *rop, const real base, const mpz_t exp) {
- uint64_t exp_ui = mpz_get_ui(exp);
- mpf_pow_ui(*rop, base, exp_ui);
-}
-
-void init_real_of_sail_string(real *rop, const sail_string op) {
- // FIXME
- mpf_init(*rop);
-}
+SAIL_BUILTIN_TYPE(real);
-#endif
+void CREATE_OF(real, sail_string)(real *rop, const sail_string op);
-#endif
+void UNDEFINED(real)(real *rop, unit u);
+
+void neg_real(real *rop, const real op);
+
+void mult_real(real *rop, const real op1, const real op2);
+void sub_real(real *rop, const real op1, const real op2);
+void add_real(real *rop, const real op1, const real op2);
+void div_real(real *rop, const real op1, const real op2);
+
+void sqrt_real(real *rop, const real op);
+void abs_real(real *rop, const real op);
+
+void round_up(sail_int *rop, const real op);
+void round_down(sail_int *rop, const real op);
+
+void to_real(real *rop, const sail_int op);
+
+bool eq_real(const real op1, const real op2);
+
+bool lt_real(const real op1, const real op2);
+bool gt_real(const real op1, const real op2);
+bool lteq_real(const real op1, const real op2);
+bool gteq_real(const real op1, const real op2);
+
+void real_power(real *rop, const real base, const sail_int exp);
+
+/* ***** Printing ***** */
+
+void string_of_int(sail_string *str, const sail_int i);
+void string_of_bits(sail_string *str, const sail_bits op);
+
+/*
+ * Utility function not callable from Sail!
+ */
+void fprint_bits(const sail_string pre,
+ const sail_bits op,
+ const sail_string post,
+ FILE *stream);
+
+unit print_bits(const sail_string str, const sail_bits op);
+unit prerr_bits(const sail_string str, const sail_bits op);
+
+unit print(const sail_string str);
+unit print_endline(const sail_string str);
+
+unit prerr(const sail_string str);
+unit prerr_endline(const sail_string str);
+
+unit print_int(const sail_string str, const sail_int op);
+unit prerr_int(const sail_string str, const sail_int op);
+
+unit sail_putchar(const sail_int op);
+
+/* ***** Misc ***** */
-/* ***** Sail memory builtins ***** */
-
-/* We organise memory available to the sail model into a linked list
- of dynamically allocated MASK + 1 size blocks. The most recently
- written block is moved to the front of the list, so contiguous
- accesses should be as fast as possible. */
-
-struct block {
- uint64_t block_id;
- uint8_t *mem;
- struct block *next;
-};
-
-struct block *sail_memory = NULL;
-
-/* Must be one less than a power of two. */
-uint64_t MASK = 0xFFFFul;
-
-// All sail vectors are at least 64-bits, but only the bottom 8 bits
-// are used in the second argument.
-void write_mem(uint64_t address, uint64_t byte)
-{
- //printf("ADDR: %lu, BYTE: %lu\n", address, byte);
-
- uint64_t mask = address & ~MASK;
- uint64_t offset = address & MASK;
-
- struct block *current = sail_memory;
-
- while (current != NULL) {
- if (current->block_id == mask) {
- current->mem[offset] = (uint8_t) byte;
- return;
- } else {
- current = current->next;
- }
- }
-
- /* If we couldn't find a block matching the mask, allocate a new
- one, write the byte, and put it at the front of the block
- list. */
- struct block *new_block = malloc(sizeof(struct block));
- new_block->block_id = mask;
- new_block->mem = calloc(MASK + 1, sizeof(uint8_t));
- new_block->mem[offset] = byte;
- new_block->next = sail_memory;
- sail_memory = new_block;
-}
-
-uint64_t read_mem(uint64_t address)
-{
- uint64_t mask = address & ~MASK;
- uint64_t offset = address & MASK;
-
- struct block *current = sail_memory;
-
- while (current != NULL) {
- if (current->block_id == mask) {
- return (uint64_t) current->mem[offset];
- } else {
- current = current->next;
- }
- }
-
- return 0;
-}
-
-void kill_mem()
-{
- while (sail_memory != NULL) {
- struct block *next = sail_memory->next;
-
- free(sail_memory->mem);
- free(sail_memory);
-
- sail_memory = next;
- }
-}
-
-// ***** ARM Memory builtins *****
-
-// These memory builtins are intended to match the semantics for the
-// __ReadRAM and __WriteRAM functions in ASL.
-
-unit write_ram(const mpz_t addr_size, // Either 32 or 64
- const mpz_t data_size_mpz, // Number of bytes
- const bv_t hex_ram, // Currently unused
- const bv_t addr_bv,
- const bv_t data)
-{
- uint64_t addr = mpz_get_ui(*addr_bv.bits);
- uint64_t data_size = mpz_get_ui(data_size_mpz);
-
- mpz_t buf;
- mpz_init_set(buf, *data.bits);
-
- uint64_t byte;
- for(uint64_t i = 0; i < data_size; ++i) {
- // Take the 8 low bits of buf and write to addr.
- byte = mpz_get_ui(buf) & 0xFF;
- write_mem(addr + i, byte);
-
- // Then shift buf 8 bits right, and increment addr.
- mpz_fdiv_q_2exp(buf, buf, 8);
- }
-
- mpz_clear(buf);
- return UNIT;
-}
-
-void read_ram(bv_t *data,
- const mpz_t addr_size,
- const mpz_t data_size_mpz,
- const bv_t hex_ram,
- const bv_t addr_bv)
-{
- uint64_t addr = mpz_get_ui(*addr_bv.bits);
- uint64_t data_size = mpz_get_ui(data_size_mpz);
-
- mpz_set_ui(*data->bits, 0);
- data->len = data_size * 8;
-
- mpz_t byte;
- mpz_init(byte);
- for(uint64_t i = data_size; i > 0; --i) {
- mpz_set_ui(byte, read_mem(addr + (i - 1)));
- mpz_mul_2exp(*data->bits, *data->bits, 8);
- mpz_add(*data->bits, *data->bits, byte);
- }
-
- mpz_clear(byte);
-}
-
-unit load_raw(uint64_t addr, const sail_string file) {
- FILE *fp = fopen(file, "r");
-
- uint64_t byte;
- while ((byte = (uint64_t)fgetc(fp)) != EOF) {
- write_mem(addr, byte);
- addr++;
- }
-
- return UNIT;
-}
-
-void load_image(char *file) {
- FILE *fp = fopen(file, "r");
-
- if (!fp) {
- fprintf(stderr, "Image file %s could not be loaded\n", file);
- exit(EXIT_FAILURE);
- }
-
- char *addr = NULL;
- char *data = NULL;
- size_t len = 0;
-
- while (true) {
- ssize_t addr_len = getline(&addr, &len, fp);
- if (addr_len == -1) break;
- ssize_t data_len = getline(&data, &len, fp);
- if (data_len == -1) break;
-
- if (!strcmp(addr, "elf_entry\n")) {
- if (sscanf(data, "%" PRIu64 "\n", &g_elf_entry) != 1) {
- fprintf(stderr, "Failed to parse elf_entry\n");
- exit(EXIT_FAILURE);
- };
- printf("Elf entry point: %" PRIx64 "\n", g_elf_entry);
- } else {
- write_mem((uint64_t) atoll(addr), (uint64_t) atoll(data));
- }
- }
-
- free(addr);
- free(data);
- fclose(fp);
-}
-
-void load_instr(uint64_t addr, uint32_t instr) {
- write_mem(addr , instr & 0xFF);
- write_mem(addr + 1, instr >> 8 & 0xFF);
- write_mem(addr + 2, instr >> 16 & 0xFF);
- write_mem(addr + 3, instr >> 24 & 0xFF);
-}
-
-// ***** Setup and cleanup functions for library code *****
-
-void setup_library(void) {
- mpf_set_default_prec(FLOAT_PRECISION);
- mpz_init(sail_lib_tmp1);
- mpz_init(sail_lib_tmp2);
-}
-
-void cleanup_library(void) {
- mpz_clear(sail_lib_tmp1);
- mpz_clear(sail_lib_tmp2);
- kill_mem();
-}
+void get_time_ns(sail_int*, const unit);
diff --git a/lib/smt.sail b/lib/smt.sail
index ae672947..c9312819 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -7,7 +7,7 @@ val div = {
smt: "div",
ocaml: "quotient",
lem: "integerDiv",
- c: "div_int"
+ c: "tdiv_int"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
overload operator / = {div}
@@ -16,7 +16,7 @@ val mod = {
smt: "mod",
ocaml: "modulus",
lem: "integerMod",
- c: "mod_int"
+ c: "tmod_int"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
overload operator % = {mod}
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 075e8cb9..b709fe45 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -41,7 +41,7 @@ val truncate = {
ocaml: "vector_truncate",
lem: "vector_truncate",
coq: "vector_truncate",
- c: "truncate"
+ c: "sail_truncate"
} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
@@ -139,11 +139,14 @@ val unsigned = {
ocaml: "uint",
lem: "uint",
interpreter: "uint",
- c: "sail_uint",
+ c: "sail_unsigned",
coq: "uint"
} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
/* We need a non-empty vector so that the range makes sense */
-val signed = "sint" : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+val signed = {
+ c: "sail_signed",
+ _: "sint"
+} : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
$endif
diff --git a/mips/Makefile b/mips/Makefile
index 6abf1848..007d56c7 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -19,7 +19,7 @@ mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail
$(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@
mips_c: mips.c ../lib/sail.h Makefile
- gcc -O2 -g -I ../lib $< -l gmp -o $@
+ gcc -O2 -g -I ../lib $< ../lib/*.c -lgmp -lz -o $@
mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS)
$(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
diff --git a/mips/main.sail b/mips/main.sail
index 8b1e01d7..6f7d377e 100644
--- a/mips/main.sail
+++ b/mips/main.sail
@@ -16,7 +16,7 @@ function fetch_and_execute () = {
/* the following skips are required on mips to fake the tag effects otherwise type checker complains */
skip_rmemt();
skip_wmvt();
- prerr_bits("PC: ", PC);
+ /* prerr_bits("PC: ", PC); */
loop_again = true;
try {
let pc_pa = TranslatePC(PC);
@@ -62,9 +62,12 @@ function dump_mips_state () : unit -> unit = {
}
}
+val "load_raw" : (bits(64), string) -> unit
+
val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt}
function main () = {
+ load_raw(0x0000000000100000, "/home/aa2019/mips_freebsd/kernel");
init_registers(to_bits(64, elf_entry()));
startTime = get_time_ns();
while (fetch_and_execute()) do ();
diff --git a/mips/prelude.sail b/mips/prelude.sail
index f0ce2e5e..e2f1e0d4 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -103,10 +103,10 @@ val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
overload operator / = {quotient_nat, quotient}
-val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", _ : "div_int"} : (int, int) -> int
-val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", _ : "mod_int"} : (int, int) -> int
+val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", _ : "tdiv_int"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", _ : "tmod_int"} : (int, int) -> int
-val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "mod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1)
+val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1)
overload operator % = {modulus}
diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml
index 9b063404..0902877a 100644
--- a/riscv/platform_impl.ml
+++ b/riscv/platform_impl.ml
@@ -152,7 +152,7 @@ let rec term_read () =
let buf = Bytes.make 1 '\000' in
let nbytes = Unix.read Unix.stdin buf 0 1 in
(* todo: handle nbytes == 0 *)
- buf.[0]
+ Bytes.get buf 0
(*
let save_string_to_file s fname =
diff --git a/src/bitfield.ml b/src/bitfield.ml
index 391a653d..afdd5baf 100644
--- a/src/bitfield.ml
+++ b/src/bitfield.ml
@@ -64,62 +64,84 @@ let rec combine = function
Defs (defs @ defs')
let newtype name size order =
- let nt = Printf.sprintf "newtype %s = Mk_%s : %s" name name (bitvec size order) in
+ let chunks_64 =
+ Util.list_init (size / 64) (fun i -> Printf.sprintf "%s_chunk_%i : vector(64, %s, bit)" name i (string_of_order order))
+ in
+ let chunks =
+ if size mod 64 = 0 then chunks_64 else
+ let chunk_rem =
+ Printf.sprintf "%s_chunk_%i : vector(%i, %s, bit)" name (List.length chunks_64) (size mod 64) (string_of_order order)
+ in
+ chunk_rem :: List.rev chunks_64
+ in
+ let nt = Printf.sprintf "struct %s = {\n %s }" name (Util.string_of_list ",\n " (fun x -> x) chunks) in
ast_of_def_string order nt
-(* These functions define the getter and setter for all the bits in the field. *)
-let full_getter name size order =
- let fg_val = Printf.sprintf "val _get_%s : %s -> %s" name name (bitvec size order) in
- let fg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v" name name in
- combine [ast_of_def_string order fg_val; ast_of_def_string order fg_function]
+let rec translate_indices hi lo =
+ if hi / 64 = lo / 64 then
+ [(hi / 64, hi mod 64, lo mod 64)]
+ else
+ (hi / 64, hi mod 64, 0) :: translate_indices (hi - (hi mod 64 + 1)) lo
-let full_setter name size order =
- let fs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" name name (bitvec size order) in
- let fs_function = String.concat "\n"
- [ Printf.sprintf "function _set_%s (r_ref, v) = {" name;
- " r = _reg_deref(r_ref);";
- Printf.sprintf " r = Mk_%s(v);" name;
- " (*r_ref) = r";
+let constructor name order start stop =
+ let indices = translate_indices start stop in
+ let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
+ let constructor_val = Printf.sprintf "val Mk_%s : %s -> %s" name (bitvec size order) name in
+ let body (chunk, hi, lo) =
+ Printf.sprintf "%s_chunk_%i = v[%i .. %i]"
+ name chunk ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop)
+ in
+ let constructor_function = String.concat "\n"
+ [ Printf.sprintf "function Mk_%s v = struct {" name;
+ Printf.sprintf " %s" (Util.string_of_list ",\n " body indices);
"}"
]
in
- combine [ast_of_def_string order fs_val; ast_of_def_string order fs_function]
-
-let full_overload name order =
- ast_of_def_string order (Printf.sprintf "overload _mod_bits = {_get_%s, _set_%s}" name name)
-
-let full_accessor name size order =
- combine [full_getter name size order; full_setter name size order; full_overload name order]
+ combine [ast_of_def_string order constructor_val; ast_of_def_string order constructor_function]
(* For every index range, create a getter and setter *)
let index_range_getter name field order start stop =
+ let indices = translate_indices start stop in
let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
let irg_val = Printf.sprintf "val _get_%s_%s : %s -> %s" name field name (bitvec size order) in
- let irg_function = Printf.sprintf "function _get_%s_%s Mk_%s(v) = v[%i .. %i]" name field name start stop in
+ let body (chunk, start, stop) =
+ Printf.sprintf "v.%s_chunk_%i[%i .. %i]" name chunk start stop
+ in
+ let irg_function = Printf.sprintf "function _get_%s_%s v = %s" name field (Util.string_of_list " @ " body indices) in
combine [ast_of_def_string order irg_val; ast_of_def_string order irg_function]
let index_range_setter name field order start stop =
+ let indices = translate_indices start stop in
let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
let irs_val = Printf.sprintf "val _set_%s_%s : (register(%s), %s) -> unit effect {wreg}" name field name (bitvec size order) in
(* Read-modify-write using an internal _reg_deref function without rreg effect *)
+ let body (chunk, hi, lo) =
+ Printf.sprintf "r.%s_chunk_%i = [ r.%s_chunk_%i with %i .. %i = v[%i .. %i]]"
+ name chunk name chunk hi lo ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop)
+ in
let irs_function = String.concat "\n"
[ Printf.sprintf "function _set_%s_%s (r_ref, v) = {" name field;
- Printf.sprintf " r = _get_%s(_reg_deref(r_ref));" name;
- Printf.sprintf " r[%i .. %i] = v;" start stop;
- Printf.sprintf " (*r_ref) = Mk_%s(r)" name;
+ " r = _reg_deref(r_ref);";
+ Printf.sprintf " %s;" (Util.string_of_list ";\n " body indices);
+ " (*r_ref) = r";
"}"
]
in
combine [ast_of_def_string order irs_val; ast_of_def_string order irs_function]
let index_range_update name field order start stop =
+ let indices = translate_indices start stop in
let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
let iru_val = Printf.sprintf "val _update_%s_%s : (%s, %s) -> %s" name field name (bitvec size order) name in
(* Read-modify-write using an internal _reg_deref function without rreg effect *)
+ let body (chunk, hi, lo) =
+ Printf.sprintf "let v = { v with %s_chunk_%i = [ v.%s_chunk_%i with %i .. %i = x[%i .. %i]] }"
+ name chunk name chunk hi lo ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop)
+ in
let iru_function = String.concat "\n"
- [ Printf.sprintf "function _update_%s_%s (Mk_%s(v), x) = {" name field name;
- Printf.sprintf " Mk_%s([v with %i .. %i = x]);" name start stop;
- "}"
+ [ Printf.sprintf "function _update_%s_%s (v, x) =" name field;
+ Printf.sprintf " %s in" (Util.string_of_list " in\n " body indices);
+ " v"
]
in
let iru_overload = Printf.sprintf "overload update_%s = {_update_%s_%s}" field name field in
@@ -142,4 +164,5 @@ let field_accessor name order (id, ir) = index_range_accessor name (string_of_id
let macro id size order ranges =
let name = string_of_id id in
- combine ([newtype name size order; full_accessor name size order] @ List.map (field_accessor name order) ranges)
+ let ranges = (mk_id "bits", BF_aux (BF_range (Big_int.of_int (size - 1), Big_int.of_int 0), Parse_ast.Unknown)) :: ranges in
+ combine ([newtype name size order; constructor name order (size - 1) 0] @ List.map (field_accessor name order) ranges)
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 27d4d5a2..da7d3c31 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -67,9 +67,6 @@ let instr_number () =
let idecl ?loc:(l=Parse_ast.Unknown) ctyp id =
I_aux (I_decl (ctyp, id), (instr_number (), l))
-let ialloc ?loc:(l=Parse_ast.Unknown) ctyp id =
- I_aux (I_alloc (ctyp, id), (instr_number (), l))
-
let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval =
I_aux (I_init (ctyp, id, cval), (instr_number (), l))
@@ -161,11 +158,11 @@ and string_of_fragment' ?zencode:(zencode=true) f =
(* String representation of ctyps here is only for debugging and
intermediate language pretty-printer. *)
let rec string_of_ctyp = function
- | CT_mpz -> "mpz_t"
- | CT_bv true -> "bv_t(dec)"
- | CT_bv false -> "bv_t(inc)"
- | CT_uint64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)"
- | CT_uint64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)"
+ | CT_int -> "mpz_t"
+ | CT_bits true -> "bv_t(dec)"
+ | CT_bits false -> "bv_t(inc)"
+ | CT_bits64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)"
+ | CT_bits64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)"
| CT_int64 -> "int64_t"
| CT_bit -> "bit"
| CT_unit -> "unit"
@@ -221,8 +218,6 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
| I_try_block instrs ->
pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
- | I_alloc (ctyp, id) ->
- pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
| I_reset (ctyp, id) ->
pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
| I_init (ctyp, id, cval) ->
@@ -282,11 +277,10 @@ let pp_cdef = function
pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
^^ hardline
| CDEF_type tdef -> pp_ctype_def tdef ^^ hardline
- | CDEF_let (n, bindings, instrs, cleanup) ->
+ | CDEF_let (n, bindings, instrs) ->
let pp_binding (id, ctyp) = pp_id id ^^ string " : " ^^ pp_ctyp ctyp in
pp_keyword "let" ^^ string (string_of_int n) ^^ parens (separate_map (comma ^^ space) pp_binding bindings) ^^ space
^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ space
- ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr cleanup) rbrace ^^ space
^^ hardline
| CDEF_startup (id, instrs)->
pp_keyword "startup" ^^ pp_id id ^^ space
@@ -357,7 +351,7 @@ let rec clexp_deps = function
instruction **)
let instr_deps = function
| I_decl (ctyp, id) -> NS.empty, NS.singleton (G_id id)
- | I_alloc (ctyp, id) | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id)
+ | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id)
| I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NS.singleton (G_id id)
| I_if (cval, _, _, _) -> cval_deps cval, NS.empty
| I_jump (cval, label) -> cval_deps cval, NS.singleton (G_label label)
@@ -438,7 +432,6 @@ let make_dot id graph =
| G_id _ -> "yellow"
| G_instr (_, I_aux (I_decl _, _)) -> "olivedrab1"
| G_instr (_, I_aux (I_init _, _)) -> "springgreen"
- | G_instr (_, I_aux (I_alloc _, _)) -> "palegreen"
| G_instr (_, I_aux (I_clear _, _)) -> "peachpuff"
| G_instr (_, I_aux (I_goto _, _)) -> "orange1"
| G_instr (_, I_aux (I_label _, _)) -> "white"
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 7d586e9a..f58dd71f 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -59,6 +59,7 @@ module Big_int = Nat_big_num
let c_verbosity = ref 1
let opt_ddump_flow_graphs = ref false
+let opt_trace = ref false
(* Optimization flags *)
let optimize_primops = ref false
@@ -211,8 +212,8 @@ let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) =
| AE_val aval -> AE_val (aval_rename from_id to_id aval)
| AE_app (id, avals, typ) -> AE_app (id, List.map (aval_rename from_id to_id) avals, typ)
| AE_cast (aexp, typ) -> AE_cast (recur aexp, typ)
- | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp)
- | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp)
+ | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp_rename from_id to_id aexp)
+ | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp_rename from_id to_id aexp)
| AE_let (id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (id, typ1, aexp1, aexp2, typ2)
| AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, recur aexp1, recur aexp2, typ2)
| AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ)
@@ -464,12 +465,12 @@ let gensym () =
incr gensym_counter;
id
-let rec split_block = function
+let rec split_block l = function
| [exp] -> [], exp
| exp :: exps ->
- let exps, last = split_block exps in
+ let exps, last = split_block l exps in
exp :: exps, last
- | [] -> c_error "empty block"
+ | [] -> c_error ~loc:l "empty block"
let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) =
let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in
@@ -524,7 +525,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
| E_lit lit -> mk_aexp (ae_lit lit (typ_of exp))
| E_block exps ->
- let exps, last = split_block exps in
+ let exps, last = split_block l exps in
let aexps = List.map anf exps in
let alast = anf last in
mk_aexp (AE_block (aexps, alast, typ_of exp))
@@ -735,7 +736,8 @@ type ctx =
tc_env : Env.t;
local_env : Env.t;
letbinds : int list;
- recursive_functions : IdSet.t
+ recursive_functions : IdSet.t;
+ no_raw : bool;
}
let initial_ctx env =
@@ -745,14 +747,15 @@ let initial_ctx env =
tc_env = env;
local_env = env;
letbinds = [];
- recursive_functions = IdSet.empty
+ recursive_functions = IdSet.empty;
+ no_raw = false;
}
let rec ctyp_equal ctyp1 ctyp2 =
match ctyp1, ctyp2 with
- | CT_mpz, CT_mpz -> true
- | CT_bv d1, CT_bv d2 -> d1 = d2
- | CT_uint64 (m1, d1), CT_uint64 (m2, d2) -> m1 = m2 && d1 = d2
+ | CT_int, CT_int -> true
+ | CT_bits d1, CT_bits d2 -> d1 = d2
+ | CT_bits64 (m1, d1), CT_bits64 (m2, d2) -> m1 = m2 && d1 = d2
| CT_bit, CT_bit -> true
| CT_int64, CT_int64 -> true
| CT_unit, CT_unit -> true
@@ -775,8 +778,8 @@ let rec ctyp_of_typ ctx typ =
match typ_aux with
| Typ_id id when string_of_id id = "bit" -> CT_bit
| Typ_id id when string_of_id id = "bool" -> CT_bool
- | Typ_id id when string_of_id id = "int" -> CT_mpz
- | Typ_id id when string_of_id id = "nat" -> CT_mpz
+ | Typ_id id when string_of_id id = "int" -> CT_int
+ | Typ_id id when string_of_id id = "nat" -> CT_int
| Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" ->
begin
match destruct_range Env.empty typ with
@@ -791,8 +794,8 @@ let rec ctyp_of_typ ctx typ =
if prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) then
(prerr_endline "yes"; CT_int64)
else
- (prerr_endline "no"; CT_mpz)
- | _ -> CT_mpz
+ (prerr_endline "no"; CT_int)
+ | _ -> CT_int
end
| Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "list" ->
@@ -805,8 +808,8 @@ let rec ctyp_of_typ ctx typ =
begin
let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
match nexp_simp n with
- | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_uint64 (Big_int.to_int n, direction)
- | _ -> CT_bv direction
+ | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_bits64 (Big_int.to_int n, direction)
+ | _ -> CT_bits direction
end
| Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _);
Typ_arg_aux (Typ_arg_order ord, _);
@@ -845,8 +848,8 @@ let rec ctyp_of_typ ctx typ =
| _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
let rec is_stack_ctyp ctyp = match ctyp with
- | CT_uint64 _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
- | CT_bv _ | CT_mpz | CT_real | CT_string | CT_list _ | CT_vector _ -> false
+ | CT_bits64 _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
+ | CT_bits _ | CT_int | CT_real | CT_string | CT_list _ | CT_vector _ -> false
| CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields
| CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (*FIXME*)
| CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
@@ -960,6 +963,8 @@ let c_fragment = function
| AV_C_fragment (frag, _) -> frag
| _ -> assert false
+let v_mask_lower i = F_lit (V_bits (Util.list_init i (fun _ -> Sail2_values.B1)))
+
let analyze_primop' ctx env l id args typ =
let ctx = { ctx with local_env = env } in
let no_change = AE_app (id, args, typ) in
@@ -990,6 +995,13 @@ let analyze_primop' ctx env l id args typ =
| "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] ->
AE_val (AV_C_fragment (F_op (v1, "&", v2), typ))
+ | "not_bits", [AV_C_fragment (v, _)] ->
+ begin match destruct_vector ctx.tc_env typ with
+ | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+ when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+ AE_val (AV_C_fragment (F_op (F_unary ("~", v), "&", v_mask_lower (Big_int.to_int n)), typ))
+ end
+
| "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] ->
let len = F_op (f, "-", F_op (t, "-", v_one)) in
AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ))
@@ -1079,7 +1091,7 @@ let cval_ctyp = function (_, ctyp) -> ctyp
let rec map_instrs f (I_aux (instr, aux)) =
let instr = match instr with
- | I_decl _ | I_alloc _ | I_init _ | I_reset _ | I_reinit _ -> instr
+ | I_decl _ | I_init _ | I_reset _ | I_reinit _ -> instr
| I_if (cval, instrs1, instrs2, ctyp) ->
I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp)
| I_funcall _ | I_convert _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr
@@ -1093,7 +1105,7 @@ let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ct
let rec instr_ctyps (I_aux (instr, aux)) =
match instr with
- | I_decl (ctyp, _) | I_alloc (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) -> [ctyp]
+ | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) -> [ctyp]
| I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> [ctyp; cval_ctyp cval]
| I_if (cval, instrs1, instrs2, ctyp) ->
ctyp :: cval_ctyp cval :: List.concat (List.map instr_ctyps instrs1 @ List.map instr_ctyps instrs2)
@@ -1125,10 +1137,9 @@ let cdef_ctyps ctx = function
| CDEF_startup (id, instrs) | CDEF_finish (id, instrs) -> List.concat (List.map instr_ctyps instrs)
| CDEF_type tdef -> ctype_def_ctyps tdef
- | CDEF_let (_, bindings, instrs, cleanup) ->
+ | CDEF_let (_, bindings, instrs) ->
List.map snd bindings
@ List.concat (List.map instr_ctyps instrs)
- @ List.concat (List.map instr_ctyps cleanup)
let is_ct_enum = function
| CT_enum _ -> true
@@ -1178,17 +1189,15 @@ let rec compile_aval ctx = function
| AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
let gs = gensym () in
- [idecl CT_mpz gs;
- iinit CT_mpz gs (F_lit (V_int n), CT_int64)],
- (F_id gs, CT_mpz),
- [iclear CT_mpz gs]
+ [iinit CT_int gs (F_lit (V_int n), CT_int64)],
+ (F_id gs, CT_int),
+ [iclear CT_int gs]
| AV_lit (L_aux (L_num n, _), typ) ->
let gs = gensym () in
- [idecl CT_mpz gs;
- iinit CT_mpz gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
- (F_id gs, CT_mpz),
- [iclear CT_mpz gs]
+ [iinit CT_int gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
+ (F_id gs, CT_int),
+ [iclear CT_int gs]
| AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), []
| AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), []
@@ -1198,8 +1207,7 @@ let rec compile_aval ctx = function
| AV_lit (L_aux (L_real str, _), _) ->
let gs = gensym () in
- [idecl CT_real gs;
- iinit CT_real gs (F_lit (V_string str), CT_string)],
+ [iinit CT_real gs (F_lit (V_string str), CT_string)],
(F_id gs, CT_real),
[iclear CT_real gs]
@@ -1213,19 +1221,16 @@ let rec compile_aval ctx = function
let cleanup = List.concat (List.rev (List.map (fun (_, _, cleanup) -> cleanup) elements)) in
let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in
let gs = gensym () in
- let tup_setup, tup_cleanup =
- if is_stack_ctyp tup_ctyp then [], [] else [ialloc tup_ctyp gs], [iclear tup_ctyp gs]
- in
setup
- @ [idecl tup_ctyp gs] @ tup_setup
+ @ [idecl tup_ctyp gs]
@ List.mapi (fun n cval -> icopy (CL_field (gs, "tup" ^ string_of_int n)) cval) cvals,
(F_id gs, CT_tup (List.map cval_ctyp cvals)),
- tup_cleanup @ cleanup
+ [iclear tup_ctyp gs]
+ @ cleanup
| AV_record (fields, typ) ->
let ctyp = ctyp_of_typ ctx typ in
let gs = gensym () in
- let setup, cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in
let compile_fields (id, aval) =
let field_setup, cval, field_cleanup = compile_aval ctx aval in
field_setup
@@ -1233,10 +1238,9 @@ let rec compile_aval ctx = function
@ field_cleanup
in
[idecl ctyp gs]
- @ setup
@ List.concat (List.map compile_fields (Bindings.bindings fields)),
(F_id gs, ctyp),
- cleanup
+ [iclear ctyp gs]
| AV_vector ([], _) ->
c_error "Encountered empty vector literal"
@@ -1248,9 +1252,9 @@ let rec compile_aval ctx = function
let len = List.length avals in
match destruct_vector ctx.tc_env typ with
| Some (_, Ord_aux (Ord_inc, _), _) ->
- [], (bitstring, CT_uint64 (len, false)), []
+ [], (bitstring, CT_bits64 (len, false)), []
| Some (_, Ord_aux (Ord_dec, _), _) ->
- [], (bitstring, CT_uint64 (len, true)), []
+ [], (bitstring, CT_bits64 (len, true)), []
| Some _ ->
c_error "Encountered order polymorphic bitvector literal"
| None ->
@@ -1265,14 +1269,13 @@ let rec compile_aval ctx = function
let first_chunk = bitstring (Util.take (len mod 64) avals) in
let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in
let gs = gensym () in
- [idecl (CT_bv true) gs;
- iinit (CT_bv true) gs (first_chunk, CT_uint64 (len mod 64, true))]
+ [iinit (CT_bits true) gs (first_chunk, CT_bits64 (len mod 64, true))]
@ List.map (fun chunk -> ifuncall (CL_id gs)
(mk_id "append_64")
- [(F_id gs, CT_bv true); (chunk, CT_uint64 (64, true))]
- (CT_bv true)) chunks,
- (F_id gs, CT_bv true),
- [iclear (CT_bv true) gs]
+ [(F_id gs, CT_bits true); (chunk, CT_bits64 (64, true))]
+ (CT_bits true)) chunks,
+ (F_id gs, CT_bits true),
+ [iclear (CT_bits true) gs]
(* If we have a bitvector value, that isn't a literal then we need to set bits individually. *)
| AV_vector (avals, Typ_aux (Typ_app (id, [_; Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id bit_id, _)), _)]), _))
@@ -1284,7 +1287,7 @@ let rec compile_aval ctx = function
| Ord_aux (Ord_var _, _) -> c_error "Polymorphic vector direction found"
in
let gs = gensym () in
- let ctyp = CT_uint64 (len, direction) in
+ let ctyp = CT_bits64 (len, direction) in
let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in
let aval_mask i aval =
let setup, cval, cleanup = compile_aval ctx aval in
@@ -1321,7 +1324,6 @@ let rec compile_aval ctx = function
@ cleanup
in
[idecl vector_ctyp gs;
- ialloc vector_ctyp gs;
iextern (CL_id gs) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)] vector_ctyp]
@ List.concat (List.mapi aval_set avals),
(F_id gs, vector_ctyp),
@@ -1340,8 +1342,7 @@ let rec compile_aval ctx = function
let setup, cval, cleanup = compile_aval ctx aval in
setup @ [ifuncall (CL_id gs) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)] (CT_list ctyp)] @ cleanup
in
- [idecl (CT_list ctyp) gs;
- ialloc (CT_list ctyp) gs]
+ [idecl (CT_list ctyp) gs]
@ List.concat (List.map mk_cons (List.rev avals)),
(F_id gs, CT_list ctyp),
[iclear (CT_list ctyp) gs]
@@ -1373,10 +1374,21 @@ let compile_funcall l ctx id args typ =
cval
else if is_stack_ctyp have_ctyp && not (is_stack_ctyp ctyp) then
let gs = gensym () in
- setup := idecl ctyp gs :: !setup;
setup := iinit ctyp gs cval :: !setup;
cleanup := iclear ctyp gs :: !cleanup;
(F_id gs, ctyp)
+ else if not (is_stack_ctyp have_ctyp) && is_stack_ctyp ctyp then
+ (* This is inefficient. FIXME: Remove id restriction on iconvert
+ instruction. Fortunatly only happens when flow typing makes a
+ length-polymorphic bitvector monomorphic. *)
+ let gs1 = gensym () in
+ let gs2 = gensym () in
+ setup := idecl have_ctyp gs1 :: !setup;
+ setup := icopy (CL_id gs1) cval :: !setup;
+ setup := idecl ctyp gs2 :: !setup;
+ setup := iconvert (CL_id gs2) ctyp gs1 have_ctyp :: !setup;
+ cleanup := iclear have_ctyp gs1 :: !cleanup;
+ (F_id gs2, ctyp)
else
c_error ~loc:l
(Printf.sprintf "Failure when setting up function %s arguments: %s and %s." (string_of_id id) (string_of_ctyp have_ctyp) (string_of_ctyp ctyp))
@@ -1391,7 +1403,7 @@ let compile_funcall l ctx id args typ =
fun ret -> ifuncall ret id sargs ret_ctyp
else if not (is_stack_ctyp ret_ctyp) && is_stack_ctyp final_ctyp then
let gs = gensym () in
- setup := ialloc ret_ctyp gs :: idecl ret_ctyp gs :: !setup;
+ setup := idecl ret_ctyp gs :: !setup;
setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup;
cleanup := iclear ret_ctyp gs :: !cleanup;
fun ret -> iconvert ret final_ctyp gs ret_ctyp
@@ -1430,13 +1442,11 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
| AP_id (pid, typ), _ ->
let ctyp = cval_ctyp cval in
let id_ctyp = ctyp_of_typ ctx typ in
- let init, cleanup = if is_stack_ctyp id_ctyp then [], [] else [ialloc id_ctyp pid], [iclear id_ctyp pid] in
if ctyp_equal id_ctyp ctyp then
- [idecl ctyp pid] @ init @ [icopy (CL_id pid) cval], cleanup
+ [idecl ctyp pid; icopy (CL_id pid) cval], [iclear id_ctyp pid]
else
let gs = gensym () in
- let gs_init, gs_cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in
- [idecl id_ctyp pid; idecl ctyp gs] @ init @ gs_init @ [icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp] @ gs_cleanup, cleanup
+ [idecl id_ctyp pid; idecl ctyp gs; icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp; iclear ctyp gs], [iclear id_ctyp pid]
| AP_tup apats, (frag, ctyp) ->
begin
let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in
@@ -1489,10 +1499,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| AE_let (id, _, binding, body, typ) ->
let setup, ctyp, call, cleanup = compile_aexp ctx binding in
let letb_setup, letb_cleanup =
- if is_stack_ctyp ctyp then
- [idecl ctyp id; iblock (setup @ [call (CL_id id)] @ cleanup)], []
- else
- [idecl ctyp id; ialloc ctyp id; iblock (setup @ [call (CL_id id)] @ cleanup)], [iclear ctyp id]
+ [idecl ctyp id; iblock (setup @ [call (CL_id id)] @ cleanup)], [iclear ctyp id]
in
let setup, ctyp, call, cleanup = compile_aexp ctx body in
let body_ctyp = ctyp_of_typ ctx typ in
@@ -1502,7 +1509,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
begin
prerr_endline ("Mismatch: " ^ string_of_ctyp body_ctyp ^ " and " ^ string_of_ctyp ctyp);
let gs = gensym () in
- letb_setup @ setup @ [idecl ctyp gs; ialloc ctyp gs; call (CL_id gs)],
+ letb_setup @ setup @ [idecl ctyp gs; call (CL_id gs)],
body_ctyp,
(fun clexp -> iconvert clexp body_ctyp gs ctyp),
[iclear ctyp gs] @ cleanup @ letb_cleanup
@@ -1547,7 +1554,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
[iblock case_instrs; ilabel case_label]
in
[icomment "begin match"]
- @ aval_setup @ [idecl ctyp case_return_id] @ (if is_stack_ctyp ctyp then [] else [ialloc ctyp case_return_id])
+ @ aval_setup @ [idecl ctyp case_return_id]
@ List.concat (List.map compile_case cases)
@ [imatch_failure ()]
@ [ilabel finish_match_label],
@@ -1605,20 +1612,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
let setup, ctyp, call, cleanup = compile_aexp ctx aexp in
if ctyp_equal if_ctyp ctyp then
fun clexp -> setup @ [call clexp] @ cleanup
- else if is_stack_ctyp ctyp then
- fun clexp ->
- let gs = gensym() in
- setup
- @ [idecl ctyp gs;
- call (CL_id gs);
- iconvert clexp if_ctyp gs ctyp]
- @ cleanup
else
fun clexp ->
let gs = gensym () in
setup
@ [idecl ctyp gs;
- ialloc ctyp gs;
call (CL_id gs);
iconvert clexp if_ctyp gs ctyp;
iclear ctyp gs]
@@ -1637,7 +1635,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| AE_record_update (aval, fields, typ) ->
let ctyp = ctyp_of_typ ctx typ in
let gs = gensym () in
- let gs_setup, gs_cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in
let compile_fields (id, aval) =
let field_setup, cval, field_cleanup = compile_aval ctx aval in
field_setup
@@ -1646,14 +1643,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
in
let setup, cval, cleanup = compile_aval ctx aval in
[idecl ctyp gs]
- @ gs_setup
@ setup
@ [icopy (CL_id gs) cval]
@ cleanup
@ List.concat (List.map compile_fields (Bindings.bindings fields)),
ctyp,
(fun clexp -> icopy clexp (F_id gs, ctyp)),
- gs_cleanup
+ [iclear ctyp gs]
| AE_short_circuit (SC_and, aval, aexp) ->
let left_setup, cval, left_cleanup = compile_aval ctx aval in
@@ -1700,7 +1696,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
be different. *)
let pointer_assign ctyp1 ctyp2 =
match ctyp1 with
- | CT_ref ctyp1 -> ctyp_equal ctyp1 ctyp2
+ | CT_ref ctyp1 when ctyp_equal ctyp1 ctyp2 -> true
+ | CT_ref ctyp1 -> c_error ~loc:l "Incompatible type in pointer assignment"
| _ -> false
in
let assign_ctyp = ctyp_of_typ ctx assign_typ in
@@ -1710,18 +1707,17 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
setup @ [call (CL_id id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup
else if pointer_assign assign_ctyp ctyp then
setup @ [call (CL_addr id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup
- else if not (is_stack_ctyp assign_ctyp) && is_stack_ctyp ctyp then
+ else
let gs = gensym () in
setup @ [ icomment comment;
idecl ctyp gs;
call (CL_id gs);
- iconvert (CL_id id) assign_ctyp gs ctyp
+ iconvert (CL_id id) assign_ctyp gs ctyp;
+ iclear ctyp gs
],
CT_unit,
(fun clexp -> icopy clexp unit_fragment),
cleanup
- else
- failwith comment
| AE_block (aexps, aexp, _) ->
let block = compile_block ctx aexps in
@@ -1792,7 +1788,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
[idecl (cval_ctyp cval) gs1;
icopy (CL_id gs1) cval;
idecl fn_return_ctyp gs2;
- ialloc fn_return_ctyp gs2;
iconvert (CL_id gs2) fn_return_ctyp gs1 (cval_ctyp cval);
ireturn (F_id gs2, fn_return_ctyp)]
else
@@ -1849,7 +1844,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
else
let gs' = gensym () in
iblock (setup
- @ [idecl ctyp gs'; ialloc ctyp gs'; call (CL_id gs'); iconvert (CL_id gs) CT_int64 gs' ctyp; iclear ctyp gs']
+ @ [idecl ctyp gs'; call (CL_id gs'); iconvert (CL_id gs) CT_int64 gs' ctyp; iclear ctyp gs']
@ cleanup)]
in
@@ -1933,7 +1928,7 @@ let generate_cleanup instrs =
let generate_cleanup' (I_aux (instr, _)) =
match instr with
| I_init (ctyp, id, cval) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)]
- | I_alloc (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)]
+ | I_decl (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)]
| instr -> []
in
let is_clear ids = function
@@ -2073,7 +2068,7 @@ let fix_exception_block ctx instrs =
let rec map_try_block f (I_aux (instr, aux)) =
let instr = match instr with
- | I_decl _ | I_alloc _ | I_reset _ | I_init _ | I_reinit _ -> instr
+ | I_decl _ | I_reset _ | I_init _ | I_reinit _ -> instr
| I_if (cval, instrs1, instrs2, ctyp) ->
I_if (cval, List.map (map_try_block f) instrs1, List.map (map_try_block f) instrs2, ctyp)
| I_funcall _ | I_convert _ | I_copy _ | I_clear _ | I_throw _ | I_return _ -> instr
@@ -2139,7 +2134,7 @@ let rec compile_def ctx = function
| DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) ->
c_debug (lazy ("Compiling function " ^ string_of_id id));
let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in
- prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp));
+ if string_of_id id = "fetch_and_execute" then prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)) else ();
let setup, ctyp, call, cleanup = compile_aexp ctx aexp in
c_debug (lazy "Compiled aexp");
let fundef_label = label "fundef_fail_" in
@@ -2186,20 +2181,13 @@ let rec compile_def ctx = function
let end_label = label "let_end_" in
let destructure, destructure_cleanup = compile_match ctx apat (F_id gs, ctyp) end_label in
let gs_setup, gs_cleanup =
- if is_stack_ctyp ctyp then [idecl ctyp gs], [] else
- [idecl ctyp gs; ialloc ctyp gs], [iclear ctyp gs]
+ [idecl ctyp gs], [iclear ctyp gs]
in
let bindings = List.map (fun (id, typ) -> id, ctyp_of_typ ctx typ) (apat_globals apat) in
- let global_setup =
- List.concat (List.map (fun (id, ctyp) -> if is_stack_ctyp ctyp then [] else [ialloc ctyp id]) bindings)
- in
- let global_cleanup =
- List.concat (List.map (fun (id, ctyp) -> if is_stack_ctyp ctyp then [] else [iclear ctyp id]) bindings)
- in
let n = !letdef_count in
incr letdef_count;
let instrs =
- global_setup @ [icomment "gs_setup"] @ gs_setup @ [icomment "setup"] @ setup
+ [icomment "gs_setup"] @ gs_setup @ [icomment "setup"] @ setup
@ [icomment "call"]
@ [call (CL_id gs)]
@ [icomment "cleanup"]
@@ -2209,7 +2197,7 @@ let rec compile_def ctx = function
@ destructure_cleanup @ gs_cleanup
@ [ilabel end_label]
in
- [CDEF_let (n, bindings, instrs, global_cleanup)],
+ [CDEF_let (n, bindings, instrs)],
{ ctx with letbinds = n :: ctx.letbinds }
(* Only DEF_default that matters is default Order, but all order
@@ -2276,7 +2264,6 @@ let rec instrs_rename from_id to_id =
function
| (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs
| I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs
- | I_aux (I_alloc (ctyp, id), aux) :: instrs -> I_aux (I_alloc (ctyp, rename id), aux) :: irename instrs
| I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs
| I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs
| I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs
@@ -2297,7 +2284,7 @@ let rec instrs_rename from_id to_id =
| [] -> []
let hoist_ctyp = function
- | CT_mpz | CT_bv _ | CT_struct _ -> true
+ | CT_int | CT_bits _ | CT_struct _ -> true
| _ -> false
let hoist_counter = ref 0
@@ -2315,43 +2302,29 @@ let hoist_allocations ctx = function
let decls = ref [] in
let cleanups = ref [] in
let rec hoist = function
- | (I_aux (I_decl (ctyp, decl_id), _) as decl) :: instrs when hoist_ctyp ctyp ->
+ | I_aux (I_decl (ctyp, decl_id), annot) :: instrs when hoist_ctyp ctyp ->
let hid = hoist_id () in
- let hoist_stop (I_aux (instr, _)) =
- match instr with
- | I_if _ | I_block _ | I_try_block _ | I_alloc _ | I_init _ | I_clear _ -> true
- | _ -> false
- in
- let rec replace_inits instrs =
- match instr_split_at hoist_stop instrs with
- | before, I_aux (I_alloc (ctyp, id), aux) :: after when Id.compare id hid = 0 ->
- before @ I_aux (I_reset (ctyp, id), aux) :: replace_inits after
- | before, I_aux (I_init (ctyp, id, cval), aux) :: after when Id.compare id hid = 0 ->
- before @ I_aux (I_reinit (ctyp, id, cval), aux) :: replace_inits after
- | before, I_aux (I_clear (ctyp, id), aux) :: after when Id.compare id hid = 0 ->
- before @ replace_inits after
-
- | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: after ->
- before @ I_aux (I_if (cval, replace_inits then_instrs, replace_inits else_instrs, ctyp), aux) :: replace_inits after
- | before, I_aux (I_block instrs, aux) :: after ->
- before @ I_aux (I_block (replace_inits instrs), aux) :: replace_inits after
- | before, I_aux (I_try_block instrs, aux) :: after ->
- before @ I_aux (I_try_block (replace_inits instrs), aux) :: replace_inits after
-
- | before, instr :: after -> before @ instr :: replace_inits after
- | before, [] -> before
- in
- decls := ialloc ctyp hid :: idecl ctyp hid :: !decls;
+ decls := idecl ctyp hid :: !decls;
cleanups := iclear ctyp hid :: !cleanups;
- let instrs = replace_inits (instrs_rename decl_id hid instrs) in
+ let instrs = instrs_rename decl_id hid instrs in
+ I_aux (I_reset (ctyp, hid), annot) :: hoist instrs
+
+ | I_aux (I_init (ctyp, decl_id, cval), annot) :: instrs when hoist_ctyp ctyp ->
+ let hid = hoist_id () in
+ decls := idecl ctyp hid :: !decls;
+ cleanups := iclear ctyp hid :: !cleanups;
+ let instrs = instrs_rename decl_id hid instrs in
+ I_aux (I_reinit (ctyp, hid, cval), annot) :: hoist instrs
+
+ | I_aux (I_clear (ctyp, _), _) :: instrs when hoist_ctyp ctyp ->
hoist instrs
- | I_aux (I_block block, aux) :: instrs ->
- I_aux (I_block (hoist block), aux) :: hoist instrs
- | I_aux (I_try_block block, aux) :: instrs ->
- I_aux (I_try_block (hoist block), aux) :: hoist instrs
- | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
- I_aux (I_if (cval, hoist then_instrs, hoist else_instrs, ctyp), aux) :: hoist instrs
+ | I_aux (I_block block, annot) :: instrs ->
+ I_aux (I_block (hoist block), annot) :: hoist instrs
+ | I_aux (I_try_block block, annot) :: instrs ->
+ I_aux (I_try_block (hoist block), annot) :: hoist instrs
+ | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), annot) :: instrs ->
+ I_aux (I_if (cval, hoist then_instrs, hoist else_instrs, ctyp), annot) :: hoist instrs
| instr :: instrs -> instr :: hoist instrs
| [] -> []
@@ -2402,9 +2375,9 @@ let flatten_instrs ctx =
flat_counter := 0;
[CDEF_fundef (function_id, heap_return, args, flatten body)]
- | CDEF_let (n, bindings, instrs, cleanup) ->
+ | CDEF_let (n, bindings, instrs) ->
flat_counter := 0;
- [CDEF_let (n, bindings, flatten instrs, flatten cleanup)]
+ [CDEF_let (n, bindings, flatten instrs)]
| cdef -> [cdef]
@@ -2490,12 +2463,12 @@ let upper_codegen_id id = string (upper_sgen_id id)
let rec sgen_ctyp = function
| CT_unit -> "unit"
- | CT_bit -> "uint64_t"
+ | CT_bit -> "mach_bits"
| CT_bool -> "bool"
- | CT_uint64 _ -> "uint64_t"
- | CT_int64 -> "int64_t"
- | CT_mpz -> "mpz_t"
- | CT_bv _ -> "bv_t"
+ | CT_bits64 _ -> "mach_bits"
+ | CT_int64 -> "mach_int"
+ | CT_int -> "sail_int"
+ | CT_bits _ -> "sail_bits"
| CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
| CT_struct (id, _) -> "struct " ^ sgen_id id
| CT_enum (id, _) -> "enum " ^ sgen_id id
@@ -2508,12 +2481,12 @@ let rec sgen_ctyp = function
let rec sgen_ctyp_name = function
| CT_unit -> "unit"
- | CT_bit -> "uint64_t"
+ | CT_bit -> "mach_bits"
| CT_bool -> "bool"
- | CT_uint64 _ -> "uint64_t"
- | CT_int64 -> "int64_t"
- | CT_mpz -> "mpz_t"
- | CT_bv _ -> "bv_t"
+ | CT_bits64 _ -> "mach_bits"
+ | CT_int64 -> "mach_int"
+ | CT_int -> "sail_int"
+ | CT_bits _ -> "sail_bits"
| CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
| CT_struct (id, _) -> sgen_id id
| CT_enum (id, _) -> sgen_id id
@@ -2526,9 +2499,9 @@ let rec sgen_ctyp_name = function
let sgen_cval_param (frag, ctyp) =
match ctyp with
- | CT_bv direction ->
+ | CT_bits direction ->
string_of_fragment frag ^ ", " ^ string_of_bool direction
- | CT_uint64 (len, direction) ->
+ | CT_bits64 (len, direction) ->
string_of_fragment frag ^ ", " ^ string_of_int len ^ "ul , " ^ string_of_bool direction
| _ ->
string_of_fragment frag
@@ -2546,21 +2519,25 @@ let sgen_clexp = function
let sgen_clexp_pure = function
| CL_id id -> sgen_id id
| CL_field (id, field) -> sgen_id id ^ "." ^ Util.zencode_string field
- | CL_addr id -> sgen_id id
+ | CL_addr id -> "*" ^ sgen_id id
| CL_addr_field (id, field) -> sgen_id id ^ "->" ^ Util.zencode_string field
| CL_have_exception -> "have_exception"
| CL_current_exception -> "current_exception"
let rec codegen_instr fid ctx (I_aux (instr, _)) =
match instr with
- | I_decl (ctyp, id) ->
+ | I_decl (ctyp, id) when is_stack_ctyp ctyp ->
string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id))
+ | I_decl (ctyp, id) ->
+ string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) ^^ hardline
+ ^^ string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+
| I_copy (clexp, cval) ->
let ctyp = cval_ctyp cval in
if is_stack_ctyp ctyp then
string (Printf.sprintf " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval))
else
- string (Printf.sprintf " set_%s(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval))
+ string (Printf.sprintf " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval))
| I_jump (cval, label) ->
string (Printf.sprintf " if (%s) goto %s;" (sgen_cval cval) label)
| I_if (cval, [then_instr], [], ctyp) ->
@@ -2613,43 +2590,56 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
end
| "vector_update_subrange", _ -> Printf.sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp)
| "vector_subrange", _ -> Printf.sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp)
- | "vector_update", CT_uint64 _ -> "update_uint64_t"
- | "vector_update", CT_bv _ -> "update_bv"
+ | "vector_update", CT_bits64 _ -> "update_mach_bits"
+ | "vector_update", CT_bits _ -> "update_sail_bits"
| "vector_update", _ -> Printf.sprintf "vector_update_%s" (sgen_ctyp_name ctyp)
| "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp)
| "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp)
- | "undefined_vector", CT_uint64 _ -> "undefined_uint64_t"
- | "undefined_vector", CT_bv _ -> "undefined_bv_t"
- | "undefined_vector", _ -> Printf.sprintf "undefined_vector_%s" (sgen_ctyp_name ctyp)
+ | "undefined_vector", CT_bits64 _ -> "UNDEFINED(mach_bits)"
+ | "undefined_vector", CT_bits _ -> "UNDEFINED(sail_bits)"
+ | "undefined_bit", _ -> "UNDEFINED(mach_bits)"
+ | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
| fname, _ -> fname
in
if fname = "reg_deref" then
if is_stack_ctyp ctyp then
string (Printf.sprintf " %s = *(%s);" (sgen_clexp_pure x) c_args)
else
- string (Printf.sprintf " set_%s(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args)
+ string (Printf.sprintf " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args)
else if is_stack_ctyp ctyp then
string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args)
else
string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args)
+
+ | I_clear (ctyp, id) when is_stack_ctyp ctyp ->
+ empty
| I_clear (ctyp, id) ->
- string (Printf.sprintf " clear_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+ string (Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+
+ | I_init (ctyp, id, cval) when is_stack_ctyp ctyp ->
+ string (Printf.sprintf " %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval))
| I_init (ctyp, id, cval) ->
- string (Printf.sprintf " init_%s_of_%s(&%s, %s);"
- (sgen_ctyp_name ctyp)
- (sgen_ctyp_name (cval_ctyp cval))
- (sgen_id id)
- (sgen_cval_param cval))
- | I_alloc (ctyp, id) ->
- string (Printf.sprintf " init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+ string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) ^^ hardline
+ ^^ string (Printf.sprintf " CREATE_OF(%s, %s)(&%s, %s);"
+ (sgen_ctyp_name ctyp)
+ (sgen_ctyp_name (cval_ctyp cval))
+ (sgen_id id)
+ (sgen_cval_param cval))
+
+ | I_reinit (ctyp, id, cval) when is_stack_ctyp ctyp ->
+ string (Printf.sprintf " %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval))
| I_reinit (ctyp, id, cval) ->
- string (Printf.sprintf " reinit_%s_of_%s(&%s, %s);"
+ string (Printf.sprintf " RECREATE_OF(%s, %s)(&%s, %s);"
(sgen_ctyp_name ctyp)
(sgen_ctyp_name (cval_ctyp cval))
(sgen_id id)
(sgen_cval_param cval))
+
+ | I_reset (ctyp, id) when is_stack_ctyp ctyp ->
+ string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id))
| I_reset (ctyp, id) ->
- string (Printf.sprintf " reinit_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+ string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+
(* FIXME: This just covers the cases we see in our specs, need a
special conversion code-generator for full generality *)
| I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 ->
@@ -2659,7 +2649,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
else if ctyp_equal ctyp1 ctyp2 then
c_error "heap tuple type conversion"
else if is_stack_ctyp ctyp1 then
- string (Printf.sprintf " %s.ztup%i = convert_%s_of_%s(%s.ztup%i);"
+ string (Printf.sprintf " %s.ztup%i = CONVERT_OF(%s, %s)(%s.ztup%i);"
(sgen_clexp_pure x)
i
(sgen_ctyp_name ctyp1)
@@ -2667,7 +2657,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
(sgen_id y)
i)
else
- string (Printf.sprintf " convert_%s_of_%s(%s.ztup%i, %s.ztup%i);"
+ string (Printf.sprintf " CONVERT_OF(%s, %s)(%s.ztup%i, %s.ztup%i);"
(sgen_ctyp_name ctyp1)
(sgen_ctyp_name ctyp2)
(sgen_clexp x)
@@ -2676,15 +2666,32 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
i)
in
separate hardline (List.mapi convert (List.map2 (fun x y -> (x, y)) ctyps1 ctyps2))
+ (* If we're converting from a bits type with a known compile time
+ length, pass it as an extra parameter to the conversion. *)
+ | I_convert (x, ctyp1, y, (CT_bits64 (n, _) as ctyp2)) ->
+ if is_stack_ctyp ctyp1 then
+ string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s, %d);"
+ (sgen_clexp_pure x)
+ (sgen_ctyp_name ctyp1)
+ (sgen_ctyp_name ctyp2)
+ (sgen_id y)
+ n)
+ else
+ string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s, %d);"
+ (sgen_ctyp_name ctyp1)
+ (sgen_ctyp_name ctyp2)
+ (sgen_clexp x)
+ (sgen_id y)
+ n)
| I_convert (x, ctyp1, y, ctyp2) ->
if is_stack_ctyp ctyp1 then
- string (Printf.sprintf " %s = convert_%s_of_%s(%s);"
+ string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s);"
(sgen_clexp_pure x)
(sgen_ctyp_name ctyp1)
(sgen_ctyp_name ctyp2)
(sgen_id y))
else
- string (Printf.sprintf " convert_%s_of_%s(%s, %s);"
+ string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s);"
(sgen_ctyp_name ctyp1)
(sgen_ctyp_name ctyp2)
(sgen_clexp x)
@@ -2692,15 +2699,18 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
| I_return cval ->
string (Printf.sprintf " return %s;" (sgen_cval cval))
| I_throw cval ->
- string (Printf.sprintf " THROW(%s)" (sgen_cval cval))
+ c_error "I_throw reached code generator"
| I_comment str ->
string (" /* " ^ str ^ " */")
| I_label str ->
string (str ^ ": ;")
| I_goto str ->
string (Printf.sprintf " goto %s;" str)
+
+ | I_raw _ when ctx.no_raw -> empty
| I_raw str ->
string (" " ^ str)
+
| I_match_failure ->
string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");")
@@ -2721,10 +2731,10 @@ let codegen_type_def ctx = function
if is_stack_ctyp ctyp then
string (Printf.sprintf "rop->%s = op.%s;" (sgen_id id) (sgen_id id))
else
- string (Printf.sprintf "set_%s(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id))
+ string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id))
in
let codegen_setter id ctors =
- string (let n = sgen_id id in Printf.sprintf "void set_%s(struct %s *rop, const struct %s op)" n n n) ^^ space
+ string (let n = sgen_id id in Printf.sprintf "void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space
^^ surround 2 0 lbrace
(separate_map hardline codegen_set (Bindings.bindings ctors))
rbrace
@@ -2732,11 +2742,11 @@ let codegen_type_def ctx = function
(* Generate an init/clear_T function for every struct T *)
let codegen_field_init f (id, ctyp) =
if not (is_stack_ctyp ctyp) then
- [string (Printf.sprintf "%s_%s(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_id id))]
+ [string (Printf.sprintf "%s(%s)(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_id id))]
else []
in
let codegen_init f id ctors =
- string (let n = sgen_id id in Printf.sprintf "void %s_%s(struct %s *op)" f n n) ^^ space
+ string (let n = sgen_id id in Printf.sprintf "void %s(%s)(struct %s *op)" f n n) ^^ space
^^ surround 2 0 lbrace
(separate hardline (Bindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat))
rbrace
@@ -2756,11 +2766,11 @@ let codegen_type_def ctx = function
^^ semi ^^ twice hardline
^^ codegen_setter id (ctor_bindings ctors)
^^ twice hardline
- ^^ codegen_init "init" id (ctor_bindings ctors)
+ ^^ codegen_init "CREATE" id (ctor_bindings ctors)
^^ twice hardline
- ^^ codegen_init "reinit" id (ctor_bindings ctors)
+ ^^ codegen_init "RECREATE" id (ctor_bindings ctors)
^^ twice hardline
- ^^ codegen_init "clear" id (ctor_bindings ctors)
+ ^^ codegen_init "KILL" id (ctor_bindings ctors)
^^ twice hardline
^^ codegen_eq
@@ -2783,28 +2793,28 @@ let codegen_type_def ctx = function
let codegen_init =
let n = sgen_id id in
let ctor_id, ctyp = List.hd tus in
- string (Printf.sprintf "void init_%s(struct %s *op)" n n)
+ string (Printf.sprintf "void CREATE(%s)(struct %s *op)" n n)
^^ hardline
^^ surround 2 0 lbrace
(string (Printf.sprintf "op->kind = Kind_%s;" (sgen_id ctor_id)) ^^ hardline
^^ if not (is_stack_ctyp ctyp) then
- string (Printf.sprintf "init_%s(&op->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
+ string (Printf.sprintf "CREATE(%s)(&op->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
else empty)
rbrace
in
let codegen_reinit =
let n = sgen_id id in
- string (Printf.sprintf "void reinit_%s(struct %s *op) {}" n n)
+ string (Printf.sprintf "void RECREATE(%s)(struct %s *op) {}" n n)
in
let clear_field v ctor_id ctyp =
if is_stack_ctyp ctyp then
string (Printf.sprintf "/* do nothing */")
else
- string (Printf.sprintf "clear_%s(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_id ctor_id))
+ string (Printf.sprintf "KILL(%s)(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_id ctor_id))
in
let codegen_clear =
let n = sgen_id id in
- string (Printf.sprintf "void clear_%s(struct %s *op)" n n) ^^ hardline
+ string (Printf.sprintf "void KILL(%s)(struct %s *op)" n n) ^^ hardline
^^ surround 2 0 lbrace
(each_ctor "op->" (clear_field "op") tus ^^ semi)
rbrace
@@ -2821,7 +2831,7 @@ let codegen_type_def ctx = function
| CT_tup ctyps ->
String.concat ", " (List.mapi (fun i ctyp -> Printf.sprintf "%s op%d" (sgen_ctyp ctyp) i) ctyps),
string (Printf.sprintf "%s op;" (sgen_ctyp ctyp)) ^^ hardline
- ^^ string (Printf.sprintf "init_%s(&op);" (sgen_ctyp_name ctyp)) ^^ hardline
+ ^^ string (Printf.sprintf "CREATE(%s)(&op);" (sgen_ctyp_name ctyp)) ^^ hardline
^^ separate hardline (List.mapi tuple_set ctyps) ^^ hardline
| ctyp -> Printf.sprintf "%s op" (sgen_ctyp ctyp), empty
in
@@ -2833,8 +2843,8 @@ let codegen_type_def ctx = function
^^ if is_stack_ctyp ctyp then
string (Printf.sprintf "rop->%s = op;" (sgen_id ctor_id))
else
- string (Printf.sprintf "init_%s(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) ^^ hardline
- ^^ string (Printf.sprintf "set_%s(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)))
+ string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) ^^ hardline
+ ^^ string (Printf.sprintf "COPY(%s)(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)))
rbrace
in
let codegen_setter =
@@ -2843,10 +2853,10 @@ let codegen_type_def ctx = function
if is_stack_ctyp ctyp then
string (Printf.sprintf "rop->%s = op.%s;" (sgen_id ctor_id) (sgen_id ctor_id))
else
- string (Printf.sprintf "init_%s(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
- ^^ string (Printf.sprintf " set_%s(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id))
+ string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
+ ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id))
in
- string (Printf.sprintf "void set_%s(struct %s *rop, struct %s op)" n n n) ^^ hardline
+ string (Printf.sprintf "void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline
^^ surround 2 0 lbrace
(each_ctor "rop->" (clear_field "rop") tus
^^ semi ^^ hardline
@@ -2928,14 +2938,14 @@ let codegen_node id ctyp =
^^ string (Printf.sprintf "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id))
let codegen_list_init id =
- string (Printf.sprintf "void init_%s(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id))
+ string (Printf.sprintf "void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id))
let codegen_list_clear id ctyp =
- string (Printf.sprintf "void clear_%s(%s *rop) {\n" (sgen_id id) (sgen_id id))
+ string (Printf.sprintf "void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
^^ string (Printf.sprintf " if (*rop == NULL) return;")
^^ (if is_stack_ctyp ctyp then empty
- else string (Printf.sprintf " clear_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)))
- ^^ string (Printf.sprintf " clear_%s(&(*rop)->tl);\n" (sgen_id id))
+ else string (Printf.sprintf " KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)))
+ ^^ string (Printf.sprintf " KILL(%s)(&(*rop)->tl);\n" (sgen_id id))
^^ string " free(*rop);"
^^ string "}"
@@ -2946,13 +2956,13 @@ let codegen_list_set id ctyp =
^^ (if is_stack_ctyp ctyp then
string " (*rop)->hd = op->hd;\n"
else
- string (Printf.sprintf " init_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
- ^^ string (Printf.sprintf " set_%s(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp)))
+ string (Printf.sprintf " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
+ ^^ string (Printf.sprintf " COPY(%s)(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp)))
^^ string (Printf.sprintf " internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id))
^^ string "}"
^^ twice hardline
- ^^ string (Printf.sprintf "void set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
- ^^ string (Printf.sprintf " clear_%s(rop);\n" (sgen_id id))
+ ^^ string (Printf.sprintf "void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+ ^^ string (Printf.sprintf " KILL(%s)(rop);\n" (sgen_id id))
^^ string (Printf.sprintf " internal_set_%s(rop, op);\n" (sgen_id id))
^^ string "}"
@@ -2963,8 +2973,8 @@ let codegen_cons id ctyp =
^^ (if is_stack_ctyp ctyp then
string " (*rop)->hd = x;\n"
else
- string (Printf.sprintf " init_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
- ^^ string (Printf.sprintf " set_%s(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp)))
+ string (Printf.sprintf " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
+ ^^ string (Printf.sprintf " COPY(%s)(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp)))
^^ string " (*rop)->tl = xs;\n"
^^ string "}"
@@ -2972,7 +2982,7 @@ let codegen_pick id ctyp =
if is_stack_ctyp ctyp then
string (Printf.sprintf "%s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id))
else
- string (Printf.sprintf "void pick_%s(%s *x, const %s xs) { set_%s(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp))
+ string (Printf.sprintf "void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp))
let codegen_list ctx ctyp =
let id = mk_id (string_of_ctyp (CT_list ctyp)) in
@@ -3000,27 +3010,27 @@ let codegen_vector ctx (direction, ctyp) =
^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id))
in
let vector_init =
- string (Printf.sprintf "void init_%s(%s *rop) {\n rop->len = 0;\n rop->data = NULL;\n}" (sgen_id id) (sgen_id id))
+ string (Printf.sprintf "void CREATE(%s)(%s *rop) {\n rop->len = 0;\n rop->data = NULL;\n}" (sgen_id id) (sgen_id id))
in
let vector_set =
- string (Printf.sprintf "void set_%s(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
- ^^ string (Printf.sprintf " clear_%s(rop);\n" (sgen_id id))
+ string (Printf.sprintf "void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+ ^^ string (Printf.sprintf " KILL(%s)(rop);\n" (sgen_id id))
^^ string " rop->len = op.len;\n"
^^ string (Printf.sprintf " rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
^^ string " for (int i = 0; i < op.len; i++) {\n"
^^ string (if is_stack_ctyp ctyp then
" (rop->data)[i] = op.data[i];\n"
else
- Printf.sprintf " init_%s((rop->data) + i);\n set_%s((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
+ Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
^^ string " }\n"
^^ string "}"
in
let vector_clear =
- string (Printf.sprintf "void clear_%s(%s *rop) {\n" (sgen_id id) (sgen_id id))
+ string (Printf.sprintf "void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
^^ (if is_stack_ctyp ctyp then empty
else
string " for (int i = 0; i < (rop->len); i++) {\n"
- ^^ string (Printf.sprintf " clear_%s((rop->data) + i);\n" (sgen_ctyp_name ctyp))
+ ^^ string (Printf.sprintf " KILL(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp))
^^ string " }\n")
^^ string " if (rop->data != NULL) free(rop->data);\n"
^^ string "}"
@@ -3032,13 +3042,13 @@ let codegen_vector ctx (direction, ctyp) =
^^ string (if is_stack_ctyp ctyp then
" rop->data[m] = elem;\n"
else
- Printf.sprintf " set_%s((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
+ Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
^^ string " } else {\n"
- ^^ string (Printf.sprintf " set_%s(rop, op);\n" (sgen_id id))
+ ^^ string (Printf.sprintf " COPY(%s)(rop, op);\n" (sgen_id id))
^^ string (if is_stack_ctyp ctyp then
" rop->data[m] = elem;\n"
else
- Printf.sprintf " set_%s((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
+ Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
^^ string " }\n"
^^ string "}"
in
@@ -3047,7 +3057,7 @@ let codegen_vector ctx (direction, ctyp) =
^^ string (if is_stack_ctyp ctyp then
" rop->data[n] = elem;\n"
else
- Printf.sprintf " set_%s((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp))
+ Printf.sprintf " COPY(%s)((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp))
^^ string "}"
in
let vector_access =
@@ -3059,7 +3069,7 @@ let codegen_vector ctx (direction, ctyp) =
else
string (Printf.sprintf "void vector_access_%s(%s *rop, %s op, mpz_t n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
^^ string " int m = mpz_get_ui(n);\n"
- ^^ string (Printf.sprintf " set_%s(rop, op.data[m]);\n" (sgen_ctyp_name ctyp))
+ ^^ string (Printf.sprintf " COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp))
^^ string "}"
in
let internal_vector_init =
@@ -3076,7 +3086,7 @@ let codegen_vector ctx (direction, ctyp) =
^^ string (if is_stack_ctyp ctyp then
" (rop->data)[i] = elem;\n"
else
- Printf.sprintf " init_%s((rop->data) + i);\n set_%s((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
+ Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
^^ string " }\n"
^^ string "}"
in
@@ -3102,6 +3112,12 @@ let codegen_decl = function
string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))
| _ -> assert false
+let codegen_alloc = function
+ | I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty
+ | I_aux (I_decl (ctyp, id), _) ->
+ string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+ | _ -> assert false
+
let codegen_def' ctx = function
| CDEF_reg_dec (id, ctyp) ->
string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline
@@ -3145,22 +3161,20 @@ let codegen_def' ctx = function
^^ hardline
in
function_header
- (* ^^ string (Printf.sprintf "{ fprintf(stderr, \"%s \"); " (string_of_id id)) *)
^^ string "{"
^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline
^^ string "}"
- (* ^^ string "}" *)
| CDEF_type ctype_def ->
codegen_type_def ctx ctype_def
| CDEF_startup (id, instrs) ->
let startup_header = string (Printf.sprintf "void startup_%s(void)" (sgen_id id)) in
- separate_map hardline codegen_decl (List.filter is_decl instrs)
+ separate_map hardline codegen_decl instrs
^^ twice hardline
^^ startup_header ^^ hardline
^^ string "{"
- ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) (List.filter (fun i -> not (is_decl i)) instrs)) ^^ hardline
+ ^^ jump 0 2 (separate_map hardline codegen_alloc instrs) ^^ hardline
^^ string "}"
| CDEF_finish (id, instrs) ->
@@ -3169,15 +3183,22 @@ let codegen_def' ctx = function
^^ twice hardline
^^ finish_header ^^ hardline
^^ string "{"
- ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) (List.filter (fun i -> not (is_decl i)) instrs)) ^^ hardline
+ ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline
^^ string "}"
- | CDEF_let (number, bindings, instrs, cleanup) ->
+ | CDEF_let (number, bindings, instrs) ->
let instrs = add_local_labels instrs in
+ let setup =
+ List.concat (List.map (fun (id, ctyp) -> [idecl ctyp id]) bindings)
+ in
+ let cleanup =
+ List.concat (List.map (fun (id, ctyp) -> [iclear ctyp id]) bindings)
+ in
separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings
^^ hardline ^^ string (Printf.sprintf "void create_letbind_%d(void) " number)
^^ string "{"
- ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) instrs) ^^ hardline
+ ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline
+ ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") { ctx with no_raw = true }) instrs) ^^ hardline
^^ string "}"
^^ hardline ^^ string (Printf.sprintf "void kill_letbind_%d(void) " number)
^^ string "{"
@@ -3227,9 +3248,61 @@ let sgen_finish = function
Printf.sprintf " finish_%s();" (sgen_id id)
| _ -> assert false
+let instrument_tracing ctx =
+ let module StringSet = Set.Make(String) in
+ let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in
+ let rec instrument = function
+ | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs ->
+ let trace_start =
+ iraw (Printf.sprintf "trace_start(\"%s\");" (String.escaped (string_of_id id)))
+ in
+ let trace_arg cval =
+ let ctyp_name = sgen_ctyp_name (cval_ctyp cval) in
+ if StringSet.mem ctyp_name traceable then
+ iraw (Printf.sprintf "trace_%s(%s);" ctyp_name (sgen_cval cval))
+ else
+ iraw "trace_unknown();"
+ in
+ let rec trace_args = function
+ | [] -> []
+ | [cval] -> [trace_arg cval]
+ | cval :: cvals ->
+ trace_arg cval :: iraw "trace_argsep();" :: trace_args cvals
+ in
+ let trace_end = iraw "trace_end();" in
+ let trace_ret =
+ let ctyp_name = sgen_ctyp_name ctyp in
+ if StringSet.mem ctyp_name traceable then
+ iraw (Printf.sprintf "trace_%s(%s);" (sgen_ctyp_name ctyp) (sgen_clexp_pure clexp))
+ else
+ iraw "trace_unknown();"
+ in
+ [trace_start]
+ @ trace_args args
+ @ [iraw "trace_argend();";
+ instr;
+ trace_end;
+ trace_ret;
+ iraw "trace_retend();"]
+ @ instrument instrs
+
+ | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (instrument block), aux) :: instrument instrs
+ | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (instrument block), aux) :: instrument instrs
+ | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
+ I_aux (I_if (cval, instrument then_instrs, instrument else_instrs, ctyp), aux) :: instrument instrs
+
+ | instr :: instrs -> instr :: instrument instrs
+ | [] -> []
+ in
+ function
+ | CDEF_fundef (function_id, heap_return, args, body) ->
+ CDEF_fundef (function_id, heap_return, args, instrument body)
+ | cdef -> cdef
+
let bytecode_ast ctx rewrites (Defs defs) =
let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in
let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in
+
let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
let cdefs = List.concat (List.rev chunks) in
@@ -3254,18 +3327,23 @@ let compile_ast ctx (Defs defs) =
let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
let cdefs = List.concat (List.rev chunks) in
+
let cdefs = optimize ctx cdefs in
+ let cdefs = if !opt_trace then List.map (instrument_tracing ctx) cdefs else cdefs in
+
let docs = List.map (codegen_def ctx) cdefs in
let preamble = separate hardline
- [ string "#include \"sail.h\"" ]
+ [ string "#include \"sail.h\"";
+ string "#include \"rts.h\"";
+ string "#include \"elf.h\"" ]
in
let exn_boilerplate =
if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else
([ " current_exception = malloc(sizeof(struct zexception));";
- " init_zexception(current_exception);" ],
- [ " clear_zexception(current_exception);";
+ " CREATE(zexception)(current_exception);" ],
+ [ " KILL(zexception)(current_exception);";
" free(current_exception);";
" if (have_exception) fprintf(stderr, \"Exiting due to uncaught exception\\n\");" ])
in
@@ -3289,15 +3367,15 @@ let compile_ast ctx (Defs defs) =
if is_stack_ctyp ctyp then
[], []
else
- [ Printf.sprintf " init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ],
- [ Printf.sprintf " clear_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ]
+ [ Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ],
+ [ Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ]
in
let postamble = separate hardline (List.map string
( [ "int main(int argc, char *argv[])";
"{";
" if (argc > 1) { load_image(argv[1]); }";
- " setup_library();" ]
+ " setup_rts();" ]
@ fst exn_boilerplate
@ startup cdefs
@ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
@@ -3308,7 +3386,7 @@ let compile_ast ctx (Defs defs) =
@ List.concat (List.map (fun r -> snd (register_init_clear r)) regs)
@ finish cdefs
@ snd exn_boilerplate
- @ [ " cleanup_library();";
+ @ [ " cleanup_rts();";
" return EXIT_SUCCESS;";
"}" ] ))
in
diff --git a/src/sail.ml b/src/sail.ml
index 741cdf9c..a933ce59 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -119,6 +119,9 @@ let options = Arg.align ([
( "-Oconstant_fold",
Arg.Set Constant_fold.optimize_constant_fold,
" Apply constant folding optimizations");
+ ( "-trace",
+ Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml],
+ " Instrument ouput with tracing");
( "-lem_ast",
Arg.Set opt_print_lem_ast,
" output a Lem AST representation of the input");
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 6c880e8d..08a65b13 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -582,6 +582,10 @@ let real_of_string str =
(* Not a very good sqrt implementation *)
let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *)
+let print str = Pervasives.print_string str
+
+let prerr str = Pervasives.prerr_string str
+
let print_int (str, x) =
print_endline (str ^ Big_int.to_string x)
diff --git a/src/value.ml b/src/value.ml
index 8ee219b7..41b52720 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -491,6 +491,9 @@ let primops =
StringMap.empty
[ ("and_bool", and_bool);
("or_bool", or_bool);
+ ("print", value_print);
+ ("prerr", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
+ ("dec_str", fun _ -> V_string "X");
("print_endline", value_print);
("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
("putchar", value_putchar);
diff --git a/test/c/assign_rename_bug.expect b/test/c/assign_rename_bug.expect
new file mode 100644
index 00000000..ef2503c0
--- /dev/null
+++ b/test/c/assign_rename_bug.expect
@@ -0,0 +1,28 @@
+0xFFF0000000001
+0xFFF0000000001
+0xFFEFFFFFFFFFF
+0xFFEFFFFFFFFFF
+0xFFF0000000002
+0xFFF0000000002
+0xFFEFFFFFFFFFE
+0xFFEFFFFFFFFFE
+0xFFF0000000003
+0xFFF0000000003
+0xFFEFFFFFFFFFD
+0xFFEFFFFFFFFFD
+0xFFF0000000004
+0xFFF0000000004
+0xFFEFFFFFFFFFC
+0xFFEFFFFFFFFFC
+0xFFF0000000005
+0xFFF0000000005
+0xFFEFFFFFFFFFB
+0xFFEFFFFFFFFFB
+0xFFF0000000006
+0xFFF0000000006
+0xFFEFFFFFFFFFA
+0xFFEFFFFFFFFFA
+0xFFF0000000007
+0xFFF0000000007
+0xFFEFFFFFFFFF9
+0xFFEFFFFFFFFF9
diff --git a/test/c/assign_rename_bug.sail b/test/c/assign_rename_bug.sail
new file mode 100644
index 00000000..8b74df2a
--- /dev/null
+++ b/test/c/assign_rename_bug.sail
@@ -0,0 +1,35 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+
+$include <exception_basic.sail>
+
+val sub_vec_int = {
+ ocaml: "sub_vec_int",
+ lem: "sub_vec_int",
+ c: "sub_bits_int"
+} : forall 'n. (bits('n), int) -> bits('n)
+
+overload operator - = {sub_vec_int}
+
+val print_bits52: (string, bits(52)) -> unit
+
+function print_bits52(str, x) = print_bits(str, x)
+
+val main : unit -> unit effect {undef}
+
+function main() = {
+ let addr : bits(52) = 0xF_FF00_0000_0000;
+ i : int = undefined;
+ size : int = 7;
+ ret : unit = ();
+ foreach (i from 1 to size by 1 in inc) {
+ ret = print_bits("", addr + i);
+ ret = print_bits52("", addr + i);
+ ret = print_bits("", addr - i);
+ ret = print_bits52("", addr - i);
+ };
+ return ret
+}
diff --git a/test/c/read_write_ram.expect b/test/c/read_write_ram.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/read_write_ram.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/read_write_ram.sail b/test/c/read_write_ram.sail
new file mode 100644
index 00000000..751d15b5
--- /dev/null
+++ b/test/c/read_write_ram.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+$include <string.sail>
+$include <exception_basic.sail>
+
+val write_ram = "write_ram" : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmem}
+
+val read_ram = "read_ram" : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val main : unit -> unit effect {escape, wmem, rmem}
+
+function main() = {
+ write_ram(64, 4, 64^0x0, 64^0x8000_0000, 0x01020304);
+ let data = read_ram(64, 4, 64^0x0, 64^0x8000_0000);
+ assert(data == 0x01020304);
+ let data = read_ram(64, 3, 64^0x0, 64^0x8000_0001);
+ assert(data == 0x010203);
+ let data = read_ram(64, 3, 64^0x0, 64^0x8000_0000);
+ assert(data == 0x020304);
+ write_ram(64, 4, 64^0x0, 64^0x7fff_ffff, 0xA1B2C3D4);
+ let data = read_ram(64, 3, 64^0x0, 64^0x8000_0000);
+ assert(data == 0xA1B2C3);
+ print_endline("ok");
+} \ No newline at end of file
diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh
index 0990938d..37787605 100755
--- a/test/c/run_tests.sh
+++ b/test/c/run_tests.sh
@@ -54,7 +54,7 @@ function run_c_tests {
if $SAILDIR/sail -no_warn -c $SAIL_OPTS $file 1> ${file%.sail}.c 2> /dev/null;
then
green "compiling $(basename $file) ($SAIL_OPTS)" "ok";
- if gcc $CC_OPTS ${file%.sail}.c -lgmp -I $SAILDIR/lib;
+ if gcc $CC_OPTS ${file%.sail}.c $SAILDIR/lib/*.c -lgmp -lz -I $SAILDIR/lib;
then
green "compiling $(basename ${file%.sail}.c) ($CC_OPTS)" "ok";
$DIR/a.out 1> ${file%.sail}.result 2> /dev/null;
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
index d9ae07ba..39e34805 100755
--- a/test/ocaml/run_tests.sh
+++ b/test/ocaml/run_tests.sh
@@ -72,7 +72,7 @@ cd $DIR
for i in `ls -d */`;
do
cd $DIR/$i;
- if $SAILDIR/sail -no_warn -o out -ocaml_trace ../prelude.sail `ls *.sail` 1> /dev/null;
+ if $SAILDIR/sail -no_warn -o out -ocaml -trace ../prelude.sail `ls *.sail` 1> /dev/null;
then
./out > result 2> /dev/null;
if diff expect result;
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 03:01:02 +0000