source: extracted/uses.ml @ 3069

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

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