source: extracted/uses.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 3.4 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107open ERTL
108
109open ERTLptr
110
111(** val examine_internal :
112    AST.ident List.list -> Joint.joint_internal_function -> Positive.pos
113    Identifiers.identifier_map **)
114let examine_internal globals fun0 =
115  let incr = fun r map ->
116    match Identifiers.lookup PreIdentifiers.RegisterTag map r with
117    | Types.None ->
118      Identifiers.add PreIdentifiers.RegisterTag map r Positive.One
119    | Types.Some v ->
120      Identifiers.add PreIdentifiers.RegisterTag map r (Positive.succ v)
121  in
122  let incr_arg = fun arg map ->
123    match arg with
124    | Joint.Reg r -> incr r map
125    | Joint.Imm x -> map
126  in
127  let f = fun x instr map ->
128    match instr with
129    | Joint.Sequential (s, x0) ->
130      (match s with
131       | Joint.COST_LABEL x1 -> map
132       | Joint.CALL (x1, x2, x3) -> map
133       | Joint.COND (r, x1) -> Obj.magic incr r map
134       | Joint.Step_seq s0 ->
135         (match s0 with
136          | Joint.COMMENT x1 -> map
137          | Joint.MOVE pair ->
138            let { Types.fst = r1; Types.snd = r2 } = Obj.magic pair in
139            let incr_dst = fun arg map0 ->
140              match arg with
141              | ERTL.PSD r -> incr r map0
142              | ERTL.HDW x1 -> map0
143            in
144            incr_dst r1
145              (match r2 with
146               | Joint.Reg a -> incr_dst a map
147               | Joint.Imm x1 -> map)
148          | Joint.POP r -> Obj.magic incr r map
149          | Joint.PUSH r -> Obj.magic incr_arg r map
150          | Joint.ADDRESS (x1, x3, x4) -> map
151          | Joint.OPACCS (x1, r1, r2, r3, r4) ->
152            Obj.magic incr r1
153              (Obj.magic incr r2
154                (Obj.magic incr_arg r3 (Obj.magic incr_arg r4 map)))
155          | Joint.OP1 (x1, r1, r2) ->
156            Obj.magic incr r1 (Obj.magic incr r2 map)
157          | Joint.OP2 (x1, r1, r2, r3) ->
158            Obj.magic incr r1
159              (Obj.magic incr_arg r2 (Obj.magic incr_arg r3 map))
160          | Joint.CLEAR_CARRY -> map
161          | Joint.SET_CARRY -> map
162          | Joint.LOAD (r1, x1, x2) -> Obj.magic incr r1 map
163          | Joint.STORE (x1, x2, r) -> Obj.magic incr_arg r map
164          | Joint.Extension_seq s1 ->
165            (match Obj.magic s1 with
166             | ERTLptr.Ertlptr_ertl s2 ->
167               (match s2 with
168                | ERTL.Ertl_new_frame -> map
169                | ERTL.Ertl_del_frame -> map
170                | ERTL.Ertl_frame_size r -> incr r map)
171             | ERTLptr.LOW_ADDRESS (r, x1) -> incr r map
172             | ERTLptr.HIGH_ADDRESS (r, x1) -> incr r map)))
173    | Joint.Final x0 -> map
174    | Joint.FCOND (x0, x1, x2) -> assert false (* absurd case *)
175  in
176  Identifiers.foldi PreIdentifiers.LabelTag f
177    (Obj.magic fun0.Joint.joint_if_code)
178    (Identifiers.empty_map PreIdentifiers.RegisterTag)
179
Note: See TracBrowser for help on using the repository browser.