extracted/joint_LTL_LIN_semantics.ml

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 open Joint_LTL_LIN
 122
 123 open ExtraMonads
 124
 125 open Deqsets_extra
 126
 127 open State
 128
 129 open Bind_new
 130
 131 open BindLists
 132
 133 open Blocks
 134
 135 open TranslateUtils
 136
 137 open ExtraGlobalenvs
 138
 139 open I8051bis
 140
 141 open BEMem
 142
 143 open Events
 144
 145 open IOMonad
 146
 147 open IO
 148
 149 open Joint_semantics
 150
 151 open SemanticsUtils
 152
 153 (** val hw_reg_store :
 154     I8051.register -> ByteValues.beval -> SemanticsUtils.hw_register_env ->
 155     SemanticsUtils.hw_register_env Errors.res **)
 156 let hw_reg_store r v e =
 157   Errors.OK (SemanticsUtils.hwreg_store r v e)
 158
 159 (** val hw_reg_retrieve :
 160     SemanticsUtils.hw_register_env -> I8051.register -> ByteValues.beval
 161     Errors.res **)
 162 let hw_reg_retrieve l r =
 163   Errors.OK (SemanticsUtils.hwreg_retrieve l r)
 164
 165 (** val hw_arg_retrieve :
 166     SemanticsUtils.hw_register_env -> I8051.register Joint.argument ->
 167     ByteValues.beval Errors.res **)
 168 let hw_arg_retrieve l = function
 169 | Joint.Reg r -> hw_reg_retrieve l r
 170 | Joint.Imm b -> Errors.OK (ByteValues.BVByte b)
 171
 172 (** val eval_registers_move :
 173     SemanticsUtils.hw_register_env -> Joint_LTL_LIN.registers_move ->
 174     SemanticsUtils.hw_register_env Errors.res **)
 175 let eval_registers_move e = function
 176 | Joint_LTL_LIN.From_acc (r, x) ->
 177   hw_reg_store r (SemanticsUtils.hwreg_retrieve e I8051.RegisterA) e
 178 | Joint_LTL_LIN.To_acc (x, r) ->
 179   hw_reg_store I8051.RegisterA (SemanticsUtils.hwreg_retrieve e r) e
 180 | Joint_LTL_LIN.Int_to_reg (r, v) -> hw_reg_store r (ByteValues.BVByte v) e
 181 | Joint_LTL_LIN.Int_to_acc (x, v) ->
 182   hw_reg_store I8051.RegisterA (ByteValues.BVByte v) e
 183
 184 (** val lTL_LIN_state : Joint_semantics.sem_state_params **)
 185 let lTL_LIN_state =
 186   { Joint_semantics.empty_framesT = (Obj.magic Types.It);
 187     Joint_semantics.empty_regsT =
 188     (Obj.magic SemanticsUtils.init_hw_register_env);
 189     Joint_semantics.load_sp = (Obj.magic SemanticsUtils.hwreg_retrieve_sp);
 190     Joint_semantics.save_sp = (Obj.magic SemanticsUtils.hwreg_store_sp) }
 191
 192 (** val ltl_lin_fetch_external_args :
 193     AST.external_function -> Joint_semantics.state -> Nat.nat -> Values.val0
 194     List.list Errors.res **)
 195 let ltl_lin_fetch_external_args _ =
 196   failwith "AXIOM TO BE REALIZED"
 197
 198 (** val ltl_lin_set_result :
 199     Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
 200     Joint_semantics.state Errors.res **)
 201 let ltl_lin_set_result _ =
 202   failwith "AXIOM TO BE REALIZED"
 203
 204 (** val lTL_LIN_save_frame :
 205     Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
 206     Joint_semantics.state Errors.res **)
 207 let lTL_LIN_save_frame k x st =
 208   match k with
 209   | Joint_semantics.PTR ->
 210     Obj.magic
 211       (Monad.m_bind0 (Monad.max_def Errors.res0)
 212         (Obj.magic
 213           (ByteValues.byte_of_val ErrorMessages.BadFunction
 214             (SemanticsUtils.hwreg_retrieve
 215               (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs)
 216               I8051.RegisterA))) (fun v ->
 217         match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 218                 (Nat.S (Nat.S Nat.O)))))))) v
 219                 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 220                   (Nat.S (Nat.S Nat.O))))))))) with
 221         | Bool.True ->
 222           Monad.m_return0 (Monad.max_def Errors.res0)
 223             st.Joint_semantics.st_no_pc
 224         | Bool.False ->
 225           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 226             ErrorMessages.BadFunction), (List.Cons ((Errors.MSG
 227             ErrorMessages.BadPointer), List.Nil)))))))
 228   | Joint_semantics.ID ->
 229     Joint_semantics.push_ra lTL_LIN_state st.Joint_semantics.st_no_pc
 230       st.Joint_semantics.pc
 231
 232 (** val eval_LTL_LIN_ext_seq :
 233     AST.ident List.list -> 'a1 Joint_semantics.genv_gen ->
 234     Joint_LTL_LIN.ltl_lin_seq -> AST.ident -> Joint_semantics.state ->
 235     Joint_semantics.state Errors.res **)
 236 let eval_LTL_LIN_ext_seq globals ge s curr_id st =
 237   match s with
 238   | Joint_LTL_LIN.SAVE_CARRY ->
 239     let regs =
 240       SemanticsUtils.hwreg_set_other st.Joint_semantics.carry
 241         (Obj.magic st.Joint_semantics.regs)
 242     in
 243     Obj.magic
 244       (Monad.m_return0 (Monad.max_def Errors.res0)
 245         (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st))
 246   | Joint_LTL_LIN.RESTORE_CARRY ->
 247     let carry = (Obj.magic st.Joint_semantics.regs).SemanticsUtils.other_bit
 248     in
 249     Obj.magic
 250       (Monad.m_return0 (Monad.max_def Errors.res0)
 251         (Joint_semantics.set_carry lTL_LIN_state carry st))
 252   | Joint_LTL_LIN.LOW_ADDRESS l ->
 253     Obj.magic
 254       (Monad.m_bind0 (Monad.max_def Errors.res0)
 255         (Obj.magic (Joint_semantics.gen_pc_from_label globals ge curr_id l))
 256         (fun pc_lab ->
 257         let { Types.fst = addrl; Types.snd = addrh } =
 258           ByteValues.beval_pair_of_pc pc_lab
 259         in
 260         let regs =
 261           SemanticsUtils.hwreg_store I8051.RegisterA addrl
 262             (Obj.magic st.Joint_semantics.regs)
 263         in
 264         Monad.m_return0 (Monad.max_def Errors.res0)
 265           (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st)))
 266   | Joint_LTL_LIN.HIGH_ADDRESS l ->
 267     Obj.magic
 268       (Monad.m_bind0 (Monad.max_def Errors.res0)
 269         (Obj.magic (Joint_semantics.gen_pc_from_label globals ge curr_id l))
 270         (fun pc_lab ->
 271         let { Types.fst = addrl; Types.snd = addrh } =
 272           ByteValues.beval_pair_of_pc pc_lab
 273         in
 274         let regs =
 275           SemanticsUtils.hwreg_store I8051.RegisterA addrh
 276             (Obj.magic st.Joint_semantics.regs)
 277         in
 278         Monad.m_return0 (Monad.max_def Errors.res0)
 279           (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st)))
 280
 281 (** val lTL_LIN_semantics : 'a1 Joint_semantics.sem_unserialized_params **)
 282 let lTL_LIN_semantics =
 283   { Joint_semantics.st_pars = lTL_LIN_state; Joint_semantics.acca_store_ =
 284     (fun x -> Obj.magic (hw_reg_store I8051.RegisterA));
 285     Joint_semantics.acca_retrieve_ = (fun e x ->
 286     hw_reg_retrieve (Obj.magic e) I8051.RegisterA);
 287     Joint_semantics.acca_arg_retrieve_ = (fun e x ->
 288     hw_reg_retrieve (Obj.magic e) I8051.RegisterA);
 289     Joint_semantics.accb_store_ = (fun x ->
 290     Obj.magic (hw_reg_store I8051.RegisterB));
 291     Joint_semantics.accb_retrieve_ = (fun e x ->
 292     hw_reg_retrieve (Obj.magic e) I8051.RegisterB);
 293     Joint_semantics.accb_arg_retrieve_ = (fun e x ->
 294     hw_reg_retrieve (Obj.magic e) I8051.RegisterB);
 295     Joint_semantics.dpl_store_ = (fun x ->
 296     Obj.magic (hw_reg_store I8051.RegisterDPL));
 297     Joint_semantics.dpl_retrieve_ = (fun e x ->
 298     hw_reg_retrieve (Obj.magic e) I8051.RegisterDPL);
 299     Joint_semantics.dpl_arg_retrieve_ = (fun e x ->
 300     hw_reg_retrieve (Obj.magic e) I8051.RegisterDPL);
 301     Joint_semantics.dph_store_ = (fun x ->
 302     Obj.magic (hw_reg_store I8051.RegisterDPH));
 303     Joint_semantics.dph_retrieve_ = (fun e x ->
 304     hw_reg_retrieve (Obj.magic e) I8051.RegisterDPH);
 305     Joint_semantics.dph_arg_retrieve_ = (fun e x ->
 306     hw_reg_retrieve (Obj.magic e) I8051.RegisterDPH);
 307     Joint_semantics.snd_arg_retrieve_ = (Obj.magic hw_arg_retrieve);
 308     Joint_semantics.pair_reg_move_ = (Obj.magic eval_registers_move);
 309     Joint_semantics.save_frame = (Obj.magic lTL_LIN_save_frame);
 310     Joint_semantics.setup_call = (fun x x0 x1 st ->
 311     Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
 312     Joint_semantics.fetch_external_args =
 313     (Obj.magic ltl_lin_fetch_external_args); Joint_semantics.set_result =
 314     (Obj.magic ltl_lin_set_result); Joint_semantics.call_args_for_main =
 315     (Obj.magic Nat.O); Joint_semantics.call_dest_for_main =
 316     (Obj.magic Types.It); Joint_semantics.read_result = (fun x x0 x1 st ->
 317     Obj.magic
 318       (Monad.m_return0 (Monad.max_def Errors.res0)
 319         (List.map
 320           (SemanticsUtils.hwreg_retrieve (Obj.magic st.Joint_semantics.regs))
 321           I8051.registerRets))); Joint_semantics.eval_ext_seq =
 322     (Obj.magic eval_LTL_LIN_ext_seq); Joint_semantics.pop_frame =
 323     (fun x x0 x1 x2 st -> Joint_semantics.pop_ra lTL_LIN_state st) }
 324