source: src/ERTLptr/uses.ma @ 2741

Last change on this file since 2741 was 2741, checked in by sacerdot, 7 years ago

File used only by untrusted code.
Implemented in Matita to exploit better typing.

File size: 3.0 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 _ _ _ ⇒ map
41      | COND r _ ⇒ incr r map
42      | step_seq s ⇒
43         match s with
44         [ COMMENT _ ⇒ map
45         | ADDRESS _ _ _ _ ⇒ map
46         | CLEAR_CARRY ⇒ map
47         | SET_CARRY ⇒ map
48         | MOVE pair ⇒
49            let 〈r1,r2〉 ≝ pair in
50            let incr_dst ≝ λarg,map.
51             match arg with
52             [ PSD r ⇒ incr r map
53             | HDW _ ⇒ map ] in
54            incr_dst r1
55             match r2 with
56             [ Reg a ⇒ incr_dst a map
57             | Imm _ ⇒ map ]
58         | POP r ⇒ incr r map
59         | PUSH r ⇒ incr_arg r map
60         | OPACCS _ r1 r2 r3 r4 ⇒
61            incr r1 (incr r2 (incr_arg r3 (incr_arg r4 map)))
62         | OP1 _ r1 r2 ⇒ incr r1 (incr r2 map)
63         | OP2 _ r1 r2 r3 ⇒ incr r1 (incr_arg r2 (incr_arg r3 map))
64         | LOAD r1 _ _ ⇒ incr r1 map
65         | STORE _ _ r ⇒ incr_arg r map
66         | extension_seq s ⇒
67            match s with
68            [ ertlptr_ertl s ⇒
69               match s with
70               [ ertl_new_frame ⇒ map
71               | ertl_del_frame ⇒ map
72               | ertl_frame_size r ⇒ incr r map ]
73            | LOW_ADDRESS r _ ⇒ incr r map
74            | HIGH_ADDRESS r _ ⇒ incr r map ]]]
75   | final _ ⇒ map
76   | FCOND (abs : has_fcond ERTLptr) _ _ _ ⇒ Ⓧabs ]
77 in
78 foldi … f (joint_if_code … fun) (empty_map …).
Note: See TracBrowser for help on using the repository browser.