diff options
| author | Shaked Flur | 2017-08-19 10:34:04 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-08-19 10:34:04 +0100 |
| commit | 9a26a0440f4d3c63ea19976c44cd39edb8149b2a (patch) | |
| tree | c3e94a92f5be5cf07663beed773b72b4a60597b6 /risc-v/riscv_extras.lem | |
| parent | d5fe6885da9758a8924929547e40dd72e7333428 (diff) | |
RISC-V store-release
Diffstat (limited to 'risc-v/riscv_extras.lem')
| -rw-r--r-- | risc-v/riscv_extras.lem | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem index 80f8bcc9..3803839d 100644 --- a/risc-v/riscv_extras.lem +++ b/risc-v/riscv_extras.lem @@ -42,15 +42,25 @@ let memory_writes : memory_writes = [] let memory_eas : memory_write_eas = - [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); - ("MEMea_conditional", (MEA Write_conditional memory_parameter_transformer)); + [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); + ("MEMea_release", (MEA Write_RISCV_release memory_parameter_transformer)); + ("MEMea_conditional", (MEA Write_RISCV_conditional memory_parameter_transformer)); + ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer)); ] let memory_vals : memory_write_vals = - [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional", (MV memory_parameter_transformer_option_address - (Just - (fun (IState interp context) b -> + [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional", + (MV memory_parameter_transformer_option_address + (Just + (fun (IState interp context) b -> + let bit = 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 bit) context))))); + ("MEMval_conditional_release", + (MV memory_parameter_transformer_option_address + (Just + (fun (IState interp context) b -> let bit = 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 bit) context))))); ] |