(**************************************************************************) (* ARM/Power Multiprocessor Machine Code Semantics: HOL sources *) (* *) (* *) (* Jade Alglave (2), Anthony Fox (1), Samin Isthiaq (3), *) (* Magnus Myreen (1), Susmit Sarkar (1), Peter Sewell (1), *) (* Francesco Zappa Nardelli (2) *) (* *) (* (1) Computer Laboratory, University of Cambridge *) (* (2) Moscova project, INRIA Paris-Rocquencourt *) (* (3) Microsoft Research Cambridge *) (* *) (* Copyright 2007-2008 *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) (* notice, this list of conditions and the following disclaimer in *) (* the documentation and/or other materials provided with the *) (* distribution. *) (* 3. The names of the authors may not be used to endorse or promote *) (* products derived from this software without specific prior *) (* written permission. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) (* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) (* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) (* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) (* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) (* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) (* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) (* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, *) (* WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING *) (* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS *) (* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (* *) (**************************************************************************) open HolKernel boolLib bossLib Parse; open wordsTheory bit_listTheory listTheory; open common_coretypesTheory common_typesTheory arm_coretypesTheory arm_typesTheory; open arm_astTheory arm_event_monadTheory arm_event_opsemTheory ; open arm_decoderTheory; open ppc_arm_axiomatic_modelTheory; (*open arm_Theory;*) open utilTheory; open HolDoc; val _ = new_theory "arm_program"; (* ---------------------------------------------------------------------------------- *> Here the decoder from arm_decoderTheory is put together with arm_execute from arm_event_opsemTheory and the event structure monad from arm_event_monadTheory. <* ---------------------------------------------------------------------------------- *) (* **************************** *) (* decoding *) (* **************************** *) val _ = Define `VERSION_MULTICORE = 7`; (* We only ever decode this version in an event structure world *) val _ = type_abbrev ("Ainstruction", ``: (ARMcondition # ARMinstruction) ``); val _ = type_abbrev("program_Ainstruction", ``: (address -> (Ainstruction#num) option) ``); (* try to decode an instruction from an address in a program_word8 memory (record the length too, to avoid having to define a separate length_of_Xinst) *) (* check that prog_Xinst is a correct decoding of prog_word8 (the relational version allows the domain of prog_Xinst to be an arbitrary subset of the domain of prog_word8, whereas the functional version gives a decoding (if possible) for every address in the domain of prog_word8) *) val _ = Define `(arm_decode_program_fun : program_word8 -> address -> (Ainstruction#num) option) prog_word8 a = if (a && 3w = 0w) then NONE else let w0 = prog_word8 (a + 0w) in let w1 = prog_word8 (a + 1w) in let w2 = prog_word8 (a + 2w) in let w3 = prog_word8 (a + 3w) in if MEM NONE [w0;w1;w2;w3] then NONE else let (raw_instruction : word32) = (THE w0) @@ (((THE w1) @@ (((THE w2) @@ (THE w3)) : word16)) : word24) in let i = arm_decode VERSION_MULTICORE raw_instruction in SOME (i,4) `; val _ = Define `(arm_decode_program_rel : program_word8 -> program_Ainstruction -> bool) prog_word8 prog_Xinst = !a. case prog_Xinst a of NONE -> T || SOME (inst,n) -> arm_decode_program_fun prog_word8 a = SOME (inst,n)`; (* **************************** *) (* event structure semantics *) (* **************************** *) (* the event structure semantics of a single instruction *) val _ = Define `arm_event_execute = arm_event_opsem$arm_execute`; (* the event structure semantics of a single instruction, restricted to those for which any reads of PC are the specified value *) val _ = Define `arm_execute_with_pc_check ii inst pc = let s = (arm_event_execute ii inst) {} in { E | ?eiid_next x. (eiid_next,x,E) IN s /\ ! v ev. ((ev.action=(Access R (Location_reg ii.proc (Reg32 r15)) v)) /\ ev IN E.events) ==> (v=pc) } `; (* let eiid_start = if j=0 then 0 else (\x. case x of NONE -> 0 || SOME (eiid,x_unit,E) -> eiid) (E_eiid_s (j-1)) in *) val _ = Define ` (arm_event_structures_of_run_skeleton:program_Ainstruction -> run_skeleton -> (arm_reg event_structure) set) prog_Ainstruction rs = let Ess = {arm_execute_with_pc_check <|proc:=p;poi:=i|> inst pc | ?n. (rs p i = SOME pc) /\ (SOME (inst, n) = prog_Ainstruction pc)} in {event_structure_bigunion Es | Es IN all_choices Ess}`; (* all such event structures are well-formed - cf arm_program_event_structure_wfScript.sml *) (* TODO: we need to define an additional "completed" predicate when we want to talk about completed executions *) (* finally, putting all this together *) val _ = Define `(arm_semantics : program_word8 -> (arm_reg state_constraint) -> (run_skeleton # program_Ainstruction # (((arm_reg event_structure) # ((arm_reg execution_witness) set)) set)) set) prog_word8 initial_state = let x1 = { (rs,prog_Xinst) | rs,prog_Xinst | run_skeleton_wf (DOMAIN prog_Xinst) rs /\ arm_decode_program_rel prog_word8 prog_Xinst } in let x2 = { (rs,prog_Xinst,Es) | (rs,prog_Xinst) IN x1 /\ (Es = arm_event_structures_of_run_skeleton prog_Xinst rs) } in let x3 = { (rs,prog_Xinst,{(E,Xs) | E IN Es /\ (Xs = { X | valid_execution E X /\ (X.initial_state = initial_state) })}) | (rs,prog_Xinst,Es) IN x2} in x3 `; val _ = export_theory ();