[2741] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "ERTLptr/ERTLptr.ma". |
---|
| 16 | |
---|
| 17 | (* This file is used only by untrusted code. We write it in Matita to |
---|
| 18 | benefit from the typing system *) |
---|
| 19 | |
---|
| 20 | definition examine_internal: |
---|
| 21 | ∀globals. joint_internal_function ERTLptr globals → |
---|
| 22 | identifier_map RegisterTag Pos ≝ |
---|
| 23 | λglobals,fun. |
---|
| 24 | let incr ≝ |
---|
| 25 | λr,map. |
---|
| 26 | match lookup RegisterTag Pos map r with |
---|
| 27 | [ None ⇒ add … map r one |
---|
| 28 | | Some v ⇒ add … map r (succ v) ] in |
---|
| 29 | let incr_arg ≝ |
---|
| 30 | λarg,map. |
---|
| 31 | match arg with |
---|
| 32 | [ Imm _ ⇒ map |
---|
| 33 | | Reg r ⇒ incr r map ] in |
---|
| 34 | let f ≝ |
---|
| 35 | λ_.λinstr.λmap. |
---|
| 36 | match instr with |
---|
| 37 | [ sequential s _ ⇒ |
---|
| 38 | match s with |
---|
| 39 | [ COST_LABEL _ ⇒ map |
---|
[3010] | 40 | | CALL id _ _ ⇒ |
---|
| 41 | match id with |
---|
| 42 | [ inr pr ⇒ incr_arg (\fst pr) (incr_arg (\snd pr) map) |
---|
| 43 | | _ ⇒ map |
---|
| 44 | ] |
---|
[2741] | 45 | | COND r _ ⇒ incr r map |
---|
| 46 | | step_seq s ⇒ |
---|
| 47 | match s with |
---|
| 48 | [ COMMENT _ ⇒ map |
---|
| 49 | | ADDRESS _ _ _ _ ⇒ map |
---|
| 50 | | CLEAR_CARRY ⇒ map |
---|
| 51 | | SET_CARRY ⇒ map |
---|
| 52 | | MOVE pair ⇒ |
---|
| 53 | let 〈r1,r2〉 ≝ pair in |
---|
| 54 | let incr_dst ≝ λarg,map. |
---|
| 55 | match arg with |
---|
| 56 | [ PSD r ⇒ incr r map |
---|
| 57 | | HDW _ ⇒ map ] in |
---|
| 58 | incr_dst r1 |
---|
| 59 | match r2 with |
---|
| 60 | [ Reg a ⇒ incr_dst a map |
---|
| 61 | | Imm _ ⇒ map ] |
---|
| 62 | | POP r ⇒ incr r map |
---|
| 63 | | PUSH r ⇒ incr_arg r map |
---|
| 64 | | OPACCS _ r1 r2 r3 r4 ⇒ |
---|
| 65 | incr r1 (incr r2 (incr_arg r3 (incr_arg r4 map))) |
---|
| 66 | | OP1 _ r1 r2 ⇒ incr r1 (incr r2 map) |
---|
| 67 | | OP2 _ r1 r2 r3 ⇒ incr r1 (incr_arg r2 (incr_arg r3 map)) |
---|
| 68 | | LOAD r1 _ _ ⇒ incr r1 map |
---|
| 69 | | STORE _ _ r ⇒ incr_arg r map |
---|
| 70 | | extension_seq s ⇒ |
---|
| 71 | match s with |
---|
| 72 | [ ertlptr_ertl s ⇒ |
---|
| 73 | match s with |
---|
| 74 | [ ertl_new_frame ⇒ map |
---|
| 75 | | ertl_del_frame ⇒ map |
---|
| 76 | | ertl_frame_size r ⇒ incr r map ] |
---|
| 77 | | LOW_ADDRESS r _ ⇒ incr r map |
---|
| 78 | | HIGH_ADDRESS r _ ⇒ incr r map ]]] |
---|
| 79 | | final _ ⇒ map |
---|
| 80 | | FCOND (abs : has_fcond ERTLptr) _ _ _ ⇒ Ⓧabs ] |
---|
| 81 | in |
---|
| 82 | foldi … f (joint_if_code … fun) (empty_map …). |
---|