diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/Makefile | 13 | ||||
| -rw-r--r-- | mips/_CoqProject | 2 | ||||
| -rw-r--r-- | mips/mips_extras.lem | 8 | ||||
| -rw-r--r-- | mips/mips_extras.v | 20 | ||||
| -rw-r--r-- | mips/mips_insts.sail | 53 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 1 | ||||
| -rw-r--r-- | mips/mips_rmem.sail | 15 | ||||
| -rw-r--r-- | mips/mips_wrappers.sail | 4 | ||||
| -rw-r--r-- | mips/prelude.sail | 16 |
9 files changed, 81 insertions, 51 deletions
diff --git a/mips/Makefile b/mips/Makefile index fa1f9fa0..03144f50 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -18,7 +18,7 @@ mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) ../sail mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail $(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@ -C_WARNINGS=-Wall -Wno-unused-but-set-variable -Wno-unused-label -Wno-maybe-uninitialized +C_WARNINGS=-Wall -Wno-unused-but-set-variable -Wno-unused-label -Wno-unused-function -Wno-maybe-uninitialized C_OPT=-O2 GCOV_FLAGS= mips_c: mips.c ../lib/sail.h ../lib/*.c Makefile @@ -47,12 +47,19 @@ mips.v: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(SAIL) -coq -dcoq_undef_axioms -o mips -coq_lib mips_extras -undefined_gen -memo_z3 $^ mips_types.v: mips.v +MIPS_COQ = mips_types.v mips_extras.v mips.v +COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail + +%.vo: %.v + coqc $(COQ_LIBS) $< +mips.vo: mips_types.vo mips_extras.vo + M%.thy: m%.lem m%_types.lem mips_extras.lem lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy %Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem - lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -i $(SAIL_DIR)/lib/hol/sail2_prompt_monad.lem -i $(SAIL_DIR)/lib/hol/sail2_prompt.lem -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ %Theory.uo: %Script.sml Holmake $@ @@ -63,5 +70,5 @@ include ../etc/loc.mk clean: rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild mips.c mips_c rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml - rm -f mips.v mips_types.v + rm -f mips.v mips_types.v $(MIPS_COQ:%.v=%.vo) $(MIPS_COQ:%.v=%.glob) $(MIPS_COQ:%.v=.%.aux) -Holmake cleanAll diff --git a/mips/_CoqProject b/mips/_CoqProject new file mode 100644 index 00000000..ad38d28d --- /dev/null +++ b/mips/_CoqProject @@ -0,0 +1,2 @@ +-R ../../bbv/theories bbv +-R ../lib/coq Sail
\ No newline at end of file diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem index 2e07586c..4edb0066 100644 --- a/mips/mips_extras.lem +++ b/mips/mips_extras.lem @@ -90,7 +90,6 @@ let shift_bits_right_arith v n = maybe_fail "shift_bits_right_arith" r (* Use constants for undefined values for now *) -let internal_pick vs = return (head vs) let undefined_string () = return "" let undefined_unit () = return () let undefined_int () = return (0:ii) @@ -112,7 +111,12 @@ val elf_entry : unit -> integer let elf_entry () = 0 declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry` -let print_bits msg bs = prerr_endline (msg ^ (string_of_bv bs)) +let print_bits msg bs = print_endline (msg ^ (string_of_bv bs)) +let prerr_bits msg bs = prerr_endline (msg ^ (string_of_bv bs)) + +val prerr_string : string -> unit +let prerr_string _ = () +declare ocaml target_rep function prerr_string = `Pervasives.prerr_string` val get_time_ns : unit -> integer let get_time_ns () = 0 diff --git a/mips/mips_extras.v b/mips/mips_extras.v index b9dd6138..6a6aed5c 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -107,7 +107,7 @@ Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%st Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii). (*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*) -Definition undefined_vector {rv a e} len (u : a) : monad rv (list a) e := returnm (repeat u len). +Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >= 0)} : monad rv (vec a len) e := returnm (vec_init u len). (*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0). (*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) @@ -138,7 +138,25 @@ Definition eq_bit (x : bitU) (y : bitU) : bool := | _,_ => false end. +Require Import Zeuclid. +Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}. +refine (existT _ (ZEuclid.modulo m n) _). +constructor. +destruct H. +assert (Zabs n = n). { rewrite Zabs_eq; auto with zarith. } +rewrite <- H at 3. +lapply (ZEuclid.mod_always_pos m n); omega. +Qed. + (* Override the more general version *) Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r. Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r. + + +Definition print_endline (_:string) : unit := tt. +Definition prerr_endline (_:string) : unit := tt. +Definition prerr_string (_:string) : unit := tt. +Definition putchar {T} (_:T) : unit := tt. +Require DecimalString. +Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail index c678000e..63c380de 100644 --- a/mips/mips_insts.sail +++ b/mips/mips_insts.sail @@ -1005,19 +1005,7 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) = /* SYSCALL/BREAK/WAIT/Trap */ /**************************************************************************************/ -/* Co-opt syscall 0xfffff for use as thread start in pccmem */ -union clause ast = SYSCALL_THREAD_START : unit -function clause decode (0b000000 @ 0xfffff @ 0b001100) = - Some(SYSCALL_THREAD_START()) -function clause execute (SYSCALL_THREAD_START()) = () - - -/* fake stop fetching instruction for ppcmem, execute doesn't do anything, - decode never produces it */ - -union clause ast = ImplementationDefinedStopFetching : unit -function clause execute (ImplementationDefinedStopFetching()) = () - +/* $include mips_rmem.sail */ union clause ast = SYSCALL : unit function clause decode (0b000000 @ code : bits(20) @ 0b001100) = @@ -1136,10 +1124,9 @@ function clause execute (Load(width, sign, linked, base, rt, offset)) = CP0LLBit = 0b1; CP0LLAddr = pAddr; match width { - B => extendLoad(MEMr_reserve_wrapper(pAddr, 1), sign), - H => extendLoad(MEMr_reserve_wrapper(pAddr, 2), sign), W => extendLoad(MEMr_reserve_wrapper(pAddr, 4), sign), - D => extendLoad(MEMr_reserve_wrapper(pAddr, 8), sign) + D => extendLoad(MEMr_reserve_wrapper(pAddr, 8), sign), + _ => throw(Error_internal_error()) /* there is no llbc or llhc */ } } else @@ -1185,10 +1172,9 @@ function clause execute (Store(width, conditional, base, rt, offset)) = { success : bool = if (CP0LLBit[0]) then match width { - B => MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0]), - H => MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0]), W => MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0]), - D => MEMw_conditional_wrapper(pAddr, 8, rt_val) + D => MEMw_conditional_wrapper(pAddr, 8, rt_val), + _ => throw(Error_internal_error()) /* there is no sbc or shc */ } else false; wGPR(rt) = zero_extend(success) } @@ -1210,8 +1196,7 @@ function clause decode(0b100010 @ base : regno @ rt : regno @ offset : imm16) = Some(LWL(base, rt, offset)) function clause execute(LWL(base, rt, offset)) = { - /* XXX length check not quite right, but conservative */ - vAddr = addrWrapper(sign_extend(offset) + rGPR(base), LoadData, W); + vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, WL); let pAddr = (TLBTranslate(vAddr, LoadData)) in { mem_val = MEMr_wrapper (pAddr[63..2] @ 0b00, 4); /* read word of interest */ @@ -1231,8 +1216,7 @@ function clause decode(0b100110 @ base : regno @ rt : regno @ offset : imm16) = Some(LWR(base, rt, offset)) function clause execute(LWR(base, rt, offset)) = { - /* XXX length check not quite right, but conservative */ - vAddr = addrWrapper(sign_extend(offset) + rGPR(base), LoadData, W); + vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, WR); let pAddr = (TLBTranslate(vAddr, LoadData)) in { mem_val = MEMr_wrapper(pAddr[63..2] @ 0b00, 4); /* read word of interest */ @@ -1254,8 +1238,7 @@ function clause decode(0b101010 @ base : regno @ rt : regno @ offset : imm16) = Some(SWL(base, rt, offset)) function clause execute(SWL(base, rt, offset)) = { - /* XXX length check not quite right, but conservative */ - vAddr = addrWrapper(sign_extend(offset) + rGPR(base), StoreData, W); + vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, WL); let pAddr = TLBTranslate(vAddr, StoreData) in { reg_val = rGPR(rt); @@ -1274,8 +1257,7 @@ function clause decode(0b101110 @ base : regno @ rt : regno @ offset : imm16) = Some(SWR(base, rt, offset)) function clause execute(SWR(base, rt, offset)) = { - /* XXX length check not quite right, but conservative */ - vAddr = addrWrapper(sign_extend(offset) + rGPR(base), StoreData, W); + vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, WR); let pAddr = TLBTranslate(vAddr, StoreData) in { wordAddr = pAddr[63..2] @ 0b00; @@ -1296,8 +1278,7 @@ function clause decode(0b011010 @ base : regno @ rt : regno @ offset : imm16) = Some(LDL(base, rt, offset)) function clause execute(LDL(base, rt, offset)) = { - /* XXX length check not quite right, but conservative */ - vAddr = addrWrapper(sign_extend(offset) + rGPR(base), LoadData, D); + vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, DL); let pAddr = TLBTranslate(vAddr, LoadData) in { mem_val = MEMr_wrapper(pAddr[63..3] @ 0b000, 8); /* read double of interest */ @@ -1322,8 +1303,7 @@ function clause decode(0b011011 @ base : regno @ rt : regno @ offset : imm16) = Some(LDR(base, rt, offset)) function clause execute(LDR(base, rt, offset)) = { - /* XXX length check not quite right, but conservative */ - vAddr = addrWrapper(sign_extend(offset) + rGPR(base), LoadData, D); + vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, DR); let pAddr = TLBTranslate(vAddr, LoadData) in { mem_val = MEMr_wrapper(pAddr[63..3] @ 0b000, 8); /* read double of interest */ @@ -1348,8 +1328,7 @@ function clause decode(0b101100 @ base : regno @ rt : regno @ offset : imm16) = Some(SDL(base, rt, offset)) function clause execute(SDL(base, rt, offset)) = { - /* XXX length check not quite right, but conservative */ - vAddr = addrWrapper(sign_extend(offset) + rGPR(base), StoreData, D); + vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, DL); let pAddr = TLBTranslate(vAddr, StoreData) in { reg_val = rGPR(rt); @@ -1374,8 +1353,7 @@ function clause decode(0b101101 @ base : regno @ rt : regno @ offset : imm16) = Some(SDR(base, rt, offset)) function clause execute(SDR(base, rt, offset)) = { - /* XXX length check not quite right, but conservative */ - vAddr = addrWrapper(sign_extend(offset) + rGPR(base), StoreData, D); + vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, DR); let pAddr = TLBTranslate(vAddr, StoreData) in { reg_val = rGPR(rt); @@ -1402,7 +1380,7 @@ function clause decode (0b101111 @ base : regno @ op : regno @ imm : imm16) = function clause execute (CACHE(base, op, imm)) = checkCP0Access () /* pretty much a NOP because no caches */ -/* PREF - prefetching into (non-existent) caches */ +/* PREF - prefetching into (non-existent) caches union clause ast = PREF : (regno, regno, bits(16)) function clause decode (0b110011 @ base : regno @ op : regno @ imm : imm16) = @@ -1410,6 +1388,7 @@ function clause decode (0b110011 @ base : regno @ op : regno @ imm : imm16) = function clause execute (PREF(base, op, imm)) = () /* XXX NOP */ +*/ /* SYNC - Memory barrier */ union clause ast = SYNC : unit @@ -1465,7 +1444,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = { @ 0b000 /* DS dcache sets */ @ 0b000 /* DL dcache lines */ @ 0b000 /* DA dcache assoc. */ - @ bool_to_bits(have_cp2) /* C2 CP2 presence */ + @ bool_to_bits(have_cp2) /* C2 CP2 presence */ @ 0b0 /* MD MDMX implemented */ @ 0b0 /* PC performance counters */ @ 0b0 /* WR watch registers */ diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index c9bebabb..6babfd19 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -565,6 +565,7 @@ function compare (cmp, valA, valB) = LTU => valA <_u valB } enum WordType = { B, H, W, D} +enum WordTypeUnaligned = { WL, WR, DL, DR } val wordWidthBytes : WordType -> range(1, 8) function wordWidthBytes(w) = diff --git a/mips/mips_rmem.sail b/mips/mips_rmem.sail new file mode 100644 index 00000000..1bc47337 --- /dev/null +++ b/mips/mips_rmem.sail @@ -0,0 +1,15 @@ +/* These instructions are used for RMEM integration only */ + +/* Co-opt syscall 0xfffff for use as thread start in pccmem */ +union clause ast = SYSCALL_THREAD_START : unit +function clause decode (0b000000 @ 0xfffff @ 0b001100) = + Some(SYSCALL_THREAD_START()) +function clause execute (SYSCALL_THREAD_START()) = () + + +/* fake stop fetching instruction for ppcmem, execute doesn't do anything, + decode never produces it */ + +union clause ast = ImplementationDefinedStopFetching : unit +function clause execute (ImplementationDefinedStopFetching()) = () + diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail index 0cc098a5..43e759b9 100644 --- a/mips/mips_wrappers.sail +++ b/mips/mips_wrappers.sail @@ -60,6 +60,10 @@ val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) function addrWrapper(addr, accessType, width) = addr +val addrWrapperUnaligned : (bits(64), MemAccessType, WordTypeUnaligned) -> bits(64) +function addrWrapperUnaligned(addr, accessType, width) = + addr + $ifdef _MIPS_TLB_STUB val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape} $else diff --git a/mips/prelude.sail b/mips/prelude.sail index 407482d6..094f82e8 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -44,7 +44,7 @@ val cast cast_unit_vec : bit -> bits(1) function cast_unit_vec b = match b { bitzero => 0b0, - bitone => 0b1 + _ => 0b1 } val print = "print_endline" : string -> unit @@ -55,7 +55,7 @@ val "prerr_string" : string -> unit val putchar = {c:"sail_putchar", _:"putchar"} : int -> unit -val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string +val concat_str = {lem: "stringAppend", coq: "String.append", _: "concat_str"} : (string, string) -> string val string_of_int = "string_of_int" : int -> string /* Unused? @@ -104,7 +104,7 @@ overload operator / = {quotient_nat, quotient} val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", coq: "Z.quot", _ : "tdiv_int"} : (int, int) -> int val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", coq: "Z.rem", _ : "tmod_int"} : (int, int) -> int -val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) +val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) overload operator % = {modulus} @@ -116,19 +116,19 @@ val max_nat = {lem: "max", coq: "Z.max", _: "max_int"} : (nat, nat) -> nat val max_int = {lem: "max", coq: "Z.max", _: "max_int"} : (int, int) -> int -val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} +val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} -val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)} +val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom", c:"max_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)} overload min = {min_atom, min_nat, min_int} overload max = {max_atom, max_nat, max_int} val __WriteRAM = "write_ram" : forall 'n 'm. - (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv} + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} val __MIPS_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -function __MIPS_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) +function __MIPS_write (addr, width, data) = let _ = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) in () val __ReadRAM = "read_ram" : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} @@ -186,7 +186,7 @@ function bool_to_bits x = if x then 0b1 else 0b0 val cast bit_to_bool : bit -> bool function bit_to_bool b = match b { bitone => true, - bitzero => false + _ => false } val cast bits_to_bool : bits(1) -> bool |