source: extracted/interpret2.mli @ 2910

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

Abstract statuses for ASM and OC completed.
A simple test program can now be run in every pass of the compiler, always
showing the same behaviour (up to initialization).

File size: 2.6 KB
Line 
1open Preamble
2
3open Fetch
4
5open Hide
6
7open Division
8
9open Z
10
11open BitVectorZ
12
13open Pointers
14
15open Coqlib
16
17open Values
18
19open Events
20
21open IOMonad
22
23open IO
24
25open Sets
26
27open Listb
28
29open StructuredTraces
30
31open AbstractStatus
32
33open BitVectorTrie
34
35open String
36
37open Exp
38
39open Arithmetic
40
41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Extranat
48
49open Integers
50
51open AST
52
53open LabelledObjects
54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
61open ErrorMessages
62
63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Setoids
70
71open Monad
72
73open Option
74
75open Div_and_mod
76
77open Jmeq
78
79open Russell
80
81open Util
82
83open List
84
85open Lists
86
87open Bool
88
89open Relations
90
91open Nat
92
93open Positive
94
95open Hints_declaration
96
97open Core_notation
98
99open Pts
100
101open Logic
102
103open Types
104
105open Identifiers
106
107open CostLabel
108
109open ASM
110
111open Status
112
113open StatusProofs
114
115open Interpret
116
117open ASMCosts
118
119open SmallstepExec
120
121open Executions
122
123open Measurable
124
125val mk_trans_system_of_abstract_status :
126  StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
127  (IO.io_out, IO.io_in) SmallstepExec.trans_system
128
129val mk_fullexec_of_abstract_status :
130  StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
131  __ -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
132
133val mk_preclassified_system_of_abstract_status :
134  StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
135  __ -> Measurable.preclassified_system
136
137val oC_preclassified_system :
138  ASM.labelled_object_code -> Measurable.preclassified_system
139
140open Assembly
141
142val execute_1_pseudo_instruction' :
143  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
144  (BitVector.word -> Bool.bool) -> Status.pseudoStatus -> Status.pseudoStatus
145
146val classify_pseudo_instruction :
147  ASM.pseudo_instruction -> StructuredTraces.status_class
148
149val aSM_classify :
150  ASM.pseudo_assembly_program -> Status.pseudoStatus ->
151  StructuredTraces.status_class
152
153val aSM_as_label_of_pc :
154  ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
155  Types.option
156
157val aSM_as_result :
158  ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
159  Types.option
160
161open AssocList
162
163val aSM_as_call_ident :
164  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
165  (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
166  AST.ident
167
168val aSM_abstract_status :
169  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
170  (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status
171
172val aSM_preclassified_system :
173  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
174  (BitVector.word -> Bool.bool) -> Measurable.preclassified_system
175
Note: See TracBrowser for help on using the repository browser.