extracted/eRTL_semantics.ml

   1 open Preamble
   2
   3 open ExtraMonads
   4
   5 open Deqsets_extra
   6
   7 open State
   8
   9 open Bind_new
  10
  11 open BindLists
  12
  13 open Blocks
  14
  15 open TranslateUtils
  16
  17 open ExtraGlobalenvs
  18
  19 open I8051bis
  20
  21 open String
  22
  23 open Sets
  24
  25 open Listb
  26
  27 open LabelledObjects
  28
  29 open BitVectorTrie
  30
  31 open Graphs
  32
  33 open I8051
  34
  35 open Order
  36
  37 open Registers
  38
  39 open BackEndOps
  40
  41 open Joint
  42
  43 open BEMem
  44
  45 open CostLabel
  46
  47 open Events
  48
  49 open IOMonad
  50
  51 open IO
  52
  53 open Extra_bool
  54
  55 open Coqlib
  56
  57 open Values
  58
  59 open FrontEndVal
  60
  61 open Hide
  62
  63 open ByteValues
  64
  65 open Division
  66
  67 open Z
  68
  69 open BitVectorZ
  70
  71 open Pointers
  72
  73 open GenMem
  74
  75 open FrontEndMem
  76
  77 open Proper
  78
  79 open PositiveMap
  80
  81 open Deqsets
  82
  83 open Extralib
  84
  85 open Lists
  86
  87 open Identifiers
  88
  89 open Exp
  90
  91 open Arithmetic
  92
  93 open Vector
  94
  95 open Div_and_mod
  96
  97 open Util
  98
  99 open FoldStuff
 100
 101 open BitVector
 102
 103 open Extranat
 104
 105 open Integers
 106
 107 open AST
 108
 109 open ErrorMessages
 110
 111 open Option
 112
 113 open Setoids
 114
 115 open Monad
 116
 117 open Jmeq
 118
 119 open Russell
 120
 121 open Positive
 122
 123 open PreIdentifiers
 124
 125 open Bool
 126
 127 open Relations
 128
 129 open Nat
 130
 131 open List
 132
 133 open Hints_declaration
 134
 135 open Core_notation
 136
 137 open Pts
 138
 139 open Logic
 140
 141 open Types
 142
 143 open Errors
 144
 145 open Globalenvs
 146
 147 open Joint_semantics
 148
 149 open SemanticsUtils
 150
 151 open ERTL
 152
 153 type ertl_reg_env =
 154   (ByteValues.beval Registers.register_env, SemanticsUtils.hw_register_env)
 155   Types.prod
 156
 157 (** val ps_reg_store :
 158     PreIdentifiers.identifier -> ByteValues.beval -> ertl_reg_env ->
 159     (ByteValues.beval Identifiers.identifier_map,
 160     SemanticsUtils.hw_register_env) Types.prod Errors.res **)
 161 let ps_reg_store r v local_env =
 162   let res = SemanticsUtils.reg_store r v local_env.Types.fst in
 163   Errors.OK { Types.fst = res; Types.snd = local_env.Types.snd }
 164
 165 (** val ps_reg_retrieve :
 166     ertl_reg_env -> Registers.register -> ByteValues.beval Errors.res **)
 167 let ps_reg_retrieve local_env =
 168   SemanticsUtils.reg_retrieve local_env.Types.fst
 169
 170 (** val hw_reg_store :
 171     I8051.register -> ByteValues.beval -> ertl_reg_env -> (ByteValues.beval
 172     Registers.register_env, SemanticsUtils.hw_register_env) Types.prod
 173     Errors.res **)
 174 let hw_reg_store r v local_env =
 175   Errors.OK { Types.fst = local_env.Types.fst; Types.snd =
 176     (SemanticsUtils.hwreg_store r v local_env.Types.snd) }
 177
 178 (** val hw_reg_retrieve :
 179     ertl_reg_env -> I8051.register -> ByteValues.beval Errors.res **)
 180 let hw_reg_retrieve local_env reg =
 181   Errors.OK (SemanticsUtils.hwreg_retrieve local_env.Types.snd reg)
 182
 183 (** val ps_arg_retrieve :
 184     ertl_reg_env -> Registers.register Joint.argument -> ByteValues.beval
 185     Errors.res **)
 186 let ps_arg_retrieve local_env = function
 187 | Joint.Reg r -> ps_reg_retrieve local_env r
 188 | Joint.Imm b ->
 189   Obj.magic
 190     (Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte b))
 191
 192 (** val get_hwsp : ertl_reg_env -> ByteValues.xpointer Errors.res **)
 193 let get_hwsp st =
 194   SemanticsUtils.hwreg_retrieve_sp st.Types.snd
 195
 196 (** val set_hwsp : ertl_reg_env -> ByteValues.xpointer -> ertl_reg_env **)
 197 let set_hwsp st sp =
 198   { Types.fst = st.Types.fst; Types.snd =
 199     (SemanticsUtils.hwreg_store_sp st.Types.snd sp) }
 200
 201 (** val eRTL_state : Joint_semantics.sem_state_params **)
 202 let eRTL_state =
 203   { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
 204     Joint_semantics.empty_regsT = (fun sp ->
 205     Obj.magic { Types.fst =
 206       (Identifiers.empty_map PreIdentifiers.RegisterTag); Types.snd =
 207       (SemanticsUtils.init_hw_register_env sp) }); Joint_semantics.load_sp =
 208     (Obj.magic get_hwsp); Joint_semantics.save_sp = (Obj.magic set_hwsp) }
 209
 210 (** val ertl_eval_move :
 211     ertl_reg_env -> (ERTL.move_dst, ERTL.move_dst Joint.argument) Types.prod
 212     -> __ **)
 213 let ertl_eval_move env pr =
 214   Monad.m_bind0 (Monad.max_def Errors.res0)
 215     (match pr.Types.snd with
 216      | Joint.Reg src ->
 217        (match src with
 218         | ERTL.PSD r -> Obj.magic (ps_reg_retrieve env r)
 219         | ERTL.HDW r -> Obj.magic (hw_reg_retrieve env r))
 220      | Joint.Imm b ->
 221        Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte b))
 222     (fun v ->
 223     match pr.Types.fst with
 224     | ERTL.PSD r -> Obj.magic (ps_reg_store r v env)
 225     | ERTL.HDW r -> Obj.magic (hw_reg_store r v env))
 226
 227 (** val ertl_allocate_local :
 228     PreIdentifiers.identifier -> ertl_reg_env -> (ByteValues.beval
 229     Identifiers.identifier_map, SemanticsUtils.hw_register_env) Types.prod **)
 230 let ertl_allocate_local reg lenv =
 231   { Types.fst =
 232     (Identifiers.add PreIdentifiers.RegisterTag lenv.Types.fst reg
 233       ByteValues.BVundef); Types.snd = lenv.Types.snd }
 234
 235 (** val ertl_save_frame :
 236     Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
 237     Joint_semantics.state Errors.res **)
 238 let ertl_save_frame x x0 st =
 239   Obj.magic
 240     (Monad.m_bind0 (Monad.max_def Errors.res0)
 241       (Obj.magic
 242         (Joint_semantics.push_ra eRTL_state st.Joint_semantics.st_no_pc
 243           st.Joint_semantics.pc)) (fun st' ->
 244       Monad.m_bind0 (Monad.max_def Errors.res0)
 245         (Obj.magic
 246           (Errors.opt_to_res (List.Cons ((Errors.MSG
 247             ErrorMessages.FrameErrorOnPush), List.Nil))
 248             st'.Joint_semantics.st_frms)) (fun frms ->
 249         Monad.m_return0 (Monad.max_def Errors.res0)
 250           (Joint_semantics.set_frms eRTL_state
 251             (Obj.magic (List.Cons ({ Types.fst =
 252               (Obj.magic st'.Joint_semantics.regs).Types.fst; Types.snd =
 253               st.Joint_semantics.pc.ByteValues.pc_block }, frms)))
 254             (Joint_semantics.set_regs eRTL_state
 255               (Obj.magic { Types.fst =
 256                 (Identifiers.empty_map PreIdentifiers.RegisterTag);
 257                 Types.snd = (Obj.magic st'.Joint_semantics.regs).Types.snd })
 258               st')))))
 259
 260 (** val ertl_pop_frame :
 261     Joint_semantics.state -> (Joint_semantics.state,
 262     ByteValues.program_counter) Types.prod Errors.res **)
 263 let ertl_pop_frame st =
 264   Obj.magic
 265     (Monad.m_bind0 (Monad.max_def Errors.res0)
 266       (Obj.magic
 267         (Errors.opt_to_res (List.Cons ((Errors.MSG
 268           ErrorMessages.FrameErrorOnPop), List.Nil))
 269           st.Joint_semantics.st_frms)) (fun frms ->
 270       match frms with
 271       | List.Nil ->
 272         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 273           ErrorMessages.FramesEmptyOnPop), List.Nil)))
 274       | List.Cons (hd, tl) ->
 275         let { Types.fst = local_mem; Types.snd = bl } = hd in
 276         let st' =
 277           Joint_semantics.set_regs eRTL_state
 278             (Obj.magic { Types.fst = local_mem; Types.snd =
 279               (Obj.magic st.Joint_semantics.regs).Types.snd })
 280             (Joint_semantics.set_frms eRTL_state (Obj.magic tl) st)
 281         in
 282         Monad.m_bind2 (Monad.max_def Errors.res0)
 283           (Obj.magic (Joint_semantics.pop_ra eRTL_state st')) (fun st'' pc ->
 284           match Pointers.eq_block (Types.pi1 bl)
 285                   (Types.pi1 pc.ByteValues.pc_block) with
 286           | Bool.True ->
 287             Obj.magic (Errors.OK { Types.fst = st''; Types.snd = pc })
 288           | Bool.False ->
 289             Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 290               ErrorMessages.BlockInFramesCorrupted), List.Nil))))))
 291
 292 (** val ertl_fetch_external_args :
 293     AST.external_function -> Joint_semantics.state -> __ -> Values.val0
 294     List.list Errors.res **)
 295 let ertl_fetch_external_args _ =
 296   failwith "AXIOM TO BE REALIZED"
 297
 298 (** val ertl_set_result :
 299     Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
 300     Joint_semantics.state Errors.res **)
 301 let ertl_set_result _ =
 302   failwith "AXIOM TO BE REALIZED"
 303
 304 (** val ps_reg_store_status :
 305     Registers.register -> ByteValues.beval -> Joint_semantics.state ->
 306     Joint_semantics.state Errors.res **)
 307 let ps_reg_store_status dst v st =
 308   let env = st.Joint_semantics.regs in
 309   Obj.magic
 310     (Monad.m_bind0 (Monad.max_def Errors.res0)
 311       (Obj.magic (ps_reg_store dst v (Obj.magic env))) (fun env' ->
 312       Monad.m_return0 (Monad.max_def Errors.res0)
 313         (Joint_semantics.set_regs eRTL_state env' st)))
 314
 315 (** val eval_ertl_seq :
 316     AST.ident List.list -> 'a1 Joint_semantics.genv_gen -> ERTL.ertl_seq ->
 317     AST.ident -> Joint_semantics.state -> Joint_semantics.state Errors.res **)
 318 let eval_ertl_seq globals ge stm id st =
 319   Obj.magic
 320     (Monad.m_bind0 (Monad.max_def Errors.res0)
 321       (Obj.magic
 322         (Errors.opt_to_res (Errors.msg ErrorMessages.FunctionNotFound)
 323           (ge.Joint_semantics.stack_sizes id))) (fun framesize ->
 324       let framesize0 =
 325         Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 326           (Nat.S (Nat.S Nat.O)))))))) framesize
 327       in
 328       (match stm with
 329        | ERTL.Ertl_new_frame ->
 330          Monad.m_bind0 (Monad.max_def Errors.res0)
 331            (Obj.magic (Joint_semantics.sp eRTL_state st)) (fun sp ->
 332            let newsp =
 333              Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 334                (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp) framesize0
 335            in
 336            Monad.m_return0 (Monad.max_def Errors.res0)
 337              (Joint_semantics.set_sp eRTL_state newsp st))
 338        | ERTL.Ertl_del_frame ->
 339          Monad.m_bind0 (Monad.max_def Errors.res0)
 340            (Obj.magic (Joint_semantics.sp eRTL_state st)) (fun sp ->
 341            let newsp =
 342              Pointers.shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 343                (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp) framesize0
 344            in
 345            Monad.m_return0 (Monad.max_def Errors.res0)
 346              (Joint_semantics.set_sp eRTL_state newsp st))
 347        | ERTL.Ertl_frame_size dst ->
 348          Obj.magic
 349            (ps_reg_store_status dst (ByteValues.BVByte framesize0) st))))
 350
 351 (** val eRTL_sem_uns : 'a1 Joint_semantics.sem_unserialized_params **)
 352 let eRTL_sem_uns =
 353   { Joint_semantics.st_pars = eRTL_state; Joint_semantics.acca_store_ =
 354     (Obj.magic ps_reg_store); Joint_semantics.acca_retrieve_ =
 355     (Obj.magic ps_reg_retrieve); Joint_semantics.acca_arg_retrieve_ =
 356     (Obj.magic ps_arg_retrieve); Joint_semantics.accb_store_ =
 357     (Obj.magic ps_reg_store); Joint_semantics.accb_retrieve_ =
 358     (Obj.magic ps_reg_retrieve); Joint_semantics.accb_arg_retrieve_ =
 359     (Obj.magic ps_arg_retrieve); Joint_semantics.dpl_store_ =
 360     (Obj.magic ps_reg_store); Joint_semantics.dpl_retrieve_ =
 361     (Obj.magic ps_reg_retrieve); Joint_semantics.dpl_arg_retrieve_ =
 362     (Obj.magic ps_arg_retrieve); Joint_semantics.dph_store_ =
 363     (Obj.magic ps_reg_store); Joint_semantics.dph_retrieve_ =
 364     (Obj.magic ps_reg_retrieve); Joint_semantics.dph_arg_retrieve_ =
 365     (Obj.magic ps_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
 366     (Obj.magic ps_arg_retrieve); Joint_semantics.pair_reg_move_ =
 367     (Obj.magic ertl_eval_move); Joint_semantics.save_frame =
 368     (Obj.magic ertl_save_frame); Joint_semantics.setup_call =
 369     (fun x x0 x1 st ->
 370     Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
 371     Joint_semantics.fetch_external_args = ertl_fetch_external_args;
 372     Joint_semantics.set_result = (Obj.magic ertl_set_result);
 373     Joint_semantics.call_args_for_main = (Obj.magic Nat.O);
 374     Joint_semantics.call_dest_for_main = (Obj.magic Types.It);
 375     Joint_semantics.read_result = (fun x x0 x1 st ->
 376     Obj.magic
 377       (Monad.m_return0 (Monad.max_def Errors.res0)
 378         (List.map
 379           (SemanticsUtils.hwreg_retrieve
 380             (Obj.magic st.Joint_semantics.regs).Types.snd)
 381           I8051.registerRets))); Joint_semantics.eval_ext_seq =
 382     (fun gl ge stm id -> eval_ertl_seq gl ge (Obj.magic stm) id);
 383     Joint_semantics.pop_frame = (fun x x0 x1 x2 -> ertl_pop_frame) }
 384
 385 (** val eRTL_semantics : SemanticsUtils.sem_graph_params **)
 386 let eRTL_semantics =
 387   { SemanticsUtils.sgp_pars =
 388     (Joint.gp_to_p__o__stmt_pars__o__uns_pars ERTL.eRTL);
 389     SemanticsUtils.sgp_sup = (fun _ -> eRTL_sem_uns);
 390     SemanticsUtils.graph_pre_main_generator = ERTL.eRTL_premain }
 391