Merge remote branch 'experiments' into experiments

1 files changed, 110 insertions, 169 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 68f82ccb..563da2e5 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -9,6 +9,14 @@
 (*    Robert Norton-Wright                                                *)
 (*    Christopher Pulte                                                   *)
 (*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
 (*                                                                        *)
 (*  All rights reserved.                                                  *)
 (*                                                                        *)
@@ -440,7 +448,8 @@ let rec interp_to_value_helper debug arg ivh_mode err_str instr direction regist
       (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out)
-    | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
+    | (outcome, _, _) ->
+       (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str ^ " " ^ Interp.string_of_outcome outcome)), events_out)
 end
 
 let call_external_functions direction outcome = 
@@ -470,7 +479,7 @@ let translate_address top_level end_flag thunk_name registers address =
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (address_error,events) =
-    interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction
+    interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str (V_list []) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -505,17 +514,16 @@ let intern_instruction direction (name,parms) =
   Interp_ast.V_ctor (Interp.id_of_string name) (mk_typ_id "ast") Interp_ast.C_Union
     (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms))
 
-let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
+let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers (instruction : Interp_ast.value) =
   let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in
   let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in
   let mode = make_mode true false debug in
   let int_mode = mode.internal_mode in
-  let intern_val = intern_instruction direction instruction in
-  let val_str = Interp.string_of_value intern_val in
-  let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
+  let val_str = Interp.string_of_value instruction in
+  let (arg,_) = Interp.to_exp int_mode Interp.eenv instruction in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (analysis_or_error,events) =
-    interp_to_value_helper debug Nothing Ivh_analysis val_str ("",[]) internal_direction
+    interp_to_value_helper debug Nothing Ivh_analysis val_str (V_list []) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -573,6 +581,33 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
          | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
             NIA_register (reg_to_reg_name reg)
          | _ -> failwith "Register footprint analysis did not return nia of expected type" end in
+       let readk_to_readk = function
+                         | "Read_plain" ->             Read_plain
+                         | "Read_reserve" ->           Read_reserve
+                         | "Read_acquire" ->           Read_acquire
+                         | "Read_exclusive" ->         Read_exclusive
+                         | "Read_exclusive_acquire" -> Read_exclusive_acquire
+                         | "Read_stream" ->            Read_stream 
+                         | "Read_RISCV_acquire"                  -> Read_RISCV_acquire
+                         | "Read_RISCV_strong_acquire"           -> Read_RISCV_strong_acquire
+                         | "Read_RISCV_reserved"                 -> Read_RISCV_reserved
+                         | "Read_RISCV_reserved_acquire"         -> Read_RISCV_reserved_acquire
+                         | "Read_RISCV_reserved_strong_acquire"  -> Read_RISCV_reserved_strong_acquire
+                         | "Read_X86_locked"                     -> Read_X86_locked
+                         | r -> failwith ("unknown read kind: " ^ r) end in
+       let writek_to_writek = function
+                         | "Write_plain" ->             Write_plain
+                         | "Write_conditional" ->       Write_conditional
+                         | "Write_release" ->           Write_release
+                         | "Write_exclusive" ->         Write_exclusive
+                         | "Write_exclusive_release" -> Write_exclusive_release 
+                         | "Write_RISCV_release"                    -> Write_RISCV_release
+                         | "Write_RISCV_strong_release"             -> Write_RISCV_strong_release
+                         | "Write_RISCV_conditional"                -> Write_RISCV_conditional
+                         | "Write_RISCV_conditional_release"        -> Write_RISCV_conditional_release
+                         | "Write_RISCV_conditional_strong_release" -> Write_RISCV_conditional_strong_release
+                         | "Write_X86_locked"                       -> Write_X86_locked
+                         | w -> failwith ("unknown write kind: " ^ w) end in
        let ik_to_ik = function
          | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _
            (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) ->
@@ -588,27 +623,19 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
                         | "Barrier_DSB_ST" -> Barrier_DSB_ST
                         | "Barrier_DSB_LD" -> Barrier_DSB_LD
                         | "Barrier_ISB" ->    Barrier_ISB
-                        | "Barrier_MIPS_SYNC" ->    Barrier_MIPS_SYNC
+                        | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC
+                        | "Barrier_x86_MFENCE" -> Barrier_x86_MFENCE
                         end)
          | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _
            (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) ->
-            IK_mem_read (match r with
-                         | "Read_plain" ->             Read_plain
-                         | "Read_reserve" ->           Read_reserve
-                         | "Read_acquire" ->           Read_acquire
-                         | "Read_exclusive" ->         Read_exclusive
-                         | "Read_exclusive_acquire" -> Read_exclusive_acquire
-                         | "Read_stream" ->            Read_stream
-                         end)
+            IK_mem_read(readk_to_readk r)
          | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _
            (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) ->
-            IK_mem_write (match w with
-                         | "Write_plain" ->             Write_plain
-                         | "Write_conditional" ->       Write_conditional
-                         | "Write_release" ->           Write_release
-                         | "Write_exclusive" ->         Write_exclusive
-                         | "Write_exclusive_release" -> Write_exclusive_release
-                          end)
+            IK_mem_write(writek_to_writek w)
+         | Interp_ast.V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _
+           (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ;
+                                (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) ->
+            IK_mem_rmw(readk_to_readk readk, writek_to_writek writek)
          | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ ->
             IK_cond_branch
          | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
@@ -680,7 +707,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (instr_decoded_error,events) =
-    interp_to_value_helper debug (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false
+    interp_to_value_helper debug (Just value) Ivh_decode val_str (V_list []) internal_direction registers [] false
       (fun _ -> Interp.resume 
           mode 
           (Interp.Thunk_frame 
@@ -688,9 +715,9 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
              top_env Interp.eenv (Interp.emem "decode top level") Interp.Top) Nothing) in
   match (instr_decoded_error) with
     | Ivh_value instr -> 
-      let instr_external = interp_value_to_instr_external top_level instr in
+       (* let instr_external = interp_value_to_instr_external top_level instr in*) 
       let (instr_decoded_error,events) =
-        interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr_external internal_direction
+        interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr (*instr_external*) internal_direction
           registers [] false
         (fun _ -> Interp.resume 
             mode
@@ -699,7 +726,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
                   (Interp_ast.Unknown, Nothing)) 
                top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in
       match (instr_decoded_error) with
-        | Ivh_value _ -> IDE_instr instr_external instr
+      | Ivh_value _ -> IDE_instr instr (*instr_external*)
         | Ivh_value_after_exn v ->
           Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now"
         | Ivh_error err -> IDE_decode_error err
@@ -713,9 +740,9 @@ end
 let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = 
   let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in
   match decode_to_instruction top_level registers value with
-  | IDE_instr instr instrv ->
+  | IDE_instr instr ->
      let mode = make_interpreter_mode true false in
-     let (arg,_) = Interp.to_exp mode Interp.eenv instrv in
+     let (arg,_) = Interp.to_exp mode Interp.eenv instr in
      Instr instr
            (IState (Interp.Thunk_frame
                       (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
@@ -750,11 +777,11 @@ let instr_external_to_interp_value top_level instr =
   Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) 
                 (mk_typ_id "ast") Interp_ast.C_Union parmsV
 
-val instruction_to_istate : context -> instruction -> instruction_state 
-let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state  = 
+val instruction_to_istate : context -> Interp_ast.value -> instruction_state 
+let instruction_to_istate (top_level:context) (instr:Interp_ast.value) : instruction_state  = 
   let mode = make_interpreter_mode true false in
   let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in
-  let ast_node = fst (Interp.to_exp mode Interp.eenv (instr_external_to_interp_value top_level instr)) in
+  let ast_node = fst (Interp.to_exp mode Interp.eenv instr) in
   (IState
      (Interp.Thunk_frame
         (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [ast_node])
@@ -1092,7 +1119,7 @@ and state_to_outcome_s pp_instruction_state mode state =
          (fun env -> interp_exhaustive mode.internal_mode.Interp.debug (Just env) state))
   )
 
-val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
+val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> Interp_ast.value -> Sail_impl_base.outcome_s unit
 let initial_outcome_s_of_instruction pp_instruction_state context mode instruction =
   let state = instruction_to_istate context instruction in
   state_to_outcome_s pp_instruction_state mode state
@@ -1222,136 +1249,13 @@ let nia_address_of_event nia_reg (event: event) : maybe (maybe address) =
   | _ -> Nothing
   end
 
-let nias_of_instruction 
-      thread_ism
-    (nia_address: list (maybe address)) (* Nothing for unknown/undef*)
-    (regs_in:     list reg_name)
-    (instruction: instruction)
-    : list nia
-  =
-  let (instruction_name, instruction_fields) = instruction in
-
-  let unknown_nia_address = List.elem Nothing nia_address in
-
-  let nias = [NIA_concrete_address addr | forall (addr MEM (List.mapMaybe id nia_address)) | true] in
-
-  (* it's a fact of the Power2.06B instruction pseudocode that in the B and Bc
-     cases there should be no Unknown values in nia_values, while in the Bclr
-     and Bcctr cases nia_values will just be Unknown and the semantics should
-     match the comments in the machineDefTypes definition of nia *)
-  (* All our other analysis is on the pseudocode directly, which is arguably
-     pleasingly robust.  We could replace the nias pattern match on
-     instruction_name with something in that style if the exhaustive interpreter
-     announced register dependencies to register writes (easy) and if it could
-     check the form of the register writes to LR and CTR matches the
-     machineDefTypes nia definition *)
-  match (thread_ism, instruction_name) with
-    | ("PPCGEN_ism", "B") ->
-       let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values 1" in
-       nias
-    | ("PPCGEN_ism", "Bc") ->
-       let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values 2" in
-       NIA_successor :: nias
-    | ("PPCGEN_ism", "Bclr") -> [ NIA_successor; NIA_LR ]
-    | ("PPCGEN_ism", "Bcctr") -> [ NIA_successor; NIA_CTR ]
-    | ("PPCGEN_ism", "Sc") ->
-       let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values 3" in
-       match instruction_fields with
-       | [(_, _, lev)] ->
-          (* LEV field is 7 bits long, pad it with false at beginning *)
-          if lev = [Bitc_zero;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one]
-                     (* (Interp_inter_imp.integer_of_byte_list (Interp_inter_imp.to_bytes (false :: bl))) = 63 *)
-          then []
-          else [NIA_successor]
-       | _ -> [ NIA_successor ]
-       end
-
-    (* AARch64 label branch (i.e. address must be known) although
-    these instructions take the address as an offset from PC, in here
-    we see the absolute address as it was extracted from the micro ops
-    just before write to PC *)
-    | ("AArch64HandSail", "BranchImmediate")   -> nias
-    | ("AArch64HandSail", "BranchConditional") -> NIA_successor :: nias
-    | ("AArch64HandSail", "CompareAndBranch")  -> NIA_successor :: nias
-    | ("AArch64HandSail", "TestBitAndBranch")  -> NIA_successor :: nias
-
-    (* AArch64 calculated address branch *)
-    | ("AArch64HandSail", "BranchRegister") ->
-        (* do some parsing of the ast fields to figure out which register holds
-           the branching address i.e. find n in "BR <Xn>". The ast constructor
-           from armV8.sail: (reg_index,BranchType) BranchRegister; *)
-        let n_integer =
-          match instruction_fields with
-          | [(_, _, n); _] -> integer_of_bit_list n
-          | _ -> fail
-          end
-        in
-        let () = ensure (0 <= n_integer && n_integer <= 31)
-                  "expected register number from 0 to 31"
-        in
-        if n_integer = 31 then
-          nias (* BR XZR *)
-        else
-          (* look for Xn (which we actually call Rn) in regs_in *)
-          let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in
-          [NIA_register r | forall (r MEM regs_in)
-                          | match r with
-                            | (Reg name _ _ _) -> name = n_reg
-                            | _ -> false
-                            end]
-
-
-    (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *)
-
-    | ("AArch64GenSail", "BranchImmediate")   -> nias
-    | ("AArch64GenSail", "BranchConditional") -> NIA_successor :: nias
-    | ("AArch64GenSail", "CompareAndBranch")  -> NIA_successor :: nias
-    | ("AArch64GenSail", "TestBitAndBranch")  -> NIA_successor :: nias
-
-    (* AArch64 calculated address branch *)
-    | ("AArch64GenSail", "branch_unconditional_register") ->
-        (* do some parsing of the ast fields to figure out which register holds
-           the branching address i.e. find n in "BR <Xn>". The ast constructor
-           from armV8.sail: (reg_index,BranchType) BranchRegister; *)
-        let n_integer =
-          match instruction_fields with
-          | [(_, _, n); _] -> integer_of_bit_list n
-          | _ -> fail
-          end
-        in
-        let () = ensure (0 <= n_integer && n_integer <= 31)
-                  "expected register number from 0 to 31"
-        in
-        if n_integer = 31 then
-          nias (* BR XZR *)
-        else
-          (* look for Xn (which we actually call Rn) in regs_in *)
-          let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in
-          [NIA_register r | forall (r MEM regs_in)
-                          | match r with
-                            | (Reg name _ _ _) -> name = n_reg
-                            | _ -> false
-                            end]
-
-    (** end of hacky *)
-
-    | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias
-
-
-    | ("MIPS_ism", "B") -> fail
-
-    | (s1,s2) ->
-       let () = ensure (not unknown_nia_address)
-                       ("unexpected unknown/undefined address in nia_values 4 (\""^s1^"\", \""^s2^"\")") in
-        [ NIA_successor ]
-    end
-
 let interp_instruction_analysis 
+      top_level
       (interp_exhaustive : ((list (reg_name * register_value)) -> list event))
-      instruction nia_reg ism environment = 
+      instruction 
+      nia_reg 
+      (nias_function : (list (maybe address) -> list reg_name -> list nia))
+      ism environment = 
     
     let es = interp_exhaustive environment in
 
@@ -1362,7 +1266,7 @@ let interp_instruction_analysis
 
     let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in
 
-    let nias = nias_of_instruction ism nia_address regs_in instruction in
+    let nias = nias_function nia_address regs_in in
 
     let dia = DIA_none in (* FIX THIS! *)
 
@@ -1376,6 +1280,41 @@ let interp_instruction_analysis
 
           if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
             inst_kind
+
+          else if
+            (forall (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_read _  -> true
+                | IK_mem_write _ -> true
+                | IK_mem_rmw _   -> false
+                | IK_barrier _   -> false
+                | IK_cond_branch -> false
+                | IK_trans _     -> false
+                | IK_simple      -> false
+                end) &&
+            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_read _  -> true
+                | _              -> false
+                end) &&
+            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_write _ -> true
+                | _              -> false
+                end)
+          then
+            match
+              List.partition
+                (function IK_mem_read _ -> true | _ -> false end)
+                (inst_kind :: inst_kinds)
+            with
+            | ((IK_mem_read r) :: rs, (IK_mem_write w) :: ws) ->
+                let () = ensure (forall (r' MEM rs). r' = IK_mem_read r) "more than one kind of read" in
+                let () = ensure (forall (w' MEM ws). w' = IK_mem_write w) "more than one kind of write" in
+                IK_mem_rmw (r, w)
+            | _ -> fail
+            end
+
           (* the TSTART instruction can also be aborted so it will have two kinds of events *)
           else if (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
                         inst_kind' = IK_trans Transaction_start) &&
@@ -1384,7 +1323,9 @@ let interp_instruction_analysis
                         || inst_kind' = IK_trans Transaction_abort)
           then
             IK_trans Transaction_start
-          else failwith "multiple instruction kinds"
+
+          else
+            failwith "multiple instruction kinds"
     end in
 
   (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind)
@@ -1400,29 +1341,29 @@ val print_and_fail_of_inequal : forall 'a. Show 'a =>
                                 (instruction -> string) ->
                                 (string * 'a) -> (string * 'a) -> unit
 let print_and_fail_if_inequal 
-      (print_endline,pp_instruction,instruction)
+      (print_endline,instruction)
       (name1,xs1) (name2,xs2) =
   if xs1 = xs2 then ()
   else 
     let () = print_endline (name1^": "^show xs1) in
     let () = print_endline (name2^": "^show xs2) in
-    failwith (name1^" and "^ name2^" inequal for instruction " ^ pp_instruction instruction)
+    failwith (name1^" and "^ name2^" inequal for instruction: \n" ^ Interp.string_of_value instruction)
 
 let interp_compare_analyses 
       print_endline
-      pp_instruction
       (non_pseudo_registers : set reg_name -> set reg_name)
       context
       endianness
       interp_exhaustive
-      instruction
+      (instruction : Interp_ast.value)
       nia_reg
+      (nias_function : (list (maybe address) -> list reg_name -> list nia))
       ism
       environment
       analysis_function
       reg_info = 
   let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = 
-    interp_instruction_analysis interp_exhaustive instruction nia_reg ism 
+    interp_instruction_analysis context interp_exhaustive instruction nia_reg nias_function ism 
                                 environment in
   let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) =
     (Set.fromList regs_in1,
@@ -1447,7 +1388,7 @@ let interp_compare_analyses
      non_pseudo_registers regs_out2S,
      non_pseudo_registers regs_feeding_address2S) in
 
-  let aux = (print_endline,pp_instruction,instruction) in
+  let aux = (print_endline,instruction) in
   let () = (print_and_fail_if_inequal aux)
              ("regs_in exhaustive",regs_in1S) 
              ("regs_in hand",regs_in2S) in