Changeset 2905 for extracted/assembly.ml
 Timestamp:
 Mar 19, 2013, 8:42:43 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/assembly.ml
r2777 r2905 2852 2852 (sigma (lookup_labels p.ASM.final_label)) })) __)) __ 2853 2853 2854 (** val ticks_of_instruction : ASM.instruction > Nat.nat **) 2855 let 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 **) 2867 let 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 **) 3218 let 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.