From a9e8518c1d24ccf6fcdd7335ed6c520e73f3920e Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Tue, 11 Apr 2017 18:37:30 +1000 Subject: [PATCH] x64: abstract: minor tweak to throws in arch_decode_irq_control_invocation --- proof/invariant-abstract/X64/ArchInterrupt_AI.thy | 1 - spec/abstract/X64/ArchDecode_A.thy | 10 ++++------ 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy index fee7b21b9..63bc0f1f3 100644 --- a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy @@ -14,7 +14,6 @@ begin context Arch begin global_naming X64 -thm irq_control_inv_valid.simps arch_decode_irq_control_invocation_def primrec arch_irq_control_inv_valid_real :: "arch_irq_control_invocation \ 'a::state_ext state \ bool" where "arch_irq_control_inv_valid_real (IssueIRQHandlerIOAPIC irq dest_slot src_slot diff --git a/spec/abstract/X64/ArchDecode_A.thy b/spec/abstract/X64/ArchDecode_A.thy index 0755fd835..0beac589a 100644 --- a/spec/abstract/X64/ArchDecode_A.thy +++ b/spec/abstract/X64/ArchDecode_A.thy @@ -67,18 +67,16 @@ definition in doE whenE (x > ucast maxIRQ) $ throwError (RangeError 0 (ucast maxIRQ)); - - dest_slot \ lookup_target_slot cnode (data_to_cptr index) (unat depth); - ensure_empty dest_slot; - irq_active \ liftE $ is_irq_active irqv; whenE irq_active $ throwError RevokeFirst; + dest_slot \ lookup_target_slot cnode (data_to_cptr index) (unat depth); + ensure_empty dest_slot; (* Following should be wrapped in to a funcion like what c did since it is pc99 related, problem is where to put this function*) - whenE (ioapic > numIOAPICs - 1) $ throwError (RangeError 0 numIOAPICs); - whenE (pin > ioapicIRQLines - 1) $ throwError (RangeError 0 ioapicIRQLines); + whenE (ioapic > numIOAPICs - 1) $ throwError (RangeError 0 (numIOAPICs-1)); + whenE (pin > ioapicIRQLines - 1) $ throwError (RangeError 0 (ioapicIRQLines-1)); whenE (level > 1) $ throwError (RangeError 0 1); whenE (polarity > 1) $ throwError (RangeError 0 1);