(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "ERTLptr/ERTLptr.ma".

(* This file is used only by untrusted code. We write it in Matita to
   benefit from the typing system *)

definition examine_internal:
 ∀globals. joint_internal_function ERTLptr globals →
  identifier_map RegisterTag Pos ≝
λglobals,fun.
 let incr ≝
  λr,map.
   match lookup RegisterTag Pos map r with
   [ None ⇒ add … map r one
   | Some v ⇒ add … map r (succ v) ] in
 let incr_arg ≝
  λarg,map.
   match arg with
   [ Imm _ ⇒ map
   | Reg r ⇒ incr r map ] in
 let f ≝
  λ_.λinstr.λmap.
   match instr with
   [ sequential s _ ⇒
      match s with
      [ COST_LABEL _ ⇒ map
      | CALL _ _ _ ⇒ map
      | COND r _ ⇒ incr r map
      | step_seq s ⇒
         match s with
         [ COMMENT _ ⇒ map
         | ADDRESS _ _ _ _ ⇒ map
         | CLEAR_CARRY ⇒ map
         | SET_CARRY ⇒ map
         | MOVE pair ⇒
            let 〈r1,r2〉 ≝ pair in
            let incr_dst ≝ λarg,map.
             match arg with
             [ PSD r ⇒ incr r map
             | HDW _ ⇒ map ] in
            incr_dst r1
             match r2 with
             [ Reg a ⇒ incr_dst a map
             | Imm _ ⇒ map ]
         | POP r ⇒ incr r map
         | PUSH r ⇒ incr_arg r map
         | OPACCS _ r1 r2 r3 r4 ⇒
            incr r1 (incr r2 (incr_arg r3 (incr_arg r4 map)))
         | OP1 _ r1 r2 ⇒ incr r1 (incr r2 map)
         | OP2 _ r1 r2 r3 ⇒ incr r1 (incr_arg r2 (incr_arg r3 map))
         | LOAD r1 _ _ ⇒ incr r1 map
         | STORE _ _ r ⇒ incr_arg r map
         | extension_seq s ⇒
            match s with
            [ ertlptr_ertl s ⇒
               match s with
               [ ertl_new_frame ⇒ map
               | ertl_del_frame ⇒ map
               | ertl_frame_size r ⇒ incr r map ]
            | LOW_ADDRESS r _ ⇒ incr r map
            | HIGH_ADDRESS r _ ⇒ incr r map ]]]
   | final _ ⇒ map
   | FCOND (abs : has_fcond ERTLptr) _ _ _ ⇒ Ⓧabs ]
 in
 foldi … f (joint_if_code … fun) (empty_map …).