Changeset 2905 for extracted/assembly.ml


Ignore:
Timestamp:
Mar 19, 2013, 8:42:43 AM (7 years ago)
Author:
sacerdot
Message:

Semantics of ASM in place (up to return values and function call names).
The test example badly diverges in ASM after being ok in LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/assembly.ml

    r2777 r2905  
    28522852  (sigma (lookup_labels p.ASM.final_label)) })) __)) __
    28532853
     2854(** val ticks_of_instruction : ASM.instruction -> Nat.nat **)
     2855let ticks_of_instruction i =
     2856  let trivial_code_memory = assembly1 i in
     2857  let trivial_status = Fetch.load_code_memory trivial_code_memory in
     2858  (Fetch.fetch trivial_status
     2859    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2860      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2861      Nat.O)))))))))))))))))).Types.snd
     2862
     2863(** val ticks_of0 :
     2864    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
     2865    (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
     2866    BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod **)
     2867let ticks_of0 program lookup_labels sigma policy ppc = function
     2868| ASM.Instruction instr ->
     2869  (match instr with
     2870   | ASM.ADD (arg1, arg2) ->
     2871     let ticks =
     2872       ticks_of_instruction (ASM.RealInstruction (ASM.ADD (arg1, arg2)))
     2873     in
     2874     { Types.fst = ticks; Types.snd = ticks }
     2875   | ASM.ADDC (arg1, arg2) ->
     2876     let ticks =
     2877       ticks_of_instruction (ASM.RealInstruction (ASM.ADDC (arg1, arg2)))
     2878     in
     2879     { Types.fst = ticks; Types.snd = ticks }
     2880   | ASM.SUBB (arg1, arg2) ->
     2881     let ticks =
     2882       ticks_of_instruction (ASM.RealInstruction (ASM.SUBB (arg1, arg2)))
     2883     in
     2884     { Types.fst = ticks; Types.snd = ticks }
     2885   | ASM.INC arg ->
     2886     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.INC arg)) in
     2887     { Types.fst = ticks; Types.snd = ticks }
     2888   | ASM.DEC arg ->
     2889     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DEC arg)) in
     2890     { Types.fst = ticks; Types.snd = ticks }
     2891   | ASM.MUL (arg1, arg2) ->
     2892     let ticks =
     2893       ticks_of_instruction (ASM.RealInstruction (ASM.MUL (arg1, arg2)))
     2894     in
     2895     { Types.fst = ticks; Types.snd = ticks }
     2896   | ASM.DIV (arg1, arg2) ->
     2897     let ticks =
     2898       ticks_of_instruction (ASM.RealInstruction (ASM.DIV (arg1, arg2)))
     2899     in
     2900     { Types.fst = ticks; Types.snd = ticks }
     2901   | ASM.DA arg ->
     2902     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DA arg)) in
     2903     { Types.fst = ticks; Types.snd = ticks }
     2904   | ASM.JC lbl ->
     2905     let lookup_address = sigma (lookup_labels lbl) in
     2906     let pc_plus_jmp_length =
     2907       sigma
     2908         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2909           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2910           Nat.O)))))))))))))))) ppc
     2911           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2912             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2913             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     2914     in
     2915     let { Types.fst = sj_possible; Types.snd = disp } =
     2916       short_jump_cond pc_plus_jmp_length lookup_address
     2917     in
     2918     (match sj_possible with
     2919      | Bool.True ->
     2920        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     2921          Nat.O)) }
     2922      | Bool.False ->
     2923        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     2924          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     2925   | ASM.JNC lbl ->
     2926     let lookup_address = sigma (lookup_labels lbl) in
     2927     let pc_plus_jmp_length =
     2928       sigma
     2929         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2930           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2931           Nat.O)))))))))))))))) ppc
     2932           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2933             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2934             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     2935     in
     2936     let { Types.fst = sj_possible; Types.snd = disp } =
     2937       short_jump_cond pc_plus_jmp_length lookup_address
     2938     in
     2939     (match sj_possible with
     2940      | Bool.True ->
     2941        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     2942          Nat.O)) }
     2943      | Bool.False ->
     2944        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     2945          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     2946   | ASM.JB (bit, lbl) ->
     2947     let lookup_address = sigma (lookup_labels lbl) in
     2948     let pc_plus_jmp_length =
     2949       sigma
     2950         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2951           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2952           Nat.O)))))))))))))))) ppc
     2953           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2954             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2955             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     2956     in
     2957     let { Types.fst = sj_possible; Types.snd = disp } =
     2958       short_jump_cond pc_plus_jmp_length lookup_address
     2959     in
     2960     (match sj_possible with
     2961      | Bool.True ->
     2962        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     2963          Nat.O)) }
     2964      | Bool.False ->
     2965        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     2966          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     2967   | ASM.JNB (bit, lbl) ->
     2968     let lookup_address = sigma (lookup_labels lbl) in
     2969     let pc_plus_jmp_length =
     2970       sigma
     2971         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2972           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2973           Nat.O)))))))))))))))) ppc
     2974           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2975             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2976             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     2977     in
     2978     let { Types.fst = sj_possible; Types.snd = disp } =
     2979       short_jump_cond pc_plus_jmp_length lookup_address
     2980     in
     2981     (match sj_possible with
     2982      | Bool.True ->
     2983        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     2984          Nat.O)) }
     2985      | Bool.False ->
     2986        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     2987          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     2988   | ASM.JBC (bit, lbl) ->
     2989     let lookup_address = sigma (lookup_labels lbl) in
     2990     let pc_plus_jmp_length =
     2991       sigma
     2992         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2993           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2994           Nat.O)))))))))))))))) ppc
     2995           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2996             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2997             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     2998     in
     2999     let { Types.fst = sj_possible; Types.snd = disp } =
     3000       short_jump_cond pc_plus_jmp_length lookup_address
     3001     in
     3002     (match sj_possible with
     3003      | Bool.True ->
     3004        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     3005          Nat.O)) }
     3006      | Bool.False ->
     3007        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     3008          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     3009   | ASM.JZ lbl ->
     3010     let lookup_address = sigma (lookup_labels lbl) in
     3011     let pc_plus_jmp_length =
     3012       sigma
     3013         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3014           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3015           Nat.O)))))))))))))))) ppc
     3016           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3017             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3018             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     3019     in
     3020     let { Types.fst = sj_possible; Types.snd = disp } =
     3021       short_jump_cond pc_plus_jmp_length lookup_address
     3022     in
     3023     (match sj_possible with
     3024      | Bool.True ->
     3025        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     3026          Nat.O)) }
     3027      | Bool.False ->
     3028        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     3029          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     3030   | ASM.JNZ lbl ->
     3031     let lookup_address = sigma (lookup_labels lbl) in
     3032     let pc_plus_jmp_length =
     3033       sigma
     3034         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3035           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3036           Nat.O)))))))))))))))) ppc
     3037           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3038             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3039             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     3040     in
     3041     let { Types.fst = sj_possible; Types.snd = disp } =
     3042       short_jump_cond pc_plus_jmp_length lookup_address
     3043     in
     3044     (match sj_possible with
     3045      | Bool.True ->
     3046        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     3047          Nat.O)) }
     3048      | Bool.False ->
     3049        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     3050          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     3051   | ASM.CJNE (arg, lbl) ->
     3052     let lookup_address = sigma (lookup_labels lbl) in
     3053     let pc_plus_jmp_length =
     3054       sigma
     3055         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3056           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3057           Nat.O)))))))))))))))) ppc
     3058           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3059             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3060             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     3061     in
     3062     let { Types.fst = sj_possible; Types.snd = disp } =
     3063       short_jump_cond pc_plus_jmp_length lookup_address
     3064     in
     3065     (match sj_possible with
     3066      | Bool.True ->
     3067        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     3068          Nat.O)) }
     3069      | Bool.False ->
     3070        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     3071          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     3072   | ASM.DJNZ (arg, lbl) ->
     3073     let lookup_address = sigma (lookup_labels lbl) in
     3074     let pc_plus_jmp_length =
     3075       sigma
     3076         (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3077           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3078           Nat.O)))))))))))))))) ppc
     3079           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3080             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3081             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     3082     in
     3083     let { Types.fst = sj_possible; Types.snd = disp } =
     3084       short_jump_cond pc_plus_jmp_length lookup_address
     3085     in
     3086     (match sj_possible with
     3087      | Bool.True ->
     3088        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     3089          Nat.O)) }
     3090      | Bool.False ->
     3091        { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
     3092          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
     3093   | ASM.ANL arg ->
     3094     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ANL arg)) in
     3095     { Types.fst = ticks; Types.snd = ticks }
     3096   | ASM.ORL arg ->
     3097     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ORL arg)) in
     3098     { Types.fst = ticks; Types.snd = ticks }
     3099   | ASM.XRL arg ->
     3100     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.XRL arg)) in
     3101     { Types.fst = ticks; Types.snd = ticks }
     3102   | ASM.CLR arg ->
     3103     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.CLR arg)) in
     3104     { Types.fst = ticks; Types.snd = ticks }
     3105   | ASM.CPL arg ->
     3106     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.CPL arg)) in
     3107     { Types.fst = ticks; Types.snd = ticks }
     3108   | ASM.RL arg ->
     3109     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RL arg)) in
     3110     { Types.fst = ticks; Types.snd = ticks }
     3111   | ASM.RLC arg ->
     3112     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RLC arg)) in
     3113     { Types.fst = ticks; Types.snd = ticks }
     3114   | ASM.RR arg ->
     3115     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RR arg)) in
     3116     { Types.fst = ticks; Types.snd = ticks }
     3117   | ASM.RRC arg ->
     3118     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RRC arg)) in
     3119     { Types.fst = ticks; Types.snd = ticks }
     3120   | ASM.SWAP arg ->
     3121     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SWAP arg)) in
     3122     { Types.fst = ticks; Types.snd = ticks }
     3123   | ASM.MOV arg ->
     3124     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MOV arg)) in
     3125     { Types.fst = ticks; Types.snd = ticks }
     3126   | ASM.MOVX arg ->
     3127     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MOVX arg)) in
     3128     { Types.fst = ticks; Types.snd = ticks }
     3129   | ASM.SETB arg ->
     3130     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SETB arg)) in
     3131     { Types.fst = ticks; Types.snd = ticks }
     3132   | ASM.PUSH arg ->
     3133     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.PUSH arg)) in
     3134     { Types.fst = ticks; Types.snd = ticks }
     3135   | ASM.POP arg ->
     3136     let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.POP arg)) in
     3137     { Types.fst = ticks; Types.snd = ticks }
     3138   | ASM.XCH (arg1, arg2) ->
     3139     let ticks =
     3140       ticks_of_instruction (ASM.RealInstruction (ASM.XCH (arg1, arg2)))
     3141     in
     3142     { Types.fst = ticks; Types.snd = ticks }
     3143   | ASM.XCHD (arg1, arg2) ->
     3144     let ticks =
     3145       ticks_of_instruction (ASM.RealInstruction (ASM.XCHD (arg1, arg2)))
     3146     in
     3147     { Types.fst = ticks; Types.snd = ticks }
     3148   | ASM.RET ->
     3149     let ticks = ticks_of_instruction (ASM.RealInstruction ASM.RET) in
     3150     { Types.fst = ticks; Types.snd = ticks }
     3151   | ASM.RETI ->
     3152     let ticks = ticks_of_instruction (ASM.RealInstruction ASM.RETI) in
     3153     { Types.fst = ticks; Types.snd = ticks }
     3154   | ASM.NOP ->
     3155     let ticks = ticks_of_instruction (ASM.RealInstruction ASM.NOP) in
     3156     { Types.fst = ticks; Types.snd = ticks }
     3157   | ASM.JMP x -> assert false (* absurd case *))
     3158| ASM.Comment comment -> { Types.fst = Nat.O; Types.snd = Nat.O }
     3159| ASM.Cost cost -> { Types.fst = Nat.O; Types.snd = Nat.O }
     3160| ASM.Jmp jmp ->
     3161  let pc_plus_jmp_length =
     3162    sigma
     3163      (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3164        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3165        Nat.O)))))))))))))))) ppc
     3166        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3167          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3168          (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     3169  in
     3170  let do_a_long = policy ppc in
     3171  let lookup_address = sigma (lookup_labels jmp) in
     3172  let { Types.fst = sj_possible; Types.snd = disp } =
     3173    short_jump_cond pc_plus_jmp_length lookup_address
     3174  in
     3175  (match Bool.andb sj_possible (Bool.notb do_a_long) with
     3176   | Bool.True ->
     3177     { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
     3178   | Bool.False ->
     3179     let { Types.fst = mj_possible; Types.snd = disp2 } =
     3180       absolute_jump_cond pc_plus_jmp_length lookup_address
     3181     in
     3182     (match Bool.andb mj_possible (Bool.notb do_a_long) with
     3183      | Bool.True ->
     3184        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     3185          Nat.O)) }
     3186      | Bool.False ->
     3187        { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
     3188          Nat.O)) }))
     3189| ASM.Jnz (x, x0, x1) -> assert false (* absurd case *)
     3190| ASM.MovSuccessor (x, x0, x1) -> assert false (* absurd case *)
     3191| ASM.Call call ->
     3192  let pc_plus_jmp_length =
     3193    sigma
     3194      (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3195        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3196        Nat.O)))))))))))))))) ppc
     3197        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3198          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3199          (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
     3200  in
     3201  let lookup_address = sigma (lookup_labels call) in
     3202  let { Types.fst = mj_possible; Types.snd = disp } =
     3203    absolute_jump_cond pc_plus_jmp_length lookup_address
     3204  in
     3205  let do_a_long = policy ppc in
     3206  (match Bool.andb mj_possible (Bool.notb do_a_long) with
     3207   | Bool.True ->
     3208     { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
     3209   | Bool.False ->
     3210     { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) })
     3211| ASM.Mov (dptr, tgt) ->
     3212  { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
     3213
     3214(** val ticks_of :
     3215    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     3216    (BitVector.word -> Bool.bool) -> BitVector.word -> (Nat.nat, Nat.nat)
     3217    Types.prod **)
     3218let ticks_of program sigma policy ppc =
     3219  let { Types.fst = labels; Types.snd = costs } =
     3220    Fetch.create_label_cost_map program.ASM.code
     3221  in
     3222  let addr_of = fun id ->
     3223    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3224      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3225      Nat.O))))))))))))))))
     3226      (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
     3227  in
     3228  let { Types.fst = fetched; Types.snd = new_ppc } =
     3229    ASM.fetch_pseudo_instruction program.ASM.code ppc
     3230  in
     3231  ticks_of0 program addr_of sigma policy ppc fetched
     3232
Note: See TracChangeset for help on using the changeset viewer.