Changeset 2905


Ignore:
Timestamp:
Mar 19, 2013, 8:42:43 AM (4 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.

Files:
13 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCosts.ml

    r2890 r2905  
    115115open Interpret
    116116
    117 (** val aSM_abstract_status :
     117(** val oC_abstract_status :
    118118    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    119119    BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status **)
    120 let aSM_abstract_status code_memory cost_labels =
     120let oC_abstract_status code_memory cost_labels =
    121121  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
    122122    StructuredTraces.as_pc_of =
    123123    (Obj.magic (Status.program_counter code_memory));
    124124    StructuredTraces.as_classify =
    125     (Obj.magic (AbstractStatus.aSM_classify code_memory));
     125    (Obj.magic (AbstractStatus.oC_classify code_memory));
    126126    StructuredTraces.as_label_of_pc = (fun pc ->
    127127    BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    140140let trace_any_label_length code_memory cost_labels trace_ends_flag start_status final_status the_trace =
    141141  StructuredTraces.as_trace_any_label_length'
    142     (aSM_abstract_status code_memory cost_labels) trace_ends_flag
     142    (oC_abstract_status code_memory cost_labels) trace_ends_flag
    143143    (Obj.magic start_status) (Obj.magic final_status) the_trace
    144144
  • extracted/aSMCosts.mli

    r2773 r2905  
    115115open Interpret
    116116
    117 val aSM_abstract_status :
     117val oC_abstract_status :
    118118  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    119119  BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status
  • extracted/aSMCostsSplit.ml

    r2773 r2905  
    182182  Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
    183183    (StructuredTraces.as_cost_get_label
    184       (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.ASM.oc)
     184      (ASMCosts.oC_abstract_status (Fetch.load_code_memory p.ASM.oc)
    185185        p.ASM.costlabels) l_sig))
    186186
  • extracted/abstractStatus.ml

    r2773 r2905  
    190190      Nat.O)))))))))))))))))
    191191
    192 (** val aSM_classify :
     192(** val oC_classify :
    193193    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
    194194    StructuredTraces.status_class **)
    195 let aSM_classify code_memory s =
     195let oC_classify code_memory s =
    196196  aSM_classify0 (current_instruction code_memory s)
    197197
  • extracted/abstractStatus.mli

    r2773 r2905  
    128128val word_deqset : Deqsets.deqSet
    129129
    130 val aSM_classify :
     130val oC_classify :
    131131  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
    132132  StructuredTraces.status_class
  • 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
  • extracted/assembly.mli

    r2773 r2905  
    164164  (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0
    165165
     166val ticks_of_instruction : ASM.instruction -> Nat.nat
     167
     168val ticks_of0 :
     169  ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
     170  (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
     171  BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod
     172
     173val ticks_of :
     174  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     175  (BitVector.word -> Bool.bool) -> BitVector.word -> (Nat.nat, Nat.nat)
     176  Types.prod
     177
  • extracted/compiler.ml

    r2904 r2905  
    543543  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
    544544  in
    545   let { Types.fst = eta2; Types.snd = max_stack } =
     545  let { Types.fst = eta29116; Types.snd = max_stack } =
    546546    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    547547  in
    548   let { Types.fst = p3; Types.snd = stack_cost } = eta2 in
     548  let { Types.fst = p3; Types.snd = stack_cost } = eta29116 in
    549549  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
    550550  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
     
    558558        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
    559559          (LINToASM.lin_to_asm p4))) (fun p5 ->
    560       let i5 = observe Assembly_pass p5 in
    561560      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
    562561        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
     
    578577    Errors.res **)
    579578let assembler observe p =
    580 prerr_endline "ASSEMBLY0";
    581579  Obj.magic
    582580    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    584582        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
    585583          (Policy.jump_expansion' p))) (fun sigma_pol ->
    586 prerr_endline "ASSEMBLY1";
    587584      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
    588585      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
     586      let i =
     587        Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
     588          Types.snd = sigma }; Types.snd = pol }
     589      in
    589590      let p0 = Assembly.assembly p sigma pol in
    590       let i = Obj.magic observe Object_code_pass (Types.pi1 p0) in
    591 prerr_endline "ASSEMBLY2";
     591      let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
    592592      Obj.magic (Errors.OK (Types.pi1 p0))))
    593593
     
    626626    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    627627    compiler_output -> 'a1 **)
    628 let rec compiler_output_rect_Type4 h_mk_compiler_output x_198 =
     628let rec compiler_output_rect_Type4 h_mk_compiler_output x_25390 =
    629629  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    630630    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    631     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_198
     631    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25390
    632632  in
    633633  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    638638    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    639639    compiler_output -> 'a1 **)
    640 let rec compiler_output_rect_Type5 h_mk_compiler_output x_200 =
     640let rec compiler_output_rect_Type5 h_mk_compiler_output x_25392 =
    641641  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    642642    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    643     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_200
     643    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25392
    644644  in
    645645  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    650650    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    651651    compiler_output -> 'a1 **)
    652 let rec compiler_output_rect_Type3 h_mk_compiler_output x_202 =
     652let rec compiler_output_rect_Type3 h_mk_compiler_output x_25394 =
    653653  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    654654    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    655     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_202
     655    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25394
    656656  in
    657657  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    662662    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    663663    compiler_output -> 'a1 **)
    664 let rec compiler_output_rect_Type2 h_mk_compiler_output x_204 =
     664let rec compiler_output_rect_Type2 h_mk_compiler_output x_25396 =
    665665  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    666666    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    667     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_204
     667    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25396
    668668  in
    669669  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    674674    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    675675    compiler_output -> 'a1 **)
    676 let rec compiler_output_rect_Type1 h_mk_compiler_output x_206 =
     676let rec compiler_output_rect_Type1 h_mk_compiler_output x_25398 =
    677677  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    678678    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    679     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_206
     679    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25398
    680680  in
    681681  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    686686    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    687687    compiler_output -> 'a1 **)
    688 let rec compiler_output_rect_Type0 h_mk_compiler_output x_208 =
     688let rec compiler_output_rect_Type0 h_mk_compiler_output x_25400 =
    689689  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    690690    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    691     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_208
     691    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25400
    692692  in
    693693  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
  • extracted/interpret2.ml

    r2880 r2905  
    165165  let cm = Fetch.load_code_memory c.ASM.oc in
    166166  mk_preclassified_system_of_abstract_status
    167     (ASMCosts.aSM_abstract_status cm c.ASM.costlabels) (fun st ->
     167    (ASMCosts.oC_abstract_status cm c.ASM.costlabels) (fun st ->
    168168    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
    169169      (Interpret.execute_1 (Fetch.load_code_memory c.ASM.oc) (Obj.magic st)))
    170170    (Obj.magic (Status.initialise_status cm))
    171171
     172open Assembly
     173
     174(** val execute_1_pseudo_instruction' :
     175    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     176    (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
     177    Status.pseudoStatus **)
     178let execute_1_pseudo_instruction' cm sigma policy status =
     179  Interpret.execute_1_pseudo_instruction cm (fun x _ ->
     180    Assembly.ticks_of cm sigma policy x) status
     181
     182(** val classify_pseudo_instruction :
     183    ASM.pseudo_instruction -> StructuredTraces.status_class **)
     184let classify_pseudo_instruction = function
     185| ASM.Instruction pre -> AbstractStatus.aSM_classify00 pre
     186| ASM.Comment x -> StructuredTraces.Cl_other
     187| ASM.Cost x -> StructuredTraces.Cl_other
     188| ASM.Jmp x -> StructuredTraces.Cl_other
     189| ASM.Jnz (x, x0, x1) -> StructuredTraces.Cl_jump
     190| ASM.MovSuccessor (x, x0, x1) -> StructuredTraces.Cl_other
     191| ASM.Call x -> StructuredTraces.Cl_call
     192| ASM.Mov (x, x0) -> StructuredTraces.Cl_other
     193
     194(** val aSM_classify :
     195    ASM.pseudo_assembly_program -> Status.pseudoStatus ->
     196    StructuredTraces.status_class **)
     197let aSM_classify cm s =
     198  classify_pseudo_instruction
     199    (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst
     200
     201(** val aSM_as_label_of_pc :
     202    ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
     203    Types.option **)
     204let aSM_as_label_of_pc prog pc =
     205  match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
     206  | ASM.Instruction x -> Types.None
     207  | ASM.Comment x -> Types.None
     208  | ASM.Cost label -> Types.Some label
     209  | ASM.Jmp x -> Types.None
     210  | ASM.Jnz (x, x0, x1) -> Types.None
     211  | ASM.MovSuccessor (x, x0, x1) -> Types.None
     212  | ASM.Call x -> Types.None
     213  | ASM.Mov (x, x0) -> Types.None
     214
     215(** val aSM_abstract_status :
     216    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     217    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
     218let aSM_abstract_status prog sigma policy =
     219  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
     220    StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
     221    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
     222    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
     223    StructuredTraces.as_result = (fun x -> Types.None);
     224    StructuredTraces.as_call_ident = (fun x -> Positive.One
     225    (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
     226    assert false (* absurd case *)) }
     227
     228(** val aSM_preclassified_system :
     229    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     230    (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
     231let aSM_preclassified_system c sigma policy =
     232  mk_preclassified_system_of_abstract_status
     233    (aSM_abstract_status c sigma policy) (fun st ->
     234    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
     235      (execute_1_pseudo_instruction' c sigma policy (Obj.magic st)))
     236    (Obj.magic (Status.initialise_status c))
     237
  • extracted/interpret2.mli

    r2880 r2905  
    138138  ASM.labelled_object_code -> Measurable.preclassified_system
    139139
     140open Assembly
     141
     142val execute_1_pseudo_instruction' :
     143  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     144  (BitVector.word -> Bool.bool) -> Status.pseudoStatus -> Status.pseudoStatus
     145
     146val classify_pseudo_instruction :
     147  ASM.pseudo_instruction -> StructuredTraces.status_class
     148
     149val aSM_classify :
     150  ASM.pseudo_assembly_program -> Status.pseudoStatus ->
     151  StructuredTraces.status_class
     152
     153val aSM_as_label_of_pc :
     154  ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
     155  Types.option
     156
     157val aSM_abstract_status :
     158  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     159  (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status
     160
     161val aSM_preclassified_system :
     162  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     163  (BitVector.word -> Bool.bool) -> Measurable.preclassified_system
     164
  • extracted/semantics.ml

    r2902 r2905  
    447447  (fun x ->
    448448    Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
    449 | Compiler.Assembly_pass -> (Obj.magic ()) (*CSC: dummy, not used yet*)
     449| Compiler.Assembly_pass ->
     450  (fun prog ->
     451    let { Types.fst = eta32145; Types.snd = policy } = Obj.magic prog in
     452    let { Types.fst = code; Types.snd = sigma } = eta32145 in
     453    Interpret2.aSM_preclassified_system code sigma policy)
    450454| Compiler.Object_code_pass ->
    451455  (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))
     
    457461    Types.unit0 **)
    458462let run_and_print pass prog n print_pass print_event print_error print_exit =
    459   (*CSC: temporary until Assembly implemented *)
    460   if pass = Assembly_pass then print_error List.Nil else
    461463  let pcs = preclassified_system_of_pass pass prog in
    462464  let prog0 = prog in
  • src/ASM/Interpret2.ma

    r2899 r2905  
    122122 λc,sigma,policy.
    123123  mk_preclassified_system_of_abstract_status
    124    pseudo_assembly_program
     124   (pseudo_assembly_program × (Word → Word) × (Word → bool))
    125125   (ASM_abstract_status c sigma policy)
    126126   (λst. return (execute_1_pseudo_instruction' … sigma policy st))
  • src/semantics.ma

    r2899 r2905  
    4040  | assembly_pass ⇒
    4141     λprog. let 〈code,sigma,policy〉 ≝ prog in
    42       mk_preclassified_system_pass … (ASM_preclassified_system prog sigma policy) …
     42      mk_preclassified_system_pass … (ASM_preclassified_system code sigma policy) …
    4343  | object_code_pass ⇒
    4444     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
Note: See TracChangeset for help on using the changeset viewer.