Merge remote branch 'experiments' into experiments

22 files changed, 47 insertions, 11 deletions

diff --git a/mips/Makefile b/mips/Makefile
new file mode 100644
index 00000000..03d7ae15
--- /dev/null
+++ b/mips/Makefile
@@ -0,0 +1,23 @@
+SAIL:=../src/sail.native
+LEM:=../../lem/lem
+
+# SOURCES:=mips_prelude.sail mips_tlb.sail mips_wrappers.sail mips_insts.sail mips_ri.sail mips_epilogue.sail ../etc/regfp.sail mips_regfp.sail
+SOURCES:=mips_prelude.sail mips_tlb_stub.sail mips_wrappers.sail mips_insts.sail mips_epilogue.sail ../etc/regfp.sail mips_regfp.sail
+
+
+all: mips.lem mips.ml mips_embed.lem
+
+mips.lem: $(SOURCES)
+	$(SAIL) -lem_ast -o $(BUILD)/mips $(SOURCES)
+
+mips.ml: mips.lem ../src/lem_interp/interp_ast.lem
+	$(LEM) -ocaml -lib ../src/lem_interp/ $<
+
+
+mips_embed.lem: $(SOURCES)
+# also generates mips_embed_sequential.lem, mips_embed_types.lem, mips_toFromInterp.lem
+	$(SAIL) -lem -lem_lib Mips_extras_embed -o mips $(SOURCES)
+
+clean:
+	rm -f mips.lem mips.ml
+	rm -f mips_embed*.lem mips_toFromInterp.lem
diff --git a/mips/hgen/ast.hgen b/mips/gen/ast.hgen
index a251adff..a251adff 100644
--- a/mips/hgen/ast.hgen
+++ b/mips/gen/ast.hgen
diff --git a/mips/hgen/fold.hgen b/mips/gen/fold.hgen
index 05b9c808..05b9c808 100644
--- a/mips/hgen/fold.hgen
+++ b/mips/gen/fold.hgen
diff --git a/mips/hgen/herdtools_ast_to_shallow_ast.hgen b/mips/gen/herdtools_ast_to_shallow_ast.hgen
index 7b1a58d9..7b1a58d9 100644
--- a/mips/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/mips/gen/herdtools_ast_to_shallow_ast.hgen
diff --git a/mips/hgen/herdtools_types_to_shallow_types.hgen b/mips/gen/herdtools_types_to_shallow_types.hgen
index 5a0e3bfc..5a0e3bfc 100644
--- a/mips/hgen/herdtools_types_to_shallow_types.hgen
+++ b/mips/gen/herdtools_types_to_shallow_types.hgen
diff --git a/mips/hgen/lexer.hgen b/mips/gen/lexer.hgen
index c01b14cc..c01b14cc 100644
--- a/mips/hgen/lexer.hgen
+++ b/mips/gen/lexer.hgen
diff --git a/mips/hgen/map.hgen b/mips/gen/map.hgen
index f5116bae..f5116bae 100644
--- a/mips/hgen/map.hgen
+++ b/mips/gen/map.hgen
diff --git a/mips/hgen/parser.hgen b/mips/gen/parser.hgen
index 8f573aa5..8f573aa5 100644
--- a/mips/hgen/parser.hgen
+++ b/mips/gen/parser.hgen
diff --git a/mips/hgen/pretty.hgen b/mips/gen/pretty.hgen
index 98f56f2e..98f56f2e 100644
--- a/mips/hgen/pretty.hgen
+++ b/mips/gen/pretty.hgen
diff --git a/mips/hgen/sail_trans_out.hgen b/mips/gen/sail_trans_out.hgen
index f2d006e8..f2d006e8 100644
--- a/mips/hgen/sail_trans_out.hgen
+++ b/mips/gen/sail_trans_out.hgen
diff --git a/mips/hgen/shallow_ast_to_herdtools_ast.hgen b/mips/gen/shallow_ast_to_herdtools_ast.hgen
index efe2c77e..efe2c77e 100644
--- a/mips/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/mips/gen/shallow_ast_to_herdtools_ast.hgen
diff --git a/mips/hgen/shallow_types_to_herdtools_types.hgen b/mips/gen/shallow_types_to_herdtools_types.hgen
index a02d83b7..a02d83b7 100644
--- a/mips/hgen/shallow_types_to_herdtools_types.hgen
+++ b/mips/gen/shallow_types_to_herdtools_types.hgen
diff --git a/mips/hgen/token_types.hgen b/mips/gen/token_types.hgen
index 170b42d3..170b42d3 100644
--- a/mips/hgen/token_types.hgen
+++ b/mips/gen/token_types.hgen
diff --git a/mips/hgen/tokens.hgen b/mips/gen/tokens.hgen
index 937c6354..937c6354 100644
--- a/mips/hgen/tokens.hgen
+++ b/mips/gen/tokens.hgen
diff --git a/mips/hgen/trans_sail.hgen b/mips/gen/trans_sail.hgen
index e42d1b19..e42d1b19 100644
--- a/mips/hgen/trans_sail.hgen
+++ b/mips/gen/trans_sail.hgen
diff --git a/mips/hgen/types.hgen b/mips/gen/types.hgen
index a1c61f4b..a1c61f4b 100644
--- a/mips/hgen/types.hgen
+++ b/mips/gen/types.hgen
diff --git a/mips/hgen/types_sail_trans_out.hgen b/mips/gen/types_sail_trans_out.hgen
index ebd31fcb..ebd31fcb 100644
--- a/mips/hgen/types_sail_trans_out.hgen
+++ b/mips/gen/types_sail_trans_out.hgen
diff --git a/mips/hgen/types_trans_sail.hgen b/mips/gen/types_trans_sail.hgen
index 63880ae9..63880ae9 100644
--- a/mips/hgen/types_trans_sail.hgen
+++ b/mips/gen/types_trans_sail.hgen
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 1fbba038..be576fb2 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -31,25 +31,25 @@ let memory_parameter_transformer_option_address _mode v =
   end
 
 
-let read_memory_functions : memory_reads =
+let mips_read_memory_functions : memory_reads =
   [ ("MEMr",             (MR Read_plain              memory_parameter_transformer));
     ("MEMr_reserve",     (MR Read_reserve            memory_parameter_transformer));
   ]
 
-let read_memory_tagged_functions : memory_read_taggeds =
+let mips_read_memory_tagged_functions : memory_read_taggeds =
   [ ("MEMr_tag",         (MRT Read_plain             memory_parameter_transformer));
     ("MEMr_tag_reserve", (MRT Read_reserve           memory_parameter_transformer));
   ]
 
-let memory_writes : memory_writes =
+let mips_memory_writes : memory_writes =
   []
 
-let memory_eas : memory_write_eas =
+let mips_memory_eas : memory_write_eas =
   [ ("MEMea",                 (MEA Write_plain           memory_parameter_transformer));
     ("MEMea_conditional",     (MEA Write_conditional     memory_parameter_transformer));
   ]
 
-let memory_vals : memory_write_vals =
+let mips_memory_vals : memory_write_vals =
   [ ("MEMval",      (MV memory_parameter_transformer_option_address Nothing));
     ("MEMval_conditional", (MV memory_parameter_transformer_option_address
                            (Just 
@@ -58,7 +58,7 @@ let memory_vals : memory_write_vals =
                              (IState (Interp.add_answer_to_stack interp bit) context)))));
   ]
 
-let memory_vals_tagged : memory_write_vals_tagged =
+let mips_memory_vals_tagged : memory_write_vals_tagged =
   [
     ("MEMval_tag",      (MVT memory_parameter_transformer_option_address Nothing));
     ("MEMval_tag_conditional", (MVT memory_parameter_transformer_option_address
@@ -68,6 +68,6 @@ let memory_vals_tagged : memory_write_vals_tagged =
                              (IState (Interp.add_answer_to_stack interp bit) context)))));
   ]
 
-let barrier_functions = [
+let mips_barrier_functions = [
   ("MEM_sync", Barrier_MIPS_SYNC);
   ]
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index a4098486..382e4d7f 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -472,6 +472,13 @@ function AccessLevel getAccessLevel() =
       case _    -> User (* behaviour undefined, assume user *)
     }
 
+function ([|2|]) int_of_accessLevel((AccessLevel)x) = 
+       switch (x) {
+         case User -> 0
+         case Supervisor -> 1
+         case Kernel -> 2
+       }
+
 function unit checkCP0Access () =
   {
     let accessLevel = getAccessLevel() in
diff --git a/mips/mips_tlb.sail b/mips/mips_tlb.sail
index 2e40deed..d72e0e75 100644
--- a/mips/mips_tlb.sail
+++ b/mips/mips_tlb.sail
@@ -108,7 +108,7 @@ function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessT
       case 0b01 -> (Supervisor, None)                       (* xsseg - supervisor mapped *)
       case 0b00 -> (User, None) (* xuseg - user mapped *)
     } in
-    if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
+    if ((int_of_accessLevel(currentAccessLevel)) < (int_of_accessLevel(requiredLevel))) then
       (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
     else 
       let (pa, c) = switch(addr) {
diff --git a/mips/run_embed.ml b/mips/run_embed.ml
index 463caffd..1bb6d5f6 100644
--- a/mips/run_embed.ml
+++ b/mips/run_embed.ml
@@ -219,7 +219,10 @@ module CHERI_model : ISA_model = struct
        let pc_vaddr = unsigned_big(Cheri_embed._PC) in
        let npc_addr = add_int_big_int 4 pc_vaddr in
        let npc_vec = to_vec_dec_big (bi64, npc_addr) in
-       set_register Cheri_embed._nextPC npc_vec
+       begin
+         set_register Cheri_embed._nextPC npc_vec;
+         set_register Cheri_embed._inCCallDelay (to_vec_dec_int (1, 0))
+       end
 
   let get_pc () = unsigned_big (Cheri_embed._PC)
 
@@ -250,7 +253,7 @@ module CHERI128_model : ISA_model = struct
     let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in
     set_register Cheri128_embed._nextPC start_addr;
     set_register_field_bit Cheri128_embed._CP0Status "BEV" Vone;
-    let initial_cap_val_int = big_int_of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *)
+    let initial_cap_val_int = big_int_of_string "0x1fffe6000000100000000000000000000" in (* hex((0x10000 << 64) + (48 << 105) + (0x7fff << 113) + (1 << 128)) T=0x10000 E=48 perms=0x7fff tag=1 *)
     let initial_cap_vec = to_vec_dec ((bi129), initial_cap_val_int) in 
     set_register Cheri128_embed._PCC initial_cap_vec;
     set_register Cheri128_embed._nextPCC initial_cap_vec;
@@ -277,7 +280,10 @@ module CHERI128_model : ISA_model = struct
        let pc_vaddr = unsigned_big(Cheri128_embed._PC) in
        let npc_addr = add_int_big_int 4 pc_vaddr in
        let npc_vec = to_vec_dec_big (bi64, npc_addr) in
-       set_register Cheri128_embed._nextPC npc_vec
+       begin
+         set_register Cheri128_embed._nextPC npc_vec;
+         set_register Cheri128_embed._inCCallDelay (to_vec_dec_int (1, 0))
+       end
 
   let get_pc () = unsigned_big (Cheri128_embed._PC)