Changeset 1910 for src/ASM/Interpret.ma
 Timestamp:
 Apr 27, 2012, 5:48:20 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1909 r1910 927 927 qed. 928 928 929 definition program_counter_after_other ≝ 930 λprogram_counter. (* XXX: program counter after fetching *) 931 λinstruction. 932 if is_unconditional_jump instruction then 933 compute_target_of_unconditional_jump program_counter instruction 934 else 935 program_counter. 936 929 937 definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat. 930 938 Σs': Status cm. 931 939 And (clock ?? s' = \snd current + clock … s) 932 ( if is_unconditional_jump (\fst (\fst current)) then940 (ASM_classify0 (\fst (\fst current)) = cl_other → 933 941 program_counter ? ? s' = 934 compute_target_of_unconditional_jump (\snd (\fst current)) (\fst (\fst current)) 935 else 936 (ASM_classify0 (\fst (\fst current)) = cl_other → 937 program_counter ? ? s' = \snd (\fst current))) ≝ 942 program_counter_after_other (\snd (\fst current)) (\fst (\fst current))) ≝ 938 943 λcm,s0,instr_pc_ticks. 939 944 let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in … … 1054 1059 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 1055 1060 And (clock ?? s' = current_instruction_cost cm s + clock … s) 1056 ( if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then1061 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1057 1062 program_counter ? ? s' = 1058 compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks)) 1059 else 1060 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1061 program_counter ? ? s' = \snd (\fst instr_pc_ticks))) ≝ 1063 program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))) ≝ 1062 1064 λcm. λs: Status cm. 1063 1065 let instr_pc_ticks ≝ fetch cm (program_counter … s) in … … 1079 1081 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 1080 1082 (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧ 1081 (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then 1082 program_counter ? cm (execute_1 cm s) = 1083 compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks)) 1084 else 1085 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1086 (program_counter ? cm (execute_1 cm s)) = \snd (\fst instr_pc_ticks))) 1083 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1084 program_counter ? cm (execute_1 cm s) = 1085 program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))). 1087 1086 (* (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *). 1088 1087 #cm #s normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.