diff options
| author | Shaked Flur | 2017-11-30 15:40:43 +0000 |
|---|---|---|
| committer | Shaked Flur | 2017-11-30 15:40:43 +0000 |
| commit | 9e1309ab7c1a137324c88c272c5a76c4c8bce016 (patch) | |
| tree | 854889fe87e8f443d4e0aafa26b970a88faf61bb /risc-v | |
| parent | 16c269d6f26fd69d8788c448b87f4bb479a6ef66 (diff) | |
match what rmem (ppcmem2) expects from ISA Makefiles
Diffstat (limited to 'risc-v')
| -rw-r--r-- | risc-v/Makefile | 24 | ||||
| -rw-r--r-- | risc-v/riscv_extras.lem | 12 |
2 files changed, 22 insertions, 14 deletions
diff --git a/risc-v/Makefile b/risc-v/Makefile index 8449c7c4..bc46e4c2 100644 --- a/risc-v/Makefile +++ b/risc-v/Makefile @@ -1,14 +1,22 @@ - SAIL:=../src/sail.native +LEM:=../../lem/lem + SOURCES:=riscv_types.sail riscv.sail ../etc/regfp.sail riscv_regfp.sail -all: lem_ast shallow -lem_ast: $(SOURCES) $(SAIL) - $(SAIL) -lem_ast $(SOURCES) -o riscv -shallow: $(SOURCES) $(SAIL) - $(SAIL) -lem_lib Riscv_extras_embed -lem $(SOURCES) -o riscv +all: riscv.lem riscv.ml riscv_embed.lem + +riscv.lem: $(SOURCES) + $(SAIL) -lem_ast -o riscv $(SOURCES) + +riscv.ml: riscv.lem ../src/lem_interp/interp_ast.lem + $(LEM) -ocaml -lib ../src/lem_interp/ $< + + +riscv_embed.lem: $(SOURCES) +# also generates riscv_embed_sequential.lem, riscv_embed_types.lem, riscv_toFromInterp.lem + $(SAIL) -lem -lem_lib Riscv_extras_embed -o riscv $(SOURCES) clean: - rm -f riscv.lem riscv_embed*.lem riscv_toFromInterp.lem - rm -f riscv_type*.lem + rm -f riscv.lem riscv.ml + rm -f riscv_embed*.lem riscv_toFromInterp.lem diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem index 30043779..4ca5f9b7 100644 --- a/risc-v/riscv_extras.lem +++ b/risc-v/riscv_extras.lem @@ -31,7 +31,7 @@ let memory_parameter_transformer_option_address _mode v = end -let read_memory_functions : memory_reads = +let riscv_read_memory_functions : memory_reads = [ ("MEMr", (MR Read_plain memory_parameter_transformer)); ("MEMr_acquire", (MR Read_RISCV_acquire memory_parameter_transformer)); ("MEMr_strong_acquire", (MR Read_RISCV_strong_acquire memory_parameter_transformer)); @@ -41,10 +41,10 @@ let read_memory_functions : memory_reads = (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); ] -let memory_writes : memory_writes = +let riscv_memory_writes : memory_writes = [] -let memory_eas : memory_write_eas = +let riscv_memory_eas : memory_write_eas = [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); ("MEMea_release", (MEA Write_RISCV_release memory_parameter_transformer)); ("MEMea_strong_release", (MEA Write_RISCV_strong_release memory_parameter_transformer)); @@ -55,7 +55,7 @@ let memory_eas : memory_write_eas = memory_parameter_transformer)); ] -let memory_vals : memory_write_vals = +let riscv_memory_vals : memory_write_vals = [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); ("MEMval_strong_release", (MV memory_parameter_transformer_option_address Nothing)); @@ -66,14 +66,14 @@ let memory_vals : memory_write_vals = ] -let speculate_conditional_success : excl_res = +let riscv_speculate_conditional_success : excl_res = let f = fun (IState interp context) b -> let bool_res = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in IState (Interp.add_answer_to_stack interp bool_res) context in Just ("speculate_conditional_success", (ER (Just f))) -let barrier_functions = +let riscv_barrier_functions = [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw); ("MEM_fence_r_rw", Barrier_RISCV_r_rw); ("MEM_fence_r_r", Barrier_RISCV_r_r); |