diff options
| -rw-r--r-- | aarch64/main.sail | 16 | ||||
| -rw-r--r-- | aarch64/prelude.sail | 31 | ||||
| -rw-r--r-- | lib/elf.sail | 8 | ||||
| -rw-r--r-- | lib/flow.sail | 42 | ||||
| -rw-r--r-- | lib/smt.sail | 30 | ||||
| -rw-r--r-- | src/elf_loader.ml | 6 |
6 files changed, 96 insertions, 37 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 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/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/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 |