extracted/costSpec.ml

   1 open Preamble
   2
   3 open BitVectorTrie
   4
   5 open Graphs
   6
   7 open Order
   8
   9 open Registers
  10
  11 open FrontEndVal
  12
  13 open Hide
  14
  15 open ByteValues
  16
  17 open GenMem
  18
  19 open FrontEndMem
  20
  21 open Division
  22
  23 open Z
  24
  25 open BitVectorZ
  26
  27 open Pointers
  28
  29 open Coqlib
  30
  31 open Values
  32
  33 open FrontEndOps
  34
  35 open CostLabel
  36
  37 open Proper
  38
  39 open PositiveMap
  40
  41 open Deqsets
  42
  43 open ErrorMessages
  44
  45 open PreIdentifiers
  46
  47 open Errors
  48
  49 open Extralib
  50
  51 open Lists
  52
  53 open Positive
  54
  55 open Identifiers
  56
  57 open Exp
  58
  59 open Arithmetic
  60
  61 open Vector
  62
  63 open Div_and_mod
  64
  65 open Util
  66
  67 open FoldStuff
  68
  69 open BitVector
  70
  71 open Jmeq
  72
  73 open Russell
  74
  75 open List
  76
  77 open Setoids
  78
  79 open Monad
  80
  81 open Option
  82
  83 open Extranat
  84
  85 open Bool
  86
  87 open Relations
  88
  89 open Nat
  90
  91 open Integers
  92
  93 open Types
  94
  95 open AST
  96
  97 open Hints_declaration
  98
  99 open Core_notation
 100
 101 open Pts
 102
 103 open Logic
 104
 105 open RTLabs_syntax
 106
 107 (** val is_cost_label : RTLabs_syntax.statement -> Bool.bool **)
 108 let 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 **)
 123 let 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 **)
 139 let well_cost_labelled_statement g 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 g l1))
 156          (is_cost_label
 157            (Identifiers.lookup_present PreIdentifiers.LabelTag g l2)))
 158    | RTLabs_syntax.St_return -> (fun _ -> Bool.True)) __
 159
 160 (** val successors : RTLabs_syntax.statement -> Graphs.label List.list **)
 161 let 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