source: extracted/costSpec.ml @ 2746

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

Exported again.

File size: 4.0 KB
Line 
1open Preamble
2
3open Graphs
4
5open Order
6
7open Registers
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open GenMem
16
17open FrontEndMem
18
19open Division
20
21open Z
22
23open BitVectorZ
24
25open Pointers
26
27open Coqlib
28
29open Values
30
31open FrontEndOps
32
33open BitVectorTrie
34
35open CostLabel
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Setoids
52
53open Monad
54
55open Option
56
57open Lists
58
59open Positive
60
61open Identifiers
62
63open Exp
64
65open Arithmetic
66
67open Vector
68
69open Div_and_mod
70
71open Jmeq
72
73open Russell
74
75open List
76
77open Util
78
79open FoldStuff
80
81open BitVector
82
83open Extranat
84
85open Bool
86
87open Relations
88
89open Nat
90
91open Integers
92
93open Types
94
95open AST
96
97open Hints_declaration
98
99open Core_notation
100
101open Pts
102
103open Logic
104
105open RTLabs_syntax
106
107(** val is_cost_label : RTLabs_syntax.statement -> Bool.bool **)
108let is_cost_label = function
109| RTLabs_syntax.St_skip x -> Bool.False
110| RTLabs_syntax.St_cost (x, x0) -> Bool.True
111| RTLabs_syntax.St_const (x, x0, x1, x2) -> Bool.False
112| RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> Bool.False
113| RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) -> Bool.False
114| RTLabs_syntax.St_load (x, x0, x1, x2) -> Bool.False
115| RTLabs_syntax.St_store (x, x0, x1, x2) -> Bool.False
116| RTLabs_syntax.St_call_id (x, x0, x1, x2) -> Bool.False
117| RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> Bool.False
118| RTLabs_syntax.St_cond (x, x0, x1) -> Bool.False
119| RTLabs_syntax.St_return -> Bool.False
120
121(** val cost_label_of :
122    RTLabs_syntax.statement -> CostLabel.costlabel Types.option **)
123let cost_label_of = function
124| RTLabs_syntax.St_skip x -> Types.None
125| RTLabs_syntax.St_cost (s0, x) -> Types.Some s0
126| RTLabs_syntax.St_const (x, x0, x1, x2) -> Types.None
127| RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> Types.None
128| RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) -> Types.None
129| RTLabs_syntax.St_load (x, x0, x1, x2) -> Types.None
130| RTLabs_syntax.St_store (x, x0, x1, x2) -> Types.None
131| RTLabs_syntax.St_call_id (x, x0, x1, x2) -> Types.None
132| RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> Types.None
133| RTLabs_syntax.St_cond (x, x0, x1) -> Types.None
134| RTLabs_syntax.St_return -> Types.None
135
136(** val well_cost_labelled_statement :
137    RTLabs_syntax.statement Graphs.graph -> RTLabs_syntax.statement ->
138    Bool.bool **)
139let well_cost_labelled_statement g0 s =
140  (match s with
141   | RTLabs_syntax.St_skip x -> (fun _ -> Bool.True)
142   | RTLabs_syntax.St_cost (x, x0) -> (fun _ -> Bool.True)
143   | RTLabs_syntax.St_const (x, x0, x1, x2) -> (fun _ -> Bool.True)
144   | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> (fun _ -> Bool.True)
145   | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) ->
146     (fun _ -> Bool.True)
147   | RTLabs_syntax.St_load (x, x0, x1, x2) -> (fun _ -> Bool.True)
148   | RTLabs_syntax.St_store (x, x0, x1, x2) -> (fun _ -> Bool.True)
149   | RTLabs_syntax.St_call_id (x, x0, x1, x2) -> (fun _ -> Bool.True)
150   | RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> (fun _ -> Bool.True)
151   | RTLabs_syntax.St_cond (x, l1, l2) ->
152     (fun _ ->
153       Bool.andb
154         (is_cost_label
155           (Identifiers.lookup_present PreIdentifiers.LabelTag g0 l1))
156         (is_cost_label
157           (Identifiers.lookup_present PreIdentifiers.LabelTag g0 l2)))
158   | RTLabs_syntax.St_return -> (fun _ -> Bool.True)) __
159
160(** val successors : RTLabs_syntax.statement -> Graphs.label List.list **)
161let rec successors = function
162| RTLabs_syntax.St_skip l -> List.Cons (l, List.Nil)
163| RTLabs_syntax.St_cost (x, l) -> List.Cons (l, List.Nil)
164| RTLabs_syntax.St_const (x, x0, x1, l) -> List.Cons (l, List.Nil)
165| RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, l) -> List.Cons (l, List.Nil)
166| RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, l) ->
167  List.Cons (l, List.Nil)
168| RTLabs_syntax.St_load (x, x0, x1, l) -> List.Cons (l, List.Nil)
169| RTLabs_syntax.St_store (x, x0, x1, l) -> List.Cons (l, List.Nil)
170| RTLabs_syntax.St_call_id (x, x0, x1, l) -> List.Cons (l, List.Nil)
171| RTLabs_syntax.St_call_ptr (x, x0, x1, l) -> List.Cons (l, List.Nil)
172| RTLabs_syntax.St_cond (x, l1, l2) ->
173  List.Cons (l1, (List.Cons (l2, List.Nil)))
174| RTLabs_syntax.St_return -> List.Nil
175
Note: See TracBrowser for help on using the repository browser.