Ignore:
Timestamp:
Jun 26, 2013, 2:22:28 PM (6 years ago)
Author:
piccolo
Message:

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/MoveCorrectness.ma

    r3253 r3371  
    2222match d with
    2323[ decision_spill n ⇒
     24  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 (localss + n)) : Byte × Byte) in
    2425  ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
    2526  ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
    2627  ! 〈newaddrl,new_carry〉 ←
    27      be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
    28   ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
     28     be_op2 (carry … st) Add (BVByte off_l) addrl;
     29  ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc (BVByte off_h) addrh;
    2930  ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
    3031  ! new_mem ← opt_to_res ? [MSG FailedStore] (bestorev (m … st) ptr bv);
     
    4647    return 〈hwreg_retrieve (regs … st) r,st〉
    4748| arg_decision_spill n ⇒
     49  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 (localss + n)) : Byte × Byte) in
    4850  ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
    4951  ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
    5052  ! 〈newaddrl,new_carry〉 ←
    51      be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
    52   ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
     53     be_op2 (carry … st) Add (BVByte off_l) addrl;
     54  ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc (BVByte off_h) addrh;
    5355  ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
    5456  ! bv ← opt_to_res ? [MSG FailedLoad] (beloadv (m … st) ptr);
     
    165167  whd in match repeat_eval_seq_no_pc; normalize nodelta
    166168  whd in match preserve_carry_bit; normalize nodelta cases cl -cl
    167   normalize nodelta whd in match (m_fold ??????) in ⊢ (??%?? → ?);
     169  normalize nodelta @pair_elim #off_h #off_l #EQoff_hl
     170  whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    168171  inversion (eval_seq_no_pc ??????) [2,4: #e #_ normalize nodelta #EQ destruct(EQ)]
    169172  #st'' whd in match set_regs; whd in match eval_seq_no_pc in ⊢ (% → ?);
     
    207210  ]
    208211  >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?); #EQptr normalize nodelta
    209   #H @('bind_inversion H) -H #bv #H lapply(opt_eq_from_res ???? H) -H #EQbv
     212  >m_return_bind #H @('bind_inversion H) -H
     213  #bv #H lapply(opt_eq_from_res ???? H) -H #EQbv
    210214  whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    211215  >(hwreg_store_commute RegisterDPH RegisterA) [2,4: normalize % #EQ destruct]
    212216  >hwreg_store_idempotent >m_return_bind whd in match set_regs; normalize nodelta
    213   whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    214   normalize nodelta inversion (eval_seq_no_pc ??????)
     217  whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match set_dp_by_offset; normalize nodelta
     218  @pair_elim #off_h_d #off_l_d #EQoff_hld whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
     219  normalize nodelta  inversion (eval_seq_no_pc ??????)
    215220  [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    216221  >(hwreg_store_commute RegisterST1 RegisterA) [2,4: normalize % #EQ destruct]
     
    280285      #EQptr1 normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    281286      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    282       >m_return_bind #H @('bind_inversion H) -H #m1 #H lapply(opt_eq_from_res ???? H)
     287      >m_return_bind >m_return_bind #H @('bind_inversion H) -H #m1 #H lapply(opt_eq_from_res ???? H)
    283288      -H #EQm1 whd in match set_m; normalize nodelta whd in ⊢ (??%% → ?);
    284289      #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
     
    288293        whd in match set_carry; normalize nodelta ]
    289294      #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
     295      >EQoff_hl normalize nodelta
    290296      >m_return_bind >m_return_bind >EQx1x2 >m_return_bind >EQy1y2
    291297      >m_return_bind >EQptr >m_return_bind >EQbv >m_return_bind
    292298      whd in match set_regs; whd in match write_decision; normalize nodelta
     299      >EQoff_hld normalize nodelta
    293300      whd in match hw_reg_retrieve; normalize nodelta
    294301      >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
     
    369376      ]
    370377      whd in match set_stack_not_a; whd in match set_dp_by_offset;
    371       whd in match repeat_eval_seq_no_pc; normalize nodelta
     378      whd in match repeat_eval_seq_no_pc; normalize nodelta whd in match get_stack;
     379      normalize nodelta whd in match set_dp_by_offset; normalize  nodelta
     380      @pair_elim #off_hs #off_ls #EQoff_hls
    372381      whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    373382      inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ normalize nodelta #EQ destruct]
     
    433442      ]
    434443      #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    435       whd in match (acca_arg_retrieve_ ?????);
     444      whd in match (acca_arg_retrieve_ ?????); >m_return_bind
    436445       #H @('bind_inversion H) -H  #m1 #H lapply(opt_eq_from_res ???? H) -H #EQm1
    437446       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
Note: See TracChangeset for help on using the changeset viewer.