source: src/ERTLptr/uses.ma @ 3010

Last change on this file since 3010 was 3010, checked in by tranquil, 7 years ago

same bug as was in liveness is now fixed

File size: 3.1 KB
Line 
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
15include "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
20definition 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
40      | CALL id _ _ ⇒
41        match id with
42        [ inr pr ⇒ incr_arg (\fst pr) (incr_arg (\snd pr) map)
43        | _ ⇒ map
44        ]
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 …).
Note: See TracBrowser for help on using the repository browser.