diff options
| -rw-r--r-- | aarch64/main.sail | 16 | ||||
| -rw-r--r-- | aarch64/prelude.sail | 31 | ||||
| -rw-r--r-- | lib/_tags | 4 | ||||
| -rw-r--r-- | lib/elf.sail | 8 | ||||
| -rw-r--r-- | lib/flow.sail | 42 | ||||
| -rw-r--r-- | lib/mono_rewrites.sail | 7 | ||||
| -rw-r--r-- | lib/smt.sail | 30 | ||||
| -rw-r--r-- | riscv/Makefile | 24 | ||||
| -rw-r--r-- | riscv/prelude.sail | 9 | ||||
| -rw-r--r-- | riscv/riscv.sail | 17 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 289 | ||||
| -rw-r--r-- | src/Makefile | 2 | ||||
| -rw-r--r-- | src/c_backend.ml | 257 | ||||
| -rw-r--r-- | src/elf_loader.ml | 6 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri128.ml | 2 | ||||
| -rw-r--r-- | src/monomorphise.ml | 70 | ||||
| -rw-r--r-- | src/monomorphise.mli | 5 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 2 | ||||
| -rw-r--r-- | src/process_file.ml | 8 | ||||
| -rw-r--r-- | src/type_check.ml | 11 | ||||
| -rw-r--r-- | test/ocaml/string_of_struct/expect | 0 | ||||
| -rw-r--r-- | test/ocaml/string_of_struct/sos.sail | 17 | ||||
| -rw-r--r-- | test/ocaml/string_of_struct/test.isail | 4 |
25 files changed, 766 insertions, 99 deletions
diff --git a/aarch64/main.sail b/aarch64/main.sail index b48f84d9..eaaf4f7f 100644 --- a/aarch64/main.sail +++ b/aarch64/main.sail @@ -1,12 +1,14 @@ -val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +$include <elf.sail> -function fetch_and_execute () = while true do { - let instr = aget_Mem(_PC, 4, AccType_IFETCH); - decode(instr); - if __BranchTaken then __BranchTaken = false else _PC = _PC + 4 -} +// Simple top level fetch and execute loop. +val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem} -val elf_entry = "Elf_loader.elf_entry" : unit -> int +function fetch_and_execute () = + while true do { + let instr = aget_Mem(_PC, 4, AccType_IFETCH); + decode(instr); + if __BranchTaken then __BranchTaken = false else _PC = _PC + 4 + } val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem} diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index da98b495..ab916e27 100644 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -1,25 +1,12 @@ default Order dec +$include <smt.sail> +$include <flow.sail> + type bits ('n : Int) = vector('n, dec, bit) infix 4 == -val div = { - smt : "div", - lem : "integerDiv" -} : forall 'n 'm. (atom('n), atom('m)) -> atom(div('n, 'm)) - -val mod = { - smt : "mod", - lem : "integerMod" -} : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm)) - -val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool -val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool - val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool @@ -86,16 +73,10 @@ val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) (' overload append = {bitvector_concat, vector_concat} -val not_bool = "not" : bool -> bool - val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) overload ~ = {not_bool, not_vec} -val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool - -function neq_atom (x, y) = not_bool(eq_atom(x, y)) - val neq_int = {lem: "neq"} : (int, int) -> bool function neq_int (x, y) = not_bool(eq_int(x, y)) @@ -110,8 +91,6 @@ function neq_anything (x, y) = not_bool(x == y) overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} -val and_bool = "and_bool" : (bool, bool) -> bool - val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -120,8 +99,6 @@ function and_vec (xs, ys) = builtin_and_vec(xs, ys) overload operator & = {and_bool, and_vec} -val or_bool = "or_bool" : (bool, bool) -> bool - val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -263,7 +240,7 @@ val abs_int = "abs_int" : int -> int val abs_real = "abs_real" : real -> real -overload abs = {abs_int, abs_real} +overload abs = {abs, abs_int, abs_real} val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat @@ -1,2 +1,2 @@ -<*.m{l,li}>: package(lem), package(linksem), package(zarith), package(uint) -<main.native>: package(lem), package(linksem), package(zarith), package(uint)
\ No newline at end of file +<*.m{l,li}>: package(lem), package(linksem), package(zarith) +<main.native>: package(lem), package(linksem), package(zarith)
\ No newline at end of file diff --git a/lib/elf.sail b/lib/elf.sail new file mode 100644 index 00000000..f158fbad --- /dev/null +++ b/lib/elf.sail @@ -0,0 +1,8 @@ +$ifndef _ELF +$define _ELF + +val elf_entry = "Elf_loader.elf_entry" : unit -> int + +val elf_tohost = "Elf_loader.elf_tohost" : unit -> int + +$endif diff --git a/lib/flow.sail b/lib/flow.sail new file mode 100644 index 00000000..cb7b1b99 --- /dev/null +++ b/lib/flow.sail @@ -0,0 +1,42 @@ +$ifndef _FLOW +$define _FLOW + +val not_bool = "not" : bool -> bool +val and_bool = "and_bool" : (bool, bool) -> bool +val or_bool = "or_bool" : (bool, bool) -> bool + +val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool + +val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool + +function neq_atom (x, y) = not_bool(eq_atom(x, y)) + +val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool +val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool +val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool +val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool + +val lt_range_atom = "lt" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val lteq_range_atom = "lteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val gt_range_atom = "gt" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val gteq_range_atom = "gteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val lt_atom_range = "lt" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val lteq_atom_range = "lteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val gt_atom_range = "gt" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool + +$ifdef TEST + +val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit + +function __flow_test (x, y) = { + if lteq_atom(x, y) then { + _prove(constraint('n <= 'm)) + } else { + _prove(constraint('n > 'm)) + } +} + +$endif + +$endif diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index fd1d1b23..a69dc379 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -122,3 +122,10 @@ function UInt_slice(xs,i,l) = { let xs = (xs & slice_mask(i,l)) >> i in UInt(xs) } + +val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure + +function zext_ones(m) = { + let v : bits('n) = extsv(0b1) in + v >> ('n - m) +} diff --git a/lib/smt.sail b/lib/smt.sail new file mode 100644 index 00000000..702b82c6 --- /dev/null +++ b/lib/smt.sail @@ -0,0 +1,30 @@ +$ifndef _SMT +$define _SMT + +// see http://smtlib.cs.uiowa.edu/theories-Ints.shtml + +val div = { + smt: "div", + ocaml: "quotient", + lem: "integerDiv" +} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)} + +val mod = { + smt: "mod", + ocaml: "modulus", + lem: "integerMod" +} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)} + +val abs = { + smt : "abs", + ocaml: "abs_int", + lem: "abs_int" +} : forall 'n. atom('n) -> {'o, 'o = abs('n). atom('o)} + +$ifdef TEST + +let __smt_x : atom(div(4, 2)) = div(8, 4) + +$endif + +$endif diff --git a/riscv/Makefile b/riscv/Makefile new file mode 100644 index 00000000..00451f6f --- /dev/null +++ b/riscv/Makefile @@ -0,0 +1,24 @@ +SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv.sail +SAIL_DIR ?= $(realpath ..) + +export SAIL_DIR + +all: riscv Riscv_embed_sequential.thy + +riscv: $(SAIL_SRCS) main.sail + $(SAIL_DIR)/sail -ocaml -o riscv $^ + +Riscv_embed_sequential.thy: riscv_embed_sequential.lem riscv_extras_embed_sequential.lem + lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \ + riscv_extras_embed_sequential.lem \ + riscv_embed_types_sequential.lem \ + riscv_embed_sequential.lem + +riscv_embed_sequential.lem: $(SAIL_SRCS) + $(SAIL_DIR)/sail -lem -o riscv -lem_sequential -lem_mwords -lem_lib Riscv_extras_embed $^ + +clean: + -rm -rf riscv _sbuild + -rm -f riscv_embed_sequential.lem riscv_embed_types_sequential.lem + -rm -f Riscv_embed_sequential.thy Riscv_embed_types_sequential.thy \ + Riscv_extras_embed_sequential.thy diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 5d56858c..6ddd56ab 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -331,6 +331,7 @@ union exception = { Error_not_implemented : string, Error_misaligned_access, Error_EBREAK, + Error_internal_error } val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) @@ -375,3 +376,11 @@ val vector64 : int -> bits(64) function vector64 n = __raw_GetSlice_int(64, n, 0) function break () : unit -> unit = () + +val vector_update_subrange_dec = "update_subrange" : forall 'n 'm 'o. + (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) + +val vector_update_subrange_inc = "update_subrange" : forall 'n 'm 'o. + (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) + +overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} diff --git a/riscv/riscv.sail b/riscv/riscv.sail index c19e84e6..7007086f 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -275,7 +275,22 @@ union clause ast = ECALL function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL) -function clause execute ECALL = not_implemented("ECALL is not implemented") +function clause execute ECALL = + let t : sync_exception = + struct { trap = match (cur_privilege) { + USER => User_ECall, + MACHINE => Machine_ECall + }, + badaddr = (None : option(regval)) } in + nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) + +/* ****************************************************************** */ +union clause ast = MRET + +function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET) + +function clause execute MRET = + nextPC = handle_exception_ctl(cur_privilege, CTL_MRET, PC) /* ****************************************************************** */ union clause ast = EBREAK diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail new file mode 100644 index 00000000..84002ed7 --- /dev/null +++ b/riscv/riscv_sys.sail @@ -0,0 +1,289 @@ +/* exception codes */ + +enum Interrupts = { + UserSWIntr, + SupervisorSWIntr, + ReservedIntr0, + MachineSWIntr, + + UserTimerIntr, + SupervisorTimerIntr, + ReservedIntr1, + MachineTimerIntr, + + UserExternalIntr, + SupervisorExternalIntr, + ReservedIntr2, + MachineExternalIntr +} + +enum ExceptionCode = { + Misaligned_Fetch, + Fetch_Access, + Illegal_Instr, + Breakpoint, + Misaligned_Load, + + Load_Access, + Misaligned_Store, + Store_Access, + + User_ECall, + Supervisor_ECall, + ReservedExc0, + Machine_ECall, + + Fetch_PageFault, + Load_PageFault, + ReservedExc1, + Store_PageFault +} + +/* machine mode registers */ + +/* FIXME: currently we have only those used by riscv-tests. */ + +bitfield Mstatus : bits(64) = { + SD : 63, + + SXL : 35 .. 34, + UXL : 33 .. 32, + + TSR : 22, + TW : 21, + TVM : 20, + MXR : 19, + SUM : 18, + MPRV : 17, + + XS : 16 .. 15, + FS : 14 .. 13, + + MPP : 12 .. 11, + SPP : 8, + + MPIE : 7, + SPIE : 5, + UPIE : 4, + + MIE : 3, + SIE : 1, + UIE : 0 +} +register mstatus : Mstatus + +bitfield Mip : bits(64) = { + MEIP : 11, + SEIP : 9, + UEIP : 8, + + MTIP : 7, + STIP : 5, + UTIP : 4, + + MSIP : 3, + SSIP : 1, + USIP : 0, + +} +register mip : Mip + +bitfield Mie : bits(64) = { + MEIE : 11, + SEIE : 9, + UEIE : 8, + + MTIE : 7, + STIE : 5, + UTIE : 4, + + MSIE : 3, + SSIE : 1, + USIE : 0, + +} +register mie : Mie + +bitfield Mideleg : bits(64) = { + MEID : 6, + SEID : 5, + UEID : 4, + + MTID : 6, + STID : 5, + UTID : 4, + + MSID : 3, + SSID : 1, + USID : 0 +} +register mideleg : Mideleg + +bitfield Medeleg : bits(64) = { + STORE_PAGE_FAULT : 15, + LOAD_PAGE_FAULT : 13, + FETCH_PAGE_FAULT : 12, + MACHINE_ECALL : 10, + SUPERVISOR_ECALL : 9, + USER_ECALL : 8, + STORE_ACCESS : 7, + MISALIGNED_STORE : 6, + LOAD_ACCESS : 5, + MISALIGNED_LOAD : 4, + BREAKPOINT : 3, + ILLEGAL_INSTR : 2, + FETCH_ACCESS : 1, + MISALIGNED_FETCH : 0 +} +register medeleg : Medeleg + +/* exception registers */ +register mepc : regval +register mtval : regval +register mtvec : regval +register mscratch : regval + +/* other registers */ + +register pmpaddr0 : regval +register pmpcfg0 : regval +/* TODO: this should be readonly, and always 0 for now */ +register mhartid : regval + +/* instruction control flow */ + +struct sync_exception = { + trap : ExceptionCode, + badaddr : option(regval) +} + +union ctl_result = { + CTL_TRAP : sync_exception, +/* TODO: + CTL_URET, + CTL_SRET, +*/ + CTL_MRET +} + +/* privilege level */ + +union privilege = { + MACHINE, + USER +} +register cur_privilege : privilege + +function priv_to_bits(p : privilege) -> bits(2) = + match (p) { + USER => 0b00, + MACHINE => 0b11 + } +function bits_to_priv(b : bits(2)) -> privilege = + match (b) { + 0b00 => USER, + 0b11 => MACHINE + } + +/* handle exceptional ctl flow by updating nextPC */ + +function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result, + pc: regval) -> regval = + /* TODO: check delegation */ + match (cur_priv, ctl) { + (_, CTL_TRAP(e)) => { + mepc = pc; + mcause = e.trap; + + mstatus->MPIE() = mstatus.MIE(); + mstatus->MIE() = false; + mstatus->MPP() = priv_to_bits(cur_priv); + cur_privilege = MACHINE; + + match (e.trap) { + Misaligned_Fetch => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + Fetch_Access => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + Illegal_Instr => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + + Breakpoint => not_implemented("breakpoint"), + + Misaligned_Load => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + Load_Access => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + Misaligned_Store => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + Store_Access => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + + User_ECall => { + mtval = EXTZ(0b0) + }, + Supervisor_ECall => { + mtval = EXTZ(0b0) + }, + Machine_ECall => { + mtval = EXTZ(0b0) + }, + + Fetch_PageFault => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + Load_PageFault => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + }, + Store_PageFault => { + match (e.badaddr) { + Some(a) => mtval = a, + None => throw(Error_internal_error) + } + } + }; + /* TODO: make register read explicit */ + mtvec + }, + (_, CTL_MRET) => { + mstatus->MIE() = mstatus.MPIE(); + mstatus->MPIE() = true; + cur_privilege = bits_to_priv(mstatus.MPP()); + mstatus->MPP() = priv_to_bits(USER); + mepc + } + } diff --git a/src/Makefile b/src/Makefile index 325cbec6..85c5abba 100644 --- a/src/Makefile +++ b/src/Makefile @@ -270,4 +270,4 @@ doc: ocamlbuild -use-ocamlfind sail.docdir/index.html lib: - ocamlbuild pretty_print.cmxa pretty_print.cma + ocamlbuild -use-ocamlfind pretty_print.cmxa pretty_print.cma diff --git a/src/c_backend.ml b/src/c_backend.ml index c1f5ddb9..b06cd950 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -63,42 +63,102 @@ let lvar_typ = function | Register typ -> typ | _ -> assert false +(* + +1) Conversion to ANF + + tannot defs -> (typ, aexp) cdefs + +2) Primitive operation optimizations + +3) Lowering to low-level imperative language + + (typ, aexp) cdefs -> (ctyp, instr list) cdefs + +4) Low level optimizations (e.g. reducing allocations) + +5) Generation of C code + + (ctyp, instr list) -> string + +*) + (**************************************************************************) (* 1. Conversion to A-normal form (ANF) *) (**************************************************************************) +(* The first step in compiling sail is converting the Sail expression + grammar into A-normal form. Essentially this converts expressions + such as f(g(x), h(y)) into something like: + + let v0 = g(x) in let v1 = h(x) in f(v0, v1) + + Essentially the arguments to every function must be trivial, and + complex expressions must be let bound to new variables, or used in + a block, assignment, or control flow statement (if, for, and + while/until loops). The aexp datatype represents these expressions, + while aval represents the trivial values. + + The X_aux construct in ast.ml isn't used here, but the typing + information is collapsed into the aexp and aval types. The + convention is that the type of an aexp is given by last argument to + a constructor. It is omitted where it is obvious - for example all + for loops have unit as their type. If some constituent part of the + aexp has an annotation, the it refers to the previous argument, so + in + + AE_let (id, typ1, _, body, typ2) + + typ1 is the type of the bound identifer, whereas typ2 is the type + of the whole let expression (and therefore also the body). + + See Flanagan et al's 'The Essence of Compiling with Continuations' *) type aexp = | AE_val of aval | AE_app of id * aval list * typ | AE_cast of aexp * typ - | AE_assign of id * aexp + | AE_assign of id * typ * aexp | AE_let of id * typ * aexp * aexp * typ | AE_block of aexp list * aexp * typ | AE_return of aval * typ + | AE_throw of aval + | AE_if of aval * aexp * aexp * typ + | AE_for of id * aexp * aexp * aexp * order * aexp + | AE_loop of loop * aexp * aexp and aval = | AV_lit of lit * typ | AV_id of id * lvar + | AV_ref of id * lvar | AV_tuple of aval list | AV_C_fragment of string * typ +(* Map over all the avals in an aexp. *) let rec map_aval f = function | AE_val v -> AE_val (f v) | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ) - | AE_assign (id, aexp) -> AE_assign (id, map_aval f aexp) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_aval f aexp) | AE_app (id, vs, typ) -> AE_app (id, List.map f vs, typ) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> + AE_let (id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ) | AE_return (aval, typ) -> AE_return (f aval, typ) + | AE_if (aval, aexp1, aexp2, typ2) -> + AE_if (f aval, map_aval f aexp1, map_aval f aexp2, typ2) +(* Map over all the functions in an aexp. *) let rec map_functions f = function | AE_app (id, vs, typ) -> f id vs typ | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ) - | AE_assign (id, aexp) -> AE_assign (id, map_functions f aexp) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp) | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2) | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) + | AE_if (aval, aexp1, aexp2, typ) -> + AE_if (aval, map_functions f aexp1, map_functions f aexp2, typ) | AE_val _ | AE_return _ as v -> v +(* For debugging we provide a pretty printer for ANF expressions. *) + let pp_id ?color:(color=Util.green) id = string (string_of_id id |> color |> Util.clear) @@ -123,8 +183,8 @@ let rec pp_aexp = function | AE_val v -> pp_aval v | AE_cast (aexp, typ) -> pp_annot typ (string "$" ^^ pp_aexp aexp) - | AE_assign (id, aexp) -> - pp_id id ^^ string " := " ^^ pp_aexp aexp + | AE_assign (id, typ, aexp) -> + pp_annot typ (pp_id id) ^^ string " := " ^^ pp_aexp aexp | AE_app (id, args, typ) -> pp_annot typ (pp_id ~color:Util.red id ^^ parens (separate_map (comma ^^ space) pp_aval args)) | AE_let (id, id_typ, binding, body, typ) -> group @@ -138,6 +198,10 @@ let rec pp_aexp = function pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="; pp_aexp binding; string "in"]) ^^ hardline ^^ pp_aexp body end + | AE_if (cond, then_aexp, else_aexp, typ) -> + pp_annot typ (separate space [ string "if"; pp_aval cond; + string "then"; pp_aexp then_aexp; + string "else"; pp_aexp else_aexp ]) | AE_block (aexps, aexp, typ) -> pp_annot typ (surround 2 0 lbrace (pp_block (aexps @ [aexp])) rbrace) | AE_return (v, typ) -> pp_annot typ (string "return" ^^ parens (pp_aval v)) @@ -169,7 +233,7 @@ let rec split_block = function exp :: exps, last | [] -> failwith "empty block" -let rec anf (E_aux (e_aux, _) as exp) = +let rec anf (E_aux (e_aux, exp_annot) as exp) = let to_aval = function | AE_val v -> (v, fun x -> x) | AE_app (_, _, typ) | AE_let (_, _, _, _, typ) | AE_return (_, typ) | AE_cast (_, typ) as aexp -> @@ -187,8 +251,19 @@ let rec anf (E_aux (e_aux, _) as exp) = | E_assign (LEXP_aux (LEXP_id id, _), exp) -> let aexp = anf exp in - AE_assign (id, aexp) - + AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp) + + | E_if (cond, then_exp, else_exp) -> + let cond_val, wrap = to_aval (anf cond) in + let then_aexp = anf then_exp in + let else_aexp = anf else_exp in + wrap (AE_if (cond_val, then_aexp, else_aexp, typ_of then_exp)) + + | E_app_infix (x, Id_aux (Id op, l), y) -> + anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot)) + | E_app_infix (x, Id_aux (DeIid op, l), y) -> + anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), exp_annot)) + | E_app (id, exps) -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in @@ -232,6 +307,7 @@ let rec anf (E_aux (e_aux, _) as exp) = let aval, wrap = to_aval (anf exp) in wrap (AE_return (aval, typ_of exp)) + | E_var (LEXP_aux (LEXP_id id, _), binding, body) | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> let env = env_of body in let lvar = Env.lookup_id id env in @@ -260,7 +336,13 @@ let rec anf (E_aux (e_aux, _) as exp) = (* Sizeof nodes removed by sizeof rewriting pass *) failwith "encountered E_sizeof or E_constraint node when converting to ANF" + | E_nondet _ -> + (* We don't compile E_nondet nodes *) + failwith "encountered E_nondet node when converting to ANF" + + (* | _ -> failwith ("Cannot convert to ANF: " ^ string_of_exp exp) + *) (**************************************************************************) (* 2. Converting sail types to C types *) @@ -270,13 +352,30 @@ let max_int64 = Big_int.of_int64 Int64.max_int let min_int64 = Big_int.of_int64 Int64.min_int type ctyp = + (* Arbitrary precision GMP integer, mpz_t in C. *) | CT_mpz + (* Variable length bitvector - flag represents direction, inc or dec *) | CT_bv of bool + (* Fixed length bitvector that fits within a 64-bit word. - int + represents length, and flag is the same as CT_bv. *) | CT_uint64 of int * bool | CT_int + (* Used for (signed) integers that fit within 64-bits. *) | CT_int64 + (* unit is a value in sail, so we represent it as a one element type + here too for clarity but we actually compile it to an int which + is always 0. *) | CT_unit - + | CT_bool + (* Abstractly represent how all the Sail user defined types get + mapped into C. We don't fully worry about precise implementation + details at this point, as C doesn't have variants or tuples + natively, but these need to be encoded. *) + | CT_tup of ctyp list + | CT_struct of id * ctyp Bindings.t + | CT_enum of id * IdSet.t + | CT_variant of id * ctyp Bindings.t + let ctyp_equal ctyp1 ctyp2 = match ctyp1, ctyp2 with | CT_mpz, CT_mpz -> true @@ -284,6 +383,8 @@ let ctyp_equal ctyp1 ctyp2 = | CT_uint64 (m1, d1), CT_uint64 (m2, d2) -> m1 = m2 && d1 = d2 | CT_int, CT_int -> true | CT_int64, CT_int64 -> true + | CT_unit, CT_unit -> true + | CT_bool, CT_bool -> true | _, _ -> false let string_of_ctyp = function @@ -295,12 +396,13 @@ let string_of_ctyp = function | CT_int64 -> "int64_t" | CT_int -> "int" | CT_unit -> "unit" + | CT_bool -> "bool" (* Convert a sail type into a C-type *) let ctyp_of_typ (Typ_aux (typ_aux, _) as typ) = match typ_aux with | Typ_id id when string_of_id id = "bit" -> CT_int - | Typ_id id when string_of_id id = "bool" -> CT_int + | Typ_id id when string_of_id id = "bool" -> CT_bool | Typ_id id when string_of_id id = "int" -> CT_mpz | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" -> begin @@ -324,10 +426,10 @@ let ctyp_of_typ (Typ_aux (typ_aux, _) as typ) = | _ -> CT_bv direction end | Typ_id id when string_of_id id = "unit" -> CT_unit - | _ -> assert false + | _ -> failwith ("No C-type for type " ^ string_of_typ typ) let is_stack_ctyp ctyp = match ctyp with - | CT_uint64 _ | CT_int64 | CT_int -> true + | CT_uint64 _ | CT_int64 | CT_int | CT_unit | CT_bool -> true | CT_bv _ | CT_mpz -> false let is_stack_typ typ = is_stack_ctyp (ctyp_of_typ typ) @@ -344,11 +446,13 @@ let literal_to_cstring (L_aux (l_aux, _) as lit) = let padding = 16 - String.length str in Some ("0x" ^ String.make padding '0' ^ str ^ "ul") | L_unit -> Some "0" + | L_true -> Some "true" + | L_false -> Some "false" | _ -> None let c_literals = let c_literal = function - | AV_lit (lit, typ) as v -> + | AV_lit (lit, typ) as v when is_stack_ctyp (ctyp_of_typ typ) -> begin match literal_to_cstring lit with | Some str -> AV_C_fragment (str, typ) @@ -474,11 +578,13 @@ type instr = | I_decl of ctyp * id | I_alloc of ctyp * id | I_init of ctyp * id * cval + | I_if of cval * instr list * instr list * ctyp | I_funcall of id * id * cval list * ctyp | I_convert of id * ctyp * id * ctyp | I_assign of id * cval | I_clear of ctyp * id | I_return of id + | I_comment of string type cdef = | CDEF_reg_dec of ctyp * id @@ -494,9 +600,15 @@ and pp_cval = function | CV_id (id, ctyp) -> parens (pp_ctyp ctyp) ^^ (pp_id id) | CV_C_fragment (str, ctyp) -> parens (pp_ctyp ctyp) ^^ (string (str |> Util.cyan |> Util.clear)) -let pp_instr = function +let rec pp_instr = function | I_decl (ctyp, id) -> parens (pp_ctyp ctyp) ^^ space ^^ pp_id id + | I_if (cval, then_instrs, else_instrs, ctyp) -> + let pp_if_block instrs = surround 2 0 lbrace (separate_map hardline pp_instr instrs) rbrace in + parens (pp_ctyp ctyp) ^^ space + ^^ pp_keyword "IF" ^^ pp_cval cval + ^^ pp_keyword "THEN" ^^ pp_if_block then_instrs + ^^ pp_keyword "ELSE" ^^ pp_if_block else_instrs | I_alloc (ctyp, id) -> pp_keyword "ALLOC" ^^ parens (pp_ctyp ctyp) ^^ space ^^ pp_id id | I_init (ctyp, id, cval) -> @@ -515,7 +627,9 @@ let pp_instr = function pp_keyword "CLEAR" ^^ pp_ctyp ctyp ^^ parens (pp_id id) | I_return id -> pp_keyword "RETURN" ^^ pp_id id - + | I_comment str -> + string ("// " ^ str) + let compile_funcall env id args typ = let setup = ref [] in let cleanup = ref [] in @@ -591,11 +705,61 @@ let rec compile_aexp env = function | AE_val (AV_C_fragment (c, typ)) -> let ctyp = ctyp_of_typ typ in [], ctyp, (fun id -> I_assign (id, CV_C_fragment (c, ctyp))), [] - + | AE_val (AV_id (id, lvar)) -> let ctyp = ctyp_of_typ (lvar_typ lvar) in - [], CT_unit, (fun id -> I_assign (id, CV_id (id, ctyp))), [] + [], ctyp, (fun id' -> I_assign (id', CV_id (id, ctyp))), [] + | AE_val (AV_lit (lit, typ)) -> + let ctyp = ctyp_of_typ typ in + if is_stack_ctyp ctyp then + assert false + else + let gs = gensym () in + [I_alloc (ctyp, gs); I_comment "fix literal init"], + ctyp, + (fun id -> I_assign (id, CV_id (gs, ctyp))), + [I_clear (ctyp, gs)] + + | AE_if (aval, then_aexp, else_aexp, if_typ) -> + let if_ctyp = ctyp_of_typ if_typ in + let compile_branch aexp = + let setup, ctyp, call, cleanup = compile_aexp env aexp in + fun id -> setup @ [call id] @ cleanup + in + let setup, ctyp, call, cleanup = compile_aexp env (AE_val aval) in + let gs = gensym () in + setup @ [I_decl (ctyp, gs); call gs], + if_ctyp, + (fun id -> I_if (CV_id (gs, ctyp), + compile_branch then_aexp id, + compile_branch else_aexp id, + if_ctyp)), + cleanup + + | AE_assign (id, assign_typ, aexp) -> + (* assign_ctyp is the type of the C variable we are assigning to, + ctyp is the type of the C expression being assigned. These may + be different. *) + let assign_ctyp = ctyp_of_typ assign_typ in + let setup, ctyp, call, cleanup = compile_aexp env aexp in + let unit_fragment = CV_C_fragment ("0", CT_unit) in + let comment = "assign " ^ string_of_ctyp assign_ctyp ^ " := " ^ string_of_ctyp ctyp in + if ctyp_equal assign_ctyp ctyp then + setup @ [call id], CT_unit, (fun id -> I_assign (id, unit_fragment)), cleanup + else if not (is_stack_ctyp assign_ctyp) && is_stack_ctyp ctyp then + let gs = gensym () in + setup @ [ I_comment comment; + I_decl (ctyp, gs); + call gs; + I_convert (id, assign_ctyp, gs, ctyp) + ], + CT_unit, + (fun id -> I_assign (id, unit_fragment)), + cleanup + else + failwith ("Failure: " ^ comment) + | AE_block (aexps, aexp, _) -> let block = compile_block env aexps in let setup, ctyp, call, cleanup = compile_aexp env aexp in @@ -611,6 +775,12 @@ and compile_block env = function let gs = gensym () in setup @ [I_decl (CT_unit, gs); call gs] @ cleanup @ rest +let rec pat_ids (P_aux (p_aux, _)) = + match p_aux with + | P_id id -> [id] + | P_tup pats -> List.concat (List.map pat_ids pats) + | _ -> failwith "Bad pattern" + let compile_def env = function | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) -> [CDEF_reg_dec (ctyp_of_typ typ, id)] @@ -632,10 +802,12 @@ let compile_def env = function else assert false in - [CDEF_fundef (id, [], instrs)] + [CDEF_fundef (id, pat_ids pat, instrs)] | _ -> assert false end + | DEF_default _ -> [] + | _ -> assert false (**************************************************************************) @@ -648,6 +820,7 @@ let codegen_id id = string (sgen_id id) let sgen_ctyp = function | CT_unit -> "int" | CT_int -> "int" + | CT_bool -> "bool" | CT_uint64 _ -> "uint64_t" | CT_int64 -> "int64_t" | CT_mpz -> "mpz_t" @@ -658,11 +831,20 @@ let sgen_cval = function | CV_id (id, _) -> string_of_id id | _ -> "CVAL??" -let codegen_instr = function +let rec codegen_instr = function | I_decl (ctyp, id) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (string_of_id id)) | I_assign (id, cval) -> - string (Printf.sprintf "%s = %s;" (string_of_id id) (sgen_cval cval)) + let ctyp = cval_ctyp cval in + if is_stack_ctyp ctyp then + string (Printf.sprintf "%s = %s;" (string_of_id id) (sgen_cval cval)) + else + string (Printf.sprintf "set_%s(%s, %s);" (sgen_ctyp ctyp) (string_of_id id) (sgen_cval cval)) + | I_if (cval, then_instrs, else_instrs, ctyp) -> + string "if" ^^ space ^^ parens (string (sgen_cval cval)) ^^ space + ^^ surround 2 0 lbrace (separate_map hardline codegen_instr then_instrs) rbrace + ^^ space ^^ string "else" ^^ space + ^^ surround 2 0 lbrace (separate_map hardline codegen_instr else_instrs) rbrace | I_funcall (x, f, args, ctyp) -> let args = Util.string_of_list ", " sgen_cval args in if is_stack_ctyp ctyp then @@ -682,20 +864,39 @@ let codegen_instr = function ^^ hardline ^^ string (Printf.sprintf "init_%s(%s);" (sgen_ctyp ctyp) (string_of_id id)) | I_convert (x, ctyp1, y, ctyp2) -> - string (Printf.sprintf "%s = convert_%s_of_%s(%s);" - (string_of_id x) - (sgen_ctyp ctyp1) - (sgen_ctyp ctyp2) - (string_of_id y)) + if is_stack_ctyp ctyp1 then + string (Printf.sprintf "%s = convert_%s_of_%s(%s);" + (string_of_id x) + (sgen_ctyp ctyp1) + (sgen_ctyp ctyp2) + (string_of_id y)) + else + string (Printf.sprintf "convert_%s_of_%s(%s, %s);" + (sgen_ctyp ctyp1) + (sgen_ctyp ctyp2) + (string_of_id x) + (string_of_id y)) | I_return id -> string (Printf.sprintf "return %s;" (string_of_id id)) + | I_comment str -> + string ("/* " ^ str ^ " */") let codegen_def env = function | CDEF_reg_dec (ctyp, id) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) - | CDEF_fundef (id, _, instrs) -> + | CDEF_fundef (id, args, instrs) -> List.iter (fun instr -> print_endline (Pretty_print_sail.to_string (pp_instr instr))) instrs; - codegen_id id ^^ hardline + let _, Typ_aux (fn_typ, _) = Env.get_val_spec id env in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ + | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ + | _ -> assert false + in + let arg_ctyps, ret_ctyp = List.map ctyp_of_typ arg_typs, ctyp_of_typ ret_typ in + + let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in + + string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline ^^ string "{" ^^ jump 2 2 (separate_map hardline codegen_instr instrs) ^^ hardline ^^ string "}" diff --git a/src/elf_loader.ml b/src/elf_loader.ml index feacdf3d..83c36821 100644 --- a/src/elf_loader.ml +++ b/src/elf_loader.ml @@ -118,9 +118,9 @@ let load_segment seg = let load_elf name = let segments, e_entry, symbol_map = read name in opt_elf_entry := e_entry; - if List.mem_assoc "tohost" symbol_map then - let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in - opt_elf_tohost := tohost_addr; + (if List.mem_assoc "tohost" symbol_map then + let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in + opt_elf_tohost := tohost_addr); List.iter load_segment segments (* The sail model can access this by externing a unit -> int function diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 8533827b..bb56c8a9 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -727,7 +727,7 @@ let initial_system_state_of_elf_file name = aarch64_register_data_all) *) | 8 (* EM_MIPS *) -> let startaddr = - let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in + let e_entry = Uint64_wrapper.of_bigint e_entry in match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with | Error.Fail s -> failwith "Failed computing entry point" | Error.Success s -> s diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index 46bc92fb..3d187aa9 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name = match Nat_big_num.to_int e_machine with | 8 (* EM_MIPS *) -> let startaddr = - let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in + let e_entry = Uint64_wrapper.of_bigint e_entry in match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with | Error.Fail s -> failwith "Failed computing entry point" | Error.Success s -> s diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 5e5bee21..6b12ebbb 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name = match Nat_big_num.to_int e_machine with | 8 (* EM_MIPS *) -> let startaddr = - let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in + let e_entry = Uint64_wrapper.of_bigint e_entry in match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with | Error.Fail s -> failwith "Failed computing entry point" | Error.Success s -> s diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 2e7ad08f..0baaf139 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -899,7 +899,8 @@ let rec freshen_pat_bindings p = (* Use the location pairs in choices to reduce case expressions at the first location to the given case at the second. *) let apply_pat_choices choices = - let rewrite_constraint (NC_aux (nc,l) as nconstr) = + let rewrite_constraint (NC_aux (nc,l) as nconstr) = E_constraint nconstr (* + Not right now - false cases may not type check match List.assoc l choices with | choice,_ -> begin match nc with @@ -907,7 +908,7 @@ let apply_pat_choices choices = E_constraint (NC_aux ((if choice < List.length is then NC_true else NC_false), Generated l)) | _ -> E_constraint nconstr end - | exception Not_found -> E_constraint nconstr + | exception Not_found -> E_constraint nconstr*) in let rewrite_case (e,cases) = match List.assoc (exp_loc e) choices with @@ -1504,11 +1505,16 @@ let split_defs continue_anyway splits defs = | Some (Some (pats,l)) -> Some (List.mapi (fun i p -> match p with - | P_aux (P_lit lit,_) when (match lit with L_aux (L_undef,_) -> false | _ -> true) -> - p,[id,E_aux (E_lit lit,(Generated Unknown,None))],[l,(i,[])] + | P_aux (P_lit lit,(pl,pannot)) + when (match lit with L_aux (L_undef,_) -> false | _ -> true) -> + p,[id,E_aux (E_lit lit,(Generated pl,pannot))],[l,(i,[])] | _ -> let p',subst = freshen_pat_bindings p in - P_aux (P_as (p',id),(l,annot)),[],[l,(i,subst)]) + match p' with + | P_aux (P_wild,_) -> + P_aux (P_id id,(l,annot)),[],[l,(i,subst)] + | _ -> + P_aux (P_as (p',id),(l,annot)),[],[l,(i,subst)]) pats) ) | P_app (id,ps) -> @@ -2226,6 +2232,7 @@ let merge rs rs' = { } type env = { + top_kids : kid list; var_deps : dependencies Bindings.t; kid_deps : dependencies KBindings.t } @@ -2248,7 +2255,7 @@ let update_env env deps pat = let var_deps = List.fold_left (fun ds v -> Bindings.add v deps ds) env.var_deps bound in let kbound = kids_bound_by_pat pat in let kid_deps = KidSet.fold (fun v ds -> KBindings.add v deps ds) kbound env.kid_deps in - { var_deps = var_deps; kid_deps = kid_deps } + { env with var_deps = var_deps; kid_deps = kid_deps } let assigned_vars_exps es = List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp)) @@ -2384,6 +2391,18 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps = | None -> None) | _ -> None +let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) = + let is_equal kid = + prove typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + in + match ne with + | Nexp_var _ + | Nexp_constant _ -> nexp + | _ -> + match List.find is_equal env.top_kids with + | kid -> Nexp_aux (Nexp_var kid,Generated l) + | exception Not_found -> nexp + (* Takes an environment of dependencies on vars, type vars, and flow control, and dependencies on mutable variables. The latter are quite conservative, we currently drop variables assigned inside loops, for example. *) @@ -2600,6 +2619,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let typ = Env.expand_synonyms tenv typ in if is_bitvector_typ typ then let _,size,_,_ = vector_typ_args_of typ in + let size = simplify_size_nexp env tenv size in match deps_of_nexp env.kid_deps [] size with | Have (args,caller,caller_kids) -> { r with @@ -2664,8 +2684,8 @@ let initial_env fn_id (TypQ_aux (tq,_)) pat set_assertions = (match KBindings.find kid set_assertions with | (l,is) -> let l' = Generated l in - let pats = List.map (fun n -> P_aux (P_lit (L_aux (L_num n,l')),(l',None))) is in - let pats = pats @ [P_aux (P_wild,(l',None))] in + let pats = List.map (fun n -> P_aux (P_lit (L_aux (L_num n,l')),(l',snd annot))) is in + let pats = pats @ [P_aux (P_wild,(l',snd annot))] in Partial (pats,l) | exception Not_found -> Total) | _ -> Total @@ -2736,7 +2756,8 @@ let initial_env fn_id (TypQ_aux (tq,_)) pat set_assertions = let _,var_deps,kid_deps = split3 (List.mapi arg pats) in let var_deps = List.fold_left dep_bindings_merge Bindings.empty var_deps in let kid_deps = List.fold_left dep_kbindings_merge kid_quant_deps kid_deps in - { var_deps = var_deps; kid_deps = kid_deps } + let top_kids = List.map fst (KBindings.bindings kid_quant_deps) in + { top_kids = top_kids; var_deps = var_deps; kid_deps = kid_deps } (* When there's more than one pick the first *) let merge_set_asserts _ x y = @@ -3059,6 +3080,10 @@ let rewrite_app env typ (id,args) = when is_slice slice1 && not (is_constant length1) -> E_app (mk_id "zext_slice", [vector1; start1; length1]) + | [E_aux (E_app (ones, [len1]),_); + _ (* unnecessary ZeroExtend length *)] -> + E_app (mk_id "zext_ones", [len1]) + | _ -> E_app (id,args) else if is_id env (Id "SignExtend") id then @@ -3099,15 +3124,23 @@ type options = { debug_analysis : int; rewrites : bool; rewrite_size_parameters : bool; - all_split_errors : bool + all_split_errors : bool; + dump_raw: bool } +let recheck defs = + let w = !Util.opt_warnings in + let () = Util.opt_warnings := false in + let r = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in + let () = Util.opt_warnings := w in + r + let monomorphise opts splits env defs = let (defs,env) = if opts.rewrites then let defs = MonoRewrites.mono_rewrite defs in (* TODO: is this necessary? *) - Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs + recheck defs else (defs,env) in (*let _ = Pretty_print.pp_defs stdout defs in*) @@ -3121,9 +3154,12 @@ let monomorphise opts splits env defs = (* TODO: currently doing this because constant propagation leaves numeric literals as int, try to avoid this later; also use final env for DEF_spec case above, because the type checker doesn't store the env at that point :( *) - if opts.rewrite_size_parameters then - let (defs,env) = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in - let defs = AtomToItself.rewrite_size_parameters env defs in - defs - else - defs + let defs = if opts.rewrite_size_parameters then + let (defs,env) = recheck defs in + let defs = AtomToItself.rewrite_size_parameters env defs in + defs + else + defs + in + let () = if opts.dump_raw then Pretty_print_sail.pp_defs stdout defs else () in + recheck defs diff --git a/src/monomorphise.mli b/src/monomorphise.mli index 8e0c1ede..11713511 100644 --- a/src/monomorphise.mli +++ b/src/monomorphise.mli @@ -53,7 +53,8 @@ type options = { debug_analysis : int; (* Debug output level for the automatic analysis *) rewrites : bool; (* Experimental rewrites for variable-sized operations *) rewrite_size_parameters : bool; (* Make implicit type parameters explicit for (e.g.) lem *) - all_split_errors : bool + all_split_errors : bool; + dump_raw: bool } val monomorphise : @@ -61,4 +62,4 @@ val monomorphise : ((string * int) * string) list -> (* List of splits from the command line *) Type_check.Env.t -> Type_check.tannot Ast.defs -> - Type_check.tannot Ast.defs + Type_check.tannot Ast.defs * Type_check.Env.t diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 96dfd9d3..c535554b 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -528,7 +528,7 @@ let ocaml_string_of_enum ctx id ids = let ocaml_string_of_struct ctx id typq fields = let arg = gensym () in let ocaml_field (typ, id) = - separate space [string (string_of_id id ^ " = \""); string "^"; ocaml_string_typ typ arg ^^ string "." ^^ zencode ctx id] + separate space [string (string_of_id id ^ " = \""); string "^"; ocaml_string_typ typ (arg ^^ string "." ^^ zencode ctx id)] in separate space [string "let"; ocaml_string_of id; parens (arg ^^ space ^^ colon ^^ space ^^ zencode ctx id); equals] ^//^ (string "\"{" ^^ separate_map (hardline ^^ string "^ \", ") ocaml_field fields ^^ string " ^ \"}\"") diff --git a/src/process_file.ml b/src/process_file.ml index cb8c8011..1ba8069f 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -196,12 +196,10 @@ let monomorphise_ast locs type_env ast = debug_analysis = !opt_dmono_analysis; rewrites = !opt_mono_rewrites; rewrite_size_parameters = !Pretty_print_lem.opt_mwords; - all_split_errors = !opt_dall_split_errors + all_split_errors = !opt_dall_split_errors; + dump_raw = !opt_ddump_raw_mono_ast } in - let ast = monomorphise opts locs type_env ast in - let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail.pp_defs stdout ast else () in - let ienv = Type_check.Env.no_casts Type_check.initial_env in - Type_check.check ienv ast + monomorphise opts locs type_env ast let open_output_with_check file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in diff --git a/src/type_check.ml b/src/type_check.ml index 41438592..a49807ce 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2020,6 +2020,12 @@ let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) - let strip_pexp : 'a pexp -> unit pexp = function pexp -> map_pexp_annot (fun (l, _) -> (l, ())) pexp let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, _) -> (l, ())) lexp +let fresh_var = + let counter = ref 0 in + fun () -> let n = !counter in + let () = counter := n+1 in + mk_id ("v#" ^ string_of_int n) + let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp = let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in let add_effect exp eff = match exp with @@ -2470,8 +2476,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) | exception (Type_error _ as typ_exn) -> match pat_aux with | P_lit lit -> - let guard = mk_exp (E_app_infix (mk_exp (E_id (mk_id "p#")), mk_id "==", mk_exp (E_lit lit))) in - let (typed_pat, env, guards) = bind_pat env (mk_pat (P_id (mk_id "p#"))) typ in + let var = fresh_var () in + let guard = mk_exp (E_app_infix (mk_exp (E_id var), mk_id "==", mk_exp (E_lit lit))) in + let (typed_pat, env, guards) = bind_pat env (mk_pat (P_id var)) typ in typed_pat, env, guard::guards | _ -> raise typ_exn diff --git a/test/ocaml/string_of_struct/expect b/test/ocaml/string_of_struct/expect new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/test/ocaml/string_of_struct/expect diff --git a/test/ocaml/string_of_struct/sos.sail b/test/ocaml/string_of_struct/sos.sail new file mode 100644 index 00000000..6d14dfd7 --- /dev/null +++ b/test/ocaml/string_of_struct/sos.sail @@ -0,0 +1,17 @@ +/* This is a regression test for a bug where an option type in a +struct would cause the ocaml backend to generate a bad string_of +function for the struct */ + +union option ('a : Type) = { + None, + Some : 'a +} + +struct test = { + test1 : int, + test2 : option(int) +} + +val main : unit -> unit + +function main () = ()
\ No newline at end of file diff --git a/test/ocaml/string_of_struct/test.isail b/test/ocaml/string_of_struct/test.isail new file mode 100644 index 00000000..6a9595e3 --- /dev/null +++ b/test/ocaml/string_of_struct/test.isail @@ -0,0 +1,4 @@ +:output result +main() +:run +:quit
\ No newline at end of file |