diff options
| author | Robert Norton | 2016-04-13 15:28:05 +0100 |
|---|---|---|
| committer | Robert Norton | 2016-04-13 15:49:21 +0100 |
| commit | b5b74f9fca5a760cb388b1f9ed7873f73b983c45 (patch) | |
| tree | c29024b25db43840f4dffc880ead2cc37416e016 /mips | |
| parent | 8753f631a14c5203ff7ec1ad495b89b8034c011b (diff) | |
add tagr and tagw in mips_extras (will need to change these to make tag writes atomic)
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_extras.lem | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem index d1eacc1c..4cf58ff5 100644 --- a/mips/mips_extras.lem +++ b/mips/mips_extras.lem @@ -43,7 +43,9 @@ let read_memory_functions : memory_reads = (v,(natFromInteger len), Just (loc_regs++ (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))) - end end end))); + end end end))); + ("TAGr", (MR Read_tag (fun mode v -> let (v, regs) = extern_mem_value mode v in + (v, 1, regs)))); ] let memory_writes : memory_writes = [ ("MEMw", (MW Write_plain @@ -85,6 +87,12 @@ let memory_writes : memory_writes = [ let v = Interp.V_lit (L_aux (if success then L_one else L_zero) Unknown) in IState (Interp.add_answer_to_stack interp_state v) c)) )); + ("TAGw", (MW Write_tag (fun mode v -> let (v, regs) = extern_mem_value mode v in + (v, 1, regs)) + (Just (fun (IState interp_state c) success -> + let v = Interp.V_lit (L_aux (if success then L_one else L_zero) Unknown) in + IState (Interp.add_answer_to_stack interp_state v) c)) + )); ] let barrier_functions = [ |