aspec/haskell: clean out resolved FIXMEs

spec/abstract/ARM/Init_A.thy

@@ -34,7 +34,7 @@ definition
   init_irq_node_ptr :: word32 where
   "init_irq_node_ptr = kernel_base + 0x8000"
 
-(* FIXME: It is easy to remove a memory slot here, but once if we want to reserve other slots of memory, we have to do the proof of disjoint for example state again.
+(* It is easy to remove a memory slot here, but once if we want to reserve other slots of memory, we have to do the proof of disjoint for example state again.
    Comment is left here so that next time we need 4k memory, we don't need to fix example state and can simply change its name. *)
 definition
   init_globals_frame :: word32 where
@@ -80,7 +80,7 @@ definition
     tcb_mcpriority = minBound,
     tcb_arch = init_arch_tcb
   \<rparr>,
-  init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), (* FIXME: same reason as why we kept the definition of init_globals_frame *)
+  init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), (* same reason as why we kept the definition of init_globals_frame *)
   init_global_pd \<mapsto> ArchObj (PageDirectory global_pd)
   )"
 

spec/abstract/ARM_HYP/ArchInvocation_A.thy

@@ -86,7 +86,6 @@ datatype page_invocation
 
 datatype vcpu_invocation =
        VCPUSetTCB obj_ref (*vcpu*) obj_ref (*tcb*)
-       (*FIXME ARMHYP: canonise canonical types for VCPUInjectIRQ *)
      | VCPUInjectIRQ obj_ref nat virq
      | VCPUReadRegister obj_ref vcpureg
      | VCPUWriteRegister obj_ref vcpureg machine_word

spec/abstract/ARM_HYP/Machine_A.thy

@@ -159,9 +159,8 @@ definition
 
 datatype arch_fault =
     VMFault vspace_ref "machine_word list"
-  (* FIXME ARMHYP are these truly arch-independant, or just in the current C version *)
+  | VGICMaintenance "data option" (* idx *)
-  | VGICMaintenance "data option" (* idx *) (* idxValid? second arguments? *)
+  | VCPUFault data (* hsr *)
-  | VCPUFault data (* hsr *) (* FIXME ARMHYP: this is a 64-bit struct, 2x data? *)
 
 
 end

spec/abstract/ARM_HYP/VCPU_A.thy

@@ -39,7 +39,7 @@ subsection "VCPU: Set TCB"
 definition decode_vcpu_set_tcb :: "arch_cap \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (arch_invocation,'z::state_ext) se_monad"
 where "decode_vcpu_set_tcb cap extras \<equiv> case (cap, extras) of
   (VCPUCap v, fs#_) \<Rightarrow> (case fs of
-        (ThreadCap t, _) \<Rightarrow> returnOk $ InvokeVCPU $ VCPUSetTCB v t (* FIXME ARMHYP C code calls deriveCap here before checking the cap type, discuss with kernel team *)
+        (ThreadCap t, _) \<Rightarrow> returnOk $ InvokeVCPU $ VCPUSetTCB v t
       | _ \<Rightarrow> throwError IllegalOperation)
  |(VCPUCap v, _) \<Rightarrow> throwError TruncatedMessage
  | _ \<Rightarrow> throwError IllegalOperation"
@@ -116,7 +116,8 @@ where
 
 text {* VCPU : inject IRQ *}
 
-(* ARMHYP FIXME see comment in VCPU_H *)
+(* This following function does not correspond to exactly what the C does, but
+it is the value that is stored inside of lr in the vgic  *)
 definition make_virq :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> obj_ref \<Rightarrow> virq" where
   "make_virq grp prio irq \<equiv>
   let

spec/abstract/IpcCancel_A.thy

@@ -102,8 +102,7 @@ where
 text {* Cancel all message operations on threads queued in a notification
 endpoint. *}
 
-text {* Miscellaneous NTFN binding stuff
+(* FIXME: Miscellaneous NTFN binding stuff, move upwards? *)
-FIXME! *}
 abbreviation
   ntfn_set_bound_tcb :: "notification \<Rightarrow> obj_ref option \<Rightarrow> notification"
 where
@@ -341,7 +340,6 @@ where
 
 text {* Cancel the message receive operation of a thread queued in an
 notification object. *}
-(* FIXME: need some way of easily retrieving ntfnBoundTCB? *)
 definition
   cancel_signal :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
 where

spec/abstract/Retype_A.thy

@@ -134,8 +134,8 @@ definition
 
 (* FIXME: we need a sensible place for these configurable constants. *)
 definition
-  reset_chunk_bits :: nat
+  reset_chunk_bits :: nat where
-where "reset_chunk_bits = 8"
+  "reset_chunk_bits = 8"
 
 definition
   get_free_ref :: "obj_ref \<Rightarrow> nat \<Rightarrow> obj_ref" where

spec/abstract/X64/ArchCSpace_A.thy

@@ -66,11 +66,10 @@ where
 | "arch_same_region_as (PML4Cap r _) c' = (\<exists>r' d'. c' = PML4Cap r' d' \<and> r = r')"
 | "arch_same_region_as ASIDControlCap c' = (c' = ASIDControlCap)"
 | "arch_same_region_as (ASIDPoolCap r _) c' = (\<exists>r' d'. c' = ASIDPoolCap r' d' \<and> r = r')"
-(* FIXME x64-vtd: *)
+(* FIXME x64-vtd:
-(*
 | "arch_same_region_as (IOPageTableCap r _ _) c = (is_IOPageTableCap c \<and> aobj_ref c = Some r)"
 | "arch_same_region_as (IOSpaceCap d_id pci_d) c = (is_IOSpaceCap c \<and> cap_io_pci_device c = pci_d)"
-  --"FIXME: should this also check domain id equality? C kernel does not"
+  FIXME x64-vtd: should this also check domain id equality? C kernel does not"
 *)
 | "arch_same_region_as (IOPortCap frst lst) c' =
    (\<exists>frst' lst'. c' = IOPortCap frst' lst' \<and> frst' = frst \<and> lst' = lst)"
@@ -87,7 +86,6 @@ definition
     | (IOPortControlCap, IOPortCap f' l') \<Rightarrow> False
     | _ \<Rightarrow> arch_same_region_as cp cp')"
 
-(* Proofs don't want to see this definition *)
 declare same_aobject_as_def[simp]
 
 definition

spec/abstract/X64/ArchInvocation_A.thy

@@ -81,7 +81,7 @@ datatype page_invocation
          (page_iomap_cap: cap)
          (page_iomap_ct_clot: cslot_ptr)
          (page_iomap_asid: iopte)
-         (page_iomap_entries: "obj_ref") (*FIXME: double check plz*)*)
+         (page_iomap_entries: "obj_ref") *)
      | PageGetAddr
          (page_get_paddr: obj_ref)
 

spec/abstract/X64/ArchTcb_A.thy

@@ -38,14 +38,13 @@ definition
 where
   "sanitise_and_flags \<equiv> mask 12 && ~~ bit 8 && ~~ bit 3 && ~~ bit 5"
 
-(* FIXME x64: this is disgusting *)
 definition
   sanitise_register :: "bool \<Rightarrow> register \<Rightarrow> machine_word \<Rightarrow> machine_word"
 where
   "sanitise_register t r v \<equiv>
-    let val = (if (r = FaultIP \<or> r = NextIP) then
+    let val = (if r = FaultIP \<or> r = NextIP
-                if (v > 0x00007fffffffffff \<and> v < 0xffff800000000000) then 0 else v
+               then if v > 0x00007fffffffffff \<and> v < 0xffff800000000000 then 0 else v
-              else v)
+               else v)
     in
       if r = FLAGS then (val || sanitise_or_flags) && sanitise_and_flags else val"
 

spec/abstract/X64/ArchVSpace_A.thy

@@ -338,11 +338,6 @@ check_mapping_pptr :: "machine_word \<Rightarrow> vm_page_entry \<Rightarrow> bo
  | VMPDPTE (HugePagePDPTE base _ _) \<Rightarrow> base = addrFromPPtr pptr
  | _ \<Rightarrow> False"
 
-(* FIXME: move to generic *)
-text {* Raise an exception if a property does not hold. *}
-definition
-throw_on_false :: "'e \<Rightarrow> (bool,'z::state_ext) s_monad \<Rightarrow> ('e + unit,'z::state_ext) s_monad" where
-"throw_on_false ex f \<equiv> doE v \<leftarrow> liftE f; unlessE v $ throwError ex odE"
 
 text {* Unmap a mapped page if the given mapping details are still current. *}
 definition

spec/abstract/X64/Arch_A.thy

@@ -47,15 +47,6 @@ definition
     od)
    )"
 
-
-(*FIXME x64: Current C code doesn't work for addresses above 32 bits.
-  This is meant to take a base address and craft a default
-  gdt_data structure. *)
-
-definition
-  base_to_gdt_data_word :: "machine_word \<Rightarrow> machine_word" where
-  "base_to_gdt_data_word = undefined"
-
 text {* Switch to a thread's virtual address space context and write its IPC
 buffer pointer into the globals frame. Clear the load-exclusive monitor. *}
 
@@ -66,7 +57,6 @@ definition
   arch_switch_to_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_switch_to_thread t \<equiv> set_vm_root t"
 
-(* x64 done *)
 definition
    arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad" where
    "arch_switch_to_idle_thread \<equiv> do
@@ -74,7 +64,6 @@ definition
      set_vm_root thread
    od"
 
-(* x64 done *)
 definition
   arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_activate_idle_thread t \<equiv> return ()"
@@ -182,7 +171,7 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
                         | _ \<Rightarrow> fail
             | None \<Rightarrow> return ()
       | _ \<Rightarrow> fail)
-(*  | PageIOMap asid cap ct_slot entries \<Rightarrow> undefined (* FIXME unimplemented *)*)
+(*  | PageIOMap asid cap ct_slot entries \<Rightarrow> undefined *)
   | PageGetAddr ptr \<Rightarrow> do
       paddr \<leftarrow> return $ fromPAddr $ addrFromPPtr ptr;
       ct \<leftarrow> gets cur_thread;
@@ -191,8 +180,7 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
       set_message_info ct msg_info
     od)"
 
-text {* PageTable capabilities confer the authority to map and unmap page
+text {* PageTable capabilities confer the authority to map and unmap page tables. *}
-tables. *}
 definition
 perform_page_table_invocation :: "page_table_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
 "perform_page_table_invocation iv \<equiv>

spec/abstract/X64/Arch_Structs_A.thy

@@ -67,7 +67,6 @@ section {* Architecture-specific objects *}
 datatype table_attr = Accessed | CacheDisabled | WriteThrough | ExecuteDisable
 type_synonym table_attrs = "table_attr set"
 
-(* FIXME: better keep two separate sets? *)
 datatype frame_attr = PTAttr table_attr | Global | PAT | Dirty
 type_synonym frame_attrs = "frame_attr set"
 

spec/haskell/src/SEL4/Object/VCPU/ARM.lhs

@@ -207,8 +207,8 @@ Currently, there is only one VCPU register available for reading/writing by the
 
 \subsection{VCPU: inject IRQ}
 
-FIXME ARMHYP: this does not at this instance correspond to exactly what the C
+This following function does not correspond to exactly what the C does, but
-    does, but it is the value that is stored inside of lr in the vgic
+it is the value that is stored inside of lr in the vgic
 
 > makeVIRQ :: Word -> Word -> Word -> VIRQ
 > makeVIRQ grp prio irq =