(**************************************************************************) (* 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 ppc_coretypesTheory ppc_typesTheory; open ppc_astTheory ppc_event_monadTheory ppc_event_opsemTheory ; open ppc_decoderTheory; open ppc_arm_axiomatic_modelTheory; (*open ppc_Theory;*) open utilTheory; open HolDoc; val _ = new_theory "ppc_program"; (* ---------------------------------------------------------------------------------- *> Here the decoder from ppc_decoderTheory is put together with ppc_execute from ppc_event_opsemTheory and the event structure monad from ppc_event_monadTheory. <* ---------------------------------------------------------------------------------- *) (* **************************** *) (* decoding *) (* **************************** *) val _ = type_abbrev("program_Pinstruction", ``: (address -> (Pinstruction#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 `(ppc_decode_program_fun : program_word8 -> address -> (Pinstruction#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 = w2bits (THE w0) ++ w2bits (THE w1) ++ w2bits (THE w2) ++ w2bits (THE w3) in let io = ppc_decode raw_instruction in case io of NONE -> NONE || SOME i -> SOME (i,4) `; val _ = Define `(ppc_decode_program_rel : program_word8 -> program_Pinstruction -> bool) prog_word8 prog_Xinst = !a. case prog_Xinst a of NONE -> T || SOME (inst,n) -> ppc_decode_program_fun prog_word8 a = SOME (inst,n)`; (* **************************** *) (* event structure semantics *) (* **************************** *) (* the event structure semantics of a single instruction *) val _ = Define `ppc_event_execute = ppc_event_opsem$ppc_exec_instr`; (* the event structure semantics of a single instruction, restricted to those for which any reads of PC are the specified value *) val _ = Define `ppc_execute_with_pc_check ii inst pc = let s = (ppc_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 PPC_PC)) 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 ` (ppc_event_structures_of_run_skeleton:program_Pinstruction -> run_skeleton -> (ppc_reg event_structure) set) prog_Pinstruction rs = let Ess = {ppc_execute_with_pc_check <|proc:=p;poi:=i|> inst pc | ?n. (rs p i = SOME pc) /\ (SOME (inst, n) = prog_Pinstruction pc)} in {event_structure_bigunion Es | Es IN all_choices Ess}`; (* all such event structures are well-formed - cf ppc_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 `(ppc_semantics : program_word8 -> (ppc_reg state_constraint) -> (run_skeleton # program_Pinstruction # (((ppc_reg event_structure) # ((ppc_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 /\ ppc_decode_program_rel prog_word8 prog_Xinst } in let x2 = { (rs,prog_Xinst,Es) | (rs,prog_Xinst) IN x1 /\ (Es = ppc_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 ();