Changeset 1581 for src/ASM


Ignore:
Timestamp:
Dec 1, 2011, 3:15:15 PM (8 years ago)
Author:
mulligan
Message:

Dangling de Bruijn pointer when trying to propagate russell to set_arg_1

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1579 r1581  
    374374  ].
    375375qed.
    376    
    377 let rec compute_max_trace_label_label_cost_is_ok
    378   (cost_labels: BitVectorTrie costlabel 16)
    379    (trace_ends_flag: trace_ends_with_ret)
    380     (start_status: Status) (final_status: Status)
    381       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    382         start_status final_status) on the_trace:
    383           And (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    384             (clock … final_status) - (clock … start_status)) (clock … start_status ≤ clock … final_status) ≝ ?
    385 and compute_max_trace_any_label_cost_is_ok
    386   (cost_labels: BitVectorTrie costlabel 16)
    387   (trace_ends_flag: trace_ends_with_ret)
    388    (start_status: Status) (final_status: Status)
    389      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    390        on the_trace:
    391          (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    392            (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?
    393 and compute_max_trace_label_return_cost_is_ok
    394   (cost_labels: BitVectorTrie costlabel 16)
    395   (start_status: Status) (final_status: Status)
    396     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
    397       on the_trace:
    398         (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
    399           (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?.
    400   [1:
    401     cases the_trace
    402     #ends_flag #start_status #end_status #any_label_trace #is_costed
    403     normalize @compute_max_trace_any_label_cost_is_ok
    404   |2:
    405     cases the_trace
    406     [1:
    407       #start_status #final_status #is_next #is_not_return #is_costed
    408       change with (current_instruction_cost start_status) in ⊢ (?(??%?)?);
    409       cases(is_next)
    410       @conj
    411       cases(execute_1 start_status)
    412       #the_status #assm
    413       whd in match eject; normalize nodelta
    414       >assm
    415       [1:
    416         @minus_plus_m_m
    417       |2:
    418         @m_le_plus_n_m
    419       ]
    420     |2:
    421       #start_status #final_status #is_next #is_return
    422       change with (current_instruction_cost start_status) in ⊢ (?(??%?)?);
    423       cases(is_next)
    424       @conj
    425       cases(execute_1 start_status)
    426       #the_status #assm
    427       whd in match eject; normalize nodelta
    428       >assm
    429       [1:
    430         @minus_plus_m_m
    431       |2:
    432         @m_le_plus_n_m
    433       ]
    434     |3:
    435       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    436       #status_final #is_next #is_call #is_after_return #call_trace #final_trace
    437       change with (
    438       let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
    439       let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    440       let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
    441         call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?);
    442       normalize nodelta;
    443       @conj
    444       [1:
    445         cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
    446           status_after_fun_call call_trace)
    447         #trace_label_return_eq #trace_label_return_le
    448         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
    449           status_final final_trace)
    450         #trace_any_label_eq #trace_any_label_le
    451         >trace_any_label_eq >trace_label_return_eq
    452         cases(is_next)
    453         cases(execute_1 status_pre_fun_call)
    454         #the_status #assm
    455         whd in match eject; normalize nodelta;
    456         >assm >commutative_plus in match
    457           (current_instruction_cost status_pre_fun_call
    458             + clock (BitVectorTrie Byte 16) status_pre_fun_call);
    459         >m_minus_n_plus_o_m_minus_n_minus_o
    460         <(plus_minus_m_m
    461           (clock (BitVectorTrie Byte 16) status_after_fun_call
    462             - clock (BitVectorTrie Byte 16) status_pre_fun_call)
    463           (current_instruction_cost status_pre_fun_call))
    464         [1:
    465           @plus_minus_rearrangement_1
    466           lapply(transitive_le
    467             (clock … status_pre_fun_call)
    468             (clock … status_start_fun_call)
    469             (clock … status_after_fun_call) ? trace_label_return_le)
    470           [1,3:
    471             cases(is_next)
    472             cases(execute_1 status_pre_fun_call)
    473             whd in match eject; normalize nodelta;
    474             #the_new_status #assm >assm @m_le_plus_n_m
    475           |2,4:
    476             #assm assumption
    477           ]
    478         |2:
    479           cases(is_next)
    480           assumption
    481       |2:
    482         cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
    483           status_after_fun_call call_trace)
    484         #trace_label_return_eq
    485         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
    486           status_final final_trace)
    487         #trace_any_label_eq cases(is_next)
    488         cases(execute_1 status_pre_fun_call)
    489         #the_status #assm
    490         whd in match eject; normalize nodelta;
    491         >assm #after_final_le #pre_after_le
    492         lapply(n_plus_m_le_o_to_m_le_o
    493           (clock … status_pre_fun_call)
    494           (current_instruction_cost status_pre_fun_call)
    495           (clock … status_after_fun_call) pre_after_le);
    496         #pre_after_le'
    497         @(transitive_le
    498           (clock … status_pre_fun_call)
    499           (clock … status_after_fun_call)
    500           (clock … status_final))
    501         assumption
    502       ]
    503     |*: cases daemon (* XXX: for now
    504       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    505       #status_final #is_next #is_call #is_after_return #call_trace #final_trace
    506       change with (
    507       let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
    508       let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    509       let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
    510         call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?);
    511       normalize nodelta;
    512       @conj
    513       [1:
    514         cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
    515           status_after_fun_call call_trace)
    516         #trace_label_return_eq #trace_label_return_le
    517         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
    518           status_final final_trace)
    519         #trace_any_label_eq #trace_any_label_le
    520         >trace_label_return_eq >trace_any_label_eq
    521         cases(is_next)
    522         >(clock_execute_1 status_pre_fun_call) in match (clock … (execute_1 status_pre_fun_call));
    523         >commutative_plus in match (
    524           (current_instruction_cost status_pre_fun_call
    525             + clock (BitVectorTrie Byte 16) status_pre_fun_call));
    526         <minus_plus
    527         <(plus_minus_m_m (clock (BitVectorTrie Byte 16) status_after_fun_call
    528   -clock (BitVectorTrie Byte 16) status_pre_fun_call) (current_instruction_cost status_pre_fun_call))
    529         [1:
    530           >plus_minus_rearrangement_1
    531           [1:
    532             %
    533           |2:
    534             assumption
    535           |3:
    536             generalize in match trace_label_return_le;
    537             cases(is_next)
    538             >(clock_execute_1 status_pre_fun_call)
    539             @plus_le_le
    540           ]
    541         |2:
    542           cases daemon (* XXX: todo *)
    543         ]
    544       |2:
    545         cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
    546           status_after_fun_call call_trace)
    547         #trace_label_return_eq cases(is_next)
    548         >clock_execute_1
    549         #trace_label_return_le
    550         lapply (plus_le_le … trace_label_return_le)
    551         #trace_label_return_le'
    552         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
    553           status_final final_trace)
    554         #trace_any_label_eq #trace_any_label_le
    555         @(transitive_le (clock … status_pre_fun_call) (clock … status_after_fun_call) (clock … status_final))
    556         assumption
    557       ]
    558     |4:
    559       #end_flag #status_pre #status_init #status_end #is_next
    560       #trace_any_label #is_other #is_not_costed
    561       change with (
    562       let current_instruction_cost ≝ current_instruction_cost status_pre in
    563       let tail_trace_cost ≝
    564        compute_max_trace_any_label_cost cost_labels end_flag
    565         status_init status_end trace_any_label
    566       in
    567         current_instruction_cost + tail_trace_cost) in ⊢ (?(??%?)?);
    568       normalize nodelta;
    569       @conj
    570       [1:
    571         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
    572         status_init status_end trace_any_label)
    573         #trace_any_label_eq #trace_any_label_le
    574         >trace_any_label_eq
    575         cases(is_next)
    576         >commutative_plus
    577         >clock_execute_1
    578         >commutative_plus in match ((current_instruction_cost status_pre+clock (BitVectorTrie Byte 16) status_pre));
    579         <minus_plus
    580         <plus_minus_m_m
    581         [1: %
    582         |2: cases daemon (* XXX: todo *)
    583         ]
    584       |2:
    585         cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
    586         status_init status_end trace_any_label)
    587         #trace_any_label_eq
    588         cases(is_next)
    589         >clock_execute_1
    590         @plus_le_le
    591       ]*)
    592     ]
    593   |3:
    594     cases the_trace
    595     [1:
    596       #status_before #status_after #trace_to_lift
    597       normalize @compute_max_trace_label_label_cost_is_ok
    598     |2:
    599       #status_initial #status_labelled #status_final #labelled_trace #ret_trace
    600       normalize
    601       cases(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
    602       #label_label_trace_equality #label_label_trace_leq
    603       cases(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
    604       #label_return_trace_equality #label_return_trace_leq
    605       >label_label_trace_equality >label_return_trace_equality
    606       @conj
    607       [2: @(transitive_le (clock (BitVectorTrie (Vector bool 8) 16) status_initial)
    608             (clock (BitVectorTrie Byte 16) status_labelled)
    609             (clock (BitVectorTrie (Vector bool 8) 16) status_final))
    610       |1: @plus_minus_rearrangement_1
    611       ]
    612       assumption
    613     ]
    614   ]
    615 qed.
    616376
    617377(* XXX: work below here: *)
  • src/ASM/Interpret.ma

    r1577 r1581  
    590590    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus)
    591591    try (/demod/ normalize nodelta >clock_set_clock @commutative_plus)
     592    [5: /demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock
    592593(* XXX: weird open goals here *)
    593594(*    [14: normalize nodelta <set_arg_8_ignores_clock /demod/ normalize nodelta
  • src/ASM/Status.ma

    r1541 r1581  
    10201020qed.
    10211021     
    1022 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; carry ]] →
    1023                        Bit → PreStatus M ≝
    1024   λm, s, a, v.
    1025     match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
     1022(* XXX: Russell typing: Σs': PreStatus M. clock … s = clock M s', causes dangling de Bruijn
     1023        pointer assertion failure in nCicMetaSubst.ml, line 293.  *)
     1024definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝
     1025  λm: Type[0].
     1026  λs: PreStatus m.
     1027  λa: [[bit_addr; carry]].
     1028  λv: Bit.
     1029    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
    10261030      [ BIT_ADDR b ⇒ λbit_addr: True.
    1027           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    1028           let bit_1 ≝ get_index_v ?? nu 0 ? in
    1029           let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
    1030           match bit_1 with
    1031             [ true ⇒
    1032                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1033                 let d ≝ address ÷ 8 in
    1034                 let m ≝ address mod 8 in
    1035                 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1036                 let sfr ≝ get_bit_addressable_sfr ? s ? t true in
    1037                 let new_sfr ≝ set_index … sfr m v ? in
    1038                   set_bit_addressable_sfr ? s new_sfr t
    1039             | false ⇒
    1040                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1041                 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1042                 let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
    1043                 let n_bit ≝ set_index … t (modulus address 8) v ? in
    1044                 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
    1045                   set_low_internal_ram ? s memory
    1046             ]
     1031        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
     1032        let bit_1 ≝ get_index_v ?? nu 0 ? in
     1033        let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
     1034        match bit_1 return λ_. ? with
     1035          [ true ⇒
     1036            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     1037            let d ≝ address ÷ 8 in
     1038            let m ≝ address mod 8 in
     1039            let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     1040            let sfr ≝ get_bit_addressable_sfr ? s ? t true in
     1041            let new_sfr ≝ set_index … sfr m v ? in
     1042              set_bit_addressable_sfr ? s new_sfr t
     1043          | false ⇒
     1044            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     1045            let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1046            let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
     1047            let n_bit ≝ set_index … t (modulus address 8) v ? in
     1048            let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
     1049              set_low_internal_ram ? s memory
     1050          ]
    10471051      | CARRY ⇒
    10481052        λcarry: True.
    1049           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    1050           let bit_1 ≝ get_index_v… nu 1 ? in
    1051           let bit_2 ≝ get_index_v… nu 2 ? in
    1052           let bit_3 ≝ get_index_v… nu 3 ? in
    1053           let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
    1054             set_8051_sfr ? s SFR_PSW new_psw
     1053        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
     1054        let bit_1 ≝ get_index_v… nu 1 ? in
     1055        let bit_2 ≝ get_index_v… nu 2 ? in
     1056        let bit_3 ≝ get_index_v… nu 3 ? in
     1057        let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
     1058          set_8051_sfr ? s SFR_PSW new_psw
    10551059      | _ ⇒
    10561060        λother: False.
Note: See TracChangeset for help on using the changeset viewer.