Changeset 2933


Ignore:
Timestamp:
Mar 21, 2013, 8:11:50 PM (4 years ago)
Author:
sacerdot
Message:

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

Location:
extracted
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • extracted/backEndOps.ml

    r2873 r2933  
    402402    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    403403    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    404 let rec eval_rect_Type4 h_mk_Eval x_19271 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19271 in
     404let rec eval_rect_Type4 h_mk_Eval x_601 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_601 in
    406406  h_mk_Eval opaccs0 op4 op5
    407407
     
    411411    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    412412    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    413 let rec eval_rect_Type5 h_mk_Eval x_19273 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19273 in
     413let rec eval_rect_Type5 h_mk_Eval x_603 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_603 in
    415415  h_mk_Eval opaccs0 op4 op5
    416416
     
    420420    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    421421    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    422 let rec eval_rect_Type3 h_mk_Eval x_19275 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19275 in
     422let rec eval_rect_Type3 h_mk_Eval x_605 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_605 in
    424424  h_mk_Eval opaccs0 op4 op5
    425425
     
    429429    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    430430    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    431 let rec eval_rect_Type2 h_mk_Eval x_19277 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19277 in
     431let rec eval_rect_Type2 h_mk_Eval x_607 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_607 in
    433433  h_mk_Eval opaccs0 op4 op5
    434434
     
    438438    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    439439    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    440 let rec eval_rect_Type1 h_mk_Eval x_19279 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19279 in
     440let rec eval_rect_Type1 h_mk_Eval x_609 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_609 in
    442442  h_mk_Eval opaccs0 op4 op5
    443443
     
    447447    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    448448    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    449 let rec eval_rect_Type0 h_mk_Eval x_19281 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19281 in
     449let rec eval_rect_Type0 h_mk_Eval x_611 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_611 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
     
    648648  Vector.fold_right2_i f { Types.fst = Vector.VEmpty; Types.snd = carry } n
    649649
     650(** val op_of_add_or_sub : ByteValues.add_or_sub -> op2 **)
     651let op_of_add_or_sub = function
     652| ByteValues.Do_add -> Addc
     653| ByteValues.Do_sub -> Sub
     654
    650655(** val be_add_sub_byte :
    651     Bool.bool -> ByteValues.bebit -> ByteValues.beval -> BitVector.byte ->
    652     (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
     656    ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
     657    BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
     658    Errors.res **)
    653659let be_add_sub_byte is_add carry a1 b2 =
    654   let op =
    655     match is_add with
    656     | Bool.True -> Addc
    657     | Bool.False -> Sub
    658   in
     660  let op = op_of_add_or_sub is_add in
    659661  (match a1 with
    660662   | ByteValues.BVundef ->
     
    726728            | ByteValues.BBptrcarry (is_add', ptr', p', by') ->
    727729              (match Bool.andb
    728                        (Bool.andb (BitVector.eq_b is_add is_add')
     730                       (Bool.andb (ByteValues.eq_add_or_sub is_add is_add')
    729731                         (Pointers.eq_block ptr.Pointers.pblock
    730732                           ptr'.Pointers.pblock))
     
    755757                   in
    756758                   let part1 = Nat.S Nat.O in
    757                    let ptr'0 = { Pointers.pblock = ptr.Pointers.pblock;
     759                   let ptr'' = { Pointers.pblock = ptr.Pointers.pblock;
    758760                     Pointers.poff =
    759761                     (Vector.vflatten (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S
     
    761763                       Nat.O)))))))) rslt) }
    762764                   in
    763                    Errors.OK { Types.fst = (ByteValues.BVptr (ptr'0, part1));
    764                    Types.snd = (ByteValues.BBptrcarry (is_add, ptr'0, part1,
     765                   Errors.OK { Types.fst = (ByteValues.BVptr (ptr'', part1));
     766                   Types.snd = (ByteValues.BBptrcarry (is_add, ptr', part1,
    765767                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    766768                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
     
    826828         List.Nil))
    827829     | ByteValues.BVByte b1 ->
    828        be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1
     830       be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a2 b1
    829831     | ByteValues.BVnull x ->
    830832       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    842844            List.Nil))
    843845        | ByteValues.BVByte b2 ->
    844           be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2
     846          be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a1
     847            b2
    845848        | ByteValues.BVnull x ->
    846849          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    866869       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    867870         List.Nil))
    868      | ByteValues.BVByte b1 -> be_add_sub_byte Bool.True carry a2 b1
     871     | ByteValues.BVByte b1 -> be_add_sub_byte ByteValues.Do_add carry a2 b1
    869872     | ByteValues.BVnull x ->
    870873       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    881884          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    882885            List.Nil))
    883         | ByteValues.BVByte b2 -> be_add_sub_byte Bool.True carry a1 b2
     886        | ByteValues.BVByte b2 ->
     887          be_add_sub_byte ByteValues.Do_add carry a1 b2
    884888        | ByteValues.BVnull x ->
    885889          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    905909       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    906910         List.Nil))
    907      | ByteValues.BVByte b1 -> be_add_sub_byte Bool.False carry a2 b1
     911     | ByteValues.BVByte b1 ->
     912       Obj.magic
     913         (Monad.m_bind0 (Monad.max_def Errors.res0)
     914           (Obj.magic
     915             (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
     916           (fun b2 ->
     917           Obj.magic (be_add_sub_byte ByteValues.Do_sub carry a1 b2)))
    908918     | ByteValues.BVnull x ->
    909919       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    920930          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    921931            List.Nil))
    922         | ByteValues.BVByte b2 -> be_add_sub_byte Bool.False carry a1 b2
     932        | ByteValues.BVByte b2 ->
     933          be_add_sub_byte ByteValues.Do_sub carry a1 b2
    923934        | ByteValues.BVnull x ->
    924935          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
  • extracted/backEndOps.mli

    r2773 r2933  
    302302  BitVector.bit) Types.prod
    303303
     304val op_of_add_or_sub : ByteValues.add_or_sub -> op2
     305
    304306val be_add_sub_byte :
    305   Bool.bool -> ByteValues.bebit -> ByteValues.beval -> BitVector.byte ->
    306   (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res
     307  ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
     308  BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
     309  Errors.res
    307310
    308311val byte_at : Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte
  • extracted/byteValues.ml

    r2827 r2933  
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_6139 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6139 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_3 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_3 in
    9393  h_mk_program_counter pc_block0 pc_offset0
    9494
     
    9696    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9797    'a1 **)
    98 let rec program_counter_rect_Type5 h_mk_program_counter x_6141 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6141 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_5 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5 in
    100100  h_mk_program_counter pc_block0 pc_offset0
    101101
     
    103103    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    104104    'a1 **)
    105 let rec program_counter_rect_Type3 h_mk_program_counter x_6143 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6143 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_7 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_7 in
    107107  h_mk_program_counter pc_block0 pc_offset0
    108108
     
    110110    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    111111    'a1 **)
    112 let rec program_counter_rect_Type2 h_mk_program_counter x_6145 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6145 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_9 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_9 in
    114114  h_mk_program_counter pc_block0 pc_offset0
    115115
     
    117117    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    118118    'a1 **)
    119 let rec program_counter_rect_Type1 h_mk_program_counter x_6147 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6147 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_11 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_11 in
    121121  h_mk_program_counter pc_block0 pc_offset0
    122122
     
    124124    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    125125    'a1 **)
    126 let rec program_counter_rect_Type0 h_mk_program_counter x_6149 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6149 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_13 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_13 in
    128128  h_mk_program_counter pc_block0 pc_offset0
    129129
     
    215215
    216216(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    217 let rec part_rect_Type4 h_mk_part x_6165 =
    218   let part_no = x_6165 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_29 =
     218  let part_no = x_29 in h_mk_part part_no __
    219219
    220220(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    221 let rec part_rect_Type5 h_mk_part x_6167 =
    222   let part_no = x_6167 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_31 =
     222  let part_no = x_31 in h_mk_part part_no __
    223223
    224224(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    225 let rec part_rect_Type3 h_mk_part x_6169 =
    226   let part_no = x_6169 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_33 =
     226  let part_no = x_33 in h_mk_part part_no __
    227227
    228228(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    229 let rec part_rect_Type2 h_mk_part x_6171 =
    230   let part_no = x_6171 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_35 =
     230  let part_no = x_35 in h_mk_part part_no __
    231231
    232232(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    233 let rec part_rect_Type1 h_mk_part x_6173 =
    234   let part_no = x_6173 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_37 =
     234  let part_no = x_37 in h_mk_part part_no __
    235235
    236236(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    237 let rec part_rect_Type0 h_mk_part x_6175 =
    238   let part_no = x_6175 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_39 =
     238  let part_no = x_39 in h_mk_part part_no __
    239239
    240240(** val part_no : part -> Nat.nat **)
     
    486486| BVundef -> h_BVundef
    487487| BVnonzero -> h_BVnonzero
    488 | BVXor (x_6209, x_6208, x_6207) -> h_BVXor x_6209 x_6208 x_6207
    489 | BVByte x_6210 -> h_BVByte x_6210
    490 | BVnull x_6211 -> h_BVnull x_6211
    491 | BVptr (x_6213, x_6212) -> h_BVptr x_6213 x_6212
    492 | BVpc (x_6215, x_6214) -> h_BVpc x_6215 x_6214
     488| BVXor (x_73, x_72, x_71) -> h_BVXor x_73 x_72 x_71
     489| BVByte x_74 -> h_BVByte x_74
     490| BVnull x_75 -> h_BVnull x_75
     491| BVptr (x_77, x_76) -> h_BVptr x_77 x_76
     492| BVpc (x_79, x_78) -> h_BVpc x_79 x_78
    493493
    494494(** val beval_rect_Type5 :
     
    500500| BVundef -> h_BVundef
    501501| BVnonzero -> h_BVnonzero
    502 | BVXor (x_6226, x_6225, x_6224) -> h_BVXor x_6226 x_6225 x_6224
    503 | BVByte x_6227 -> h_BVByte x_6227
    504 | BVnull x_6228 -> h_BVnull x_6228
    505 | BVptr (x_6230, x_6229) -> h_BVptr x_6230 x_6229
    506 | BVpc (x_6232, x_6231) -> h_BVpc x_6232 x_6231
     502| BVXor (x_90, x_89, x_88) -> h_BVXor x_90 x_89 x_88
     503| BVByte x_91 -> h_BVByte x_91
     504| BVnull x_92 -> h_BVnull x_92
     505| BVptr (x_94, x_93) -> h_BVptr x_94 x_93
     506| BVpc (x_96, x_95) -> h_BVpc x_96 x_95
    507507
    508508(** val beval_rect_Type3 :
     
    514514| BVundef -> h_BVundef
    515515| BVnonzero -> h_BVnonzero
    516 | BVXor (x_6243, x_6242, x_6241) -> h_BVXor x_6243 x_6242 x_6241
    517 | BVByte x_6244 -> h_BVByte x_6244
    518 | BVnull x_6245 -> h_BVnull x_6245
    519 | BVptr (x_6247, x_6246) -> h_BVptr x_6247 x_6246
    520 | BVpc (x_6249, x_6248) -> h_BVpc x_6249 x_6248
     516| BVXor (x_107, x_106, x_105) -> h_BVXor x_107 x_106 x_105
     517| BVByte x_108 -> h_BVByte x_108
     518| BVnull x_109 -> h_BVnull x_109
     519| BVptr (x_111, x_110) -> h_BVptr x_111 x_110
     520| BVpc (x_113, x_112) -> h_BVpc x_113 x_112
    521521
    522522(** val beval_rect_Type2 :
     
    528528| BVundef -> h_BVundef
    529529| BVnonzero -> h_BVnonzero
    530 | BVXor (x_6260, x_6259, x_6258) -> h_BVXor x_6260 x_6259 x_6258
    531 | BVByte x_6261 -> h_BVByte x_6261
    532 | BVnull x_6262 -> h_BVnull x_6262
    533 | BVptr (x_6264, x_6263) -> h_BVptr x_6264 x_6263
    534 | BVpc (x_6266, x_6265) -> h_BVpc x_6266 x_6265
     530| BVXor (x_124, x_123, x_122) -> h_BVXor x_124 x_123 x_122
     531| BVByte x_125 -> h_BVByte x_125
     532| BVnull x_126 -> h_BVnull x_126
     533| BVptr (x_128, x_127) -> h_BVptr x_128 x_127
     534| BVpc (x_130, x_129) -> h_BVpc x_130 x_129
    535535
    536536(** val beval_rect_Type1 :
     
    542542| BVundef -> h_BVundef
    543543| BVnonzero -> h_BVnonzero
    544 | BVXor (x_6277, x_6276, x_6275) -> h_BVXor x_6277 x_6276 x_6275
    545 | BVByte x_6278 -> h_BVByte x_6278
    546 | BVnull x_6279 -> h_BVnull x_6279
    547 | BVptr (x_6281, x_6280) -> h_BVptr x_6281 x_6280
    548 | BVpc (x_6283, x_6282) -> h_BVpc x_6283 x_6282
     544| BVXor (x_141, x_140, x_139) -> h_BVXor x_141 x_140 x_139
     545| BVByte x_142 -> h_BVByte x_142
     546| BVnull x_143 -> h_BVnull x_143
     547| BVptr (x_145, x_144) -> h_BVptr x_145 x_144
     548| BVpc (x_147, x_146) -> h_BVpc x_147 x_146
    549549
    550550(** val beval_rect_Type0 :
     
    556556| BVundef -> h_BVundef
    557557| BVnonzero -> h_BVnonzero
    558 | BVXor (x_6294, x_6293, x_6292) -> h_BVXor x_6294 x_6293 x_6292
    559 | BVByte x_6295 -> h_BVByte x_6295
    560 | BVnull x_6296 -> h_BVnull x_6296
    561 | BVptr (x_6298, x_6297) -> h_BVptr x_6298 x_6297
    562 | BVpc (x_6300, x_6299) -> h_BVpc x_6300 x_6299
     558| BVXor (x_158, x_157, x_156) -> h_BVXor x_158 x_157 x_156
     559| BVByte x_159 -> h_BVByte x_159
     560| BVnull x_160 -> h_BVnull x_160
     561| BVptr (x_162, x_161) -> h_BVptr x_162 x_161
     562| BVpc (x_164, x_163) -> h_BVpc x_164 x_163
    563563
    564564(** val beval_inv_rect_Type4 :
     
    828828| BVByte b ->
    829829  Errors.OK
    830     (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    831       Nat.O))))))))
    832       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    833         Nat.O))))))))) b)
     830    (Bool.notb
     831      (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     832        (Nat.S Nat.O))))))))
     833        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     834          (Nat.S Nat.O))))))))) b))
    834835| BVnull x -> Errors.OK Bool.False
    835836| BVptr (x, x0) -> Errors.OK Bool.True
     
    890891                ErrorMessages.NotAnInt32Val), List.Nil))))))))
    891892
     893type add_or_sub =
     894| Do_add
     895| Do_sub
     896
     897(** val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     898let rec add_or_sub_rect_Type4 h_do_add h_do_sub = function
     899| Do_add -> h_do_add
     900| Do_sub -> h_do_sub
     901
     902(** val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     903let rec add_or_sub_rect_Type5 h_do_add h_do_sub = function
     904| Do_add -> h_do_add
     905| Do_sub -> h_do_sub
     906
     907(** val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     908let rec add_or_sub_rect_Type3 h_do_add h_do_sub = function
     909| Do_add -> h_do_add
     910| Do_sub -> h_do_sub
     911
     912(** val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     913let rec add_or_sub_rect_Type2 h_do_add h_do_sub = function
     914| Do_add -> h_do_add
     915| Do_sub -> h_do_sub
     916
     917(** val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     918let rec add_or_sub_rect_Type1 h_do_add h_do_sub = function
     919| Do_add -> h_do_add
     920| Do_sub -> h_do_sub
     921
     922(** val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     923let rec add_or_sub_rect_Type0 h_do_add h_do_sub = function
     924| Do_add -> h_do_add
     925| Do_sub -> h_do_sub
     926
     927(** val add_or_sub_inv_rect_Type4 :
     928    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     929let add_or_sub_inv_rect_Type4 hterm h1 h2 =
     930  let hcut = add_or_sub_rect_Type4 h1 h2 hterm in hcut __
     931
     932(** val add_or_sub_inv_rect_Type3 :
     933    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     934let add_or_sub_inv_rect_Type3 hterm h1 h2 =
     935  let hcut = add_or_sub_rect_Type3 h1 h2 hterm in hcut __
     936
     937(** val add_or_sub_inv_rect_Type2 :
     938    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     939let add_or_sub_inv_rect_Type2 hterm h1 h2 =
     940  let hcut = add_or_sub_rect_Type2 h1 h2 hterm in hcut __
     941
     942(** val add_or_sub_inv_rect_Type1 :
     943    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     944let add_or_sub_inv_rect_Type1 hterm h1 h2 =
     945  let hcut = add_or_sub_rect_Type1 h1 h2 hterm in hcut __
     946
     947(** val add_or_sub_inv_rect_Type0 :
     948    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     949let add_or_sub_inv_rect_Type0 hterm h1 h2 =
     950  let hcut = add_or_sub_rect_Type0 h1 h2 hterm in hcut __
     951
     952(** val add_or_sub_discr : add_or_sub -> add_or_sub -> __ **)
     953let add_or_sub_discr x y =
     954  Logic.eq_rect_Type2 x
     955    (match x with
     956     | Do_add -> Obj.magic (fun _ dH -> dH)
     957     | Do_sub -> Obj.magic (fun _ dH -> dH)) y
     958
     959(** val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __ **)
     960let add_or_sub_jmdiscr x y =
     961  Logic.eq_rect_Type2 x
     962    (match x with
     963     | Do_add -> Obj.magic (fun _ dH -> dH)
     964     | Do_sub -> Obj.magic (fun _ dH -> dH)) y
     965
     966(** val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool **)
     967let eq_add_or_sub x y =
     968  match x with
     969  | Do_add ->
     970    (match y with
     971     | Do_add -> Bool.True
     972     | Do_sub -> Bool.False)
     973  | Do_sub ->
     974    (match y with
     975     | Do_add -> Bool.False
     976     | Do_sub -> Bool.True)
     977
    892978type bebit =
    893979| BBbit of Bool.bool
    894980| BBundef
    895 | BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
     981| BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
    896982
    897983(** val bebit_rect_Type4 :
    898     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     984    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    899985    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    900986let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    901 | BBbit x_6419 -> h_BBbit x_6419
     987| BBbit x_322 -> h_BBbit x_322
    902988| BBundef -> h_BBundef
    903 | BBptrcarry (x_6422, x_6421, p, x_6420) ->
    904   h_BBptrcarry x_6422 x_6421 p x_6420
     989| BBptrcarry (x_325, x_324, p, x_323) -> h_BBptrcarry x_325 x_324 p x_323
    905990
    906991(** val bebit_rect_Type5 :
    907     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     992    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    908993    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    909994let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    910 | BBbit x_6427 -> h_BBbit x_6427
     995| BBbit x_330 -> h_BBbit x_330
    911996| BBundef -> h_BBundef
    912 | BBptrcarry (x_6430, x_6429, p, x_6428) ->
    913   h_BBptrcarry x_6430 x_6429 p x_6428
     997| BBptrcarry (x_333, x_332, p, x_331) -> h_BBptrcarry x_333 x_332 p x_331
    914998
    915999(** val bebit_rect_Type3 :
    916     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     1000    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    9171001    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    9181002let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    919 | BBbit x_6435 -> h_BBbit x_6435
     1003| BBbit x_338 -> h_BBbit x_338
    9201004| BBundef -> h_BBundef
    921 | BBptrcarry (x_6438, x_6437, p, x_6436) ->
    922   h_BBptrcarry x_6438 x_6437 p x_6436
     1005| BBptrcarry (x_341, x_340, p, x_339) -> h_BBptrcarry x_341 x_340 p x_339
    9231006
    9241007(** val bebit_rect_Type2 :
    925     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     1008    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    9261009    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    9271010let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    928 | BBbit x_6443 -> h_BBbit x_6443
     1011| BBbit x_346 -> h_BBbit x_346
    9291012| BBundef -> h_BBundef
    930 | BBptrcarry (x_6446, x_6445, p, x_6444) ->
    931   h_BBptrcarry x_6446 x_6445 p x_6444
     1013| BBptrcarry (x_349, x_348, p, x_347) -> h_BBptrcarry x_349 x_348 p x_347
    9321014
    9331015(** val bebit_rect_Type1 :
    934     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     1016    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    9351017    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    9361018let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    937 | BBbit x_6451 -> h_BBbit x_6451
     1019| BBbit x_354 -> h_BBbit x_354
    9381020| BBundef -> h_BBundef
    939 | BBptrcarry (x_6454, x_6453, p, x_6452) ->
    940   h_BBptrcarry x_6454 x_6453 p x_6452
     1021| BBptrcarry (x_357, x_356, p, x_355) -> h_BBptrcarry x_357 x_356 p x_355
    9411022
    9421023(** val bebit_rect_Type0 :
    943     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     1024    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    9441025    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    9451026let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    946 | BBbit x_6459 -> h_BBbit x_6459
     1027| BBbit x_362 -> h_BBbit x_362
    9471028| BBundef -> h_BBundef
    948 | BBptrcarry (x_6462, x_6461, p, x_6460) ->
    949   h_BBptrcarry x_6462 x_6461 p x_6460
     1029| BBptrcarry (x_365, x_364, p, x_363) -> h_BBptrcarry x_365 x_364 p x_363
    9501030
    9511031(** val bebit_inv_rect_Type4 :
    952     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1032    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9531033    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9541034let bebit_inv_rect_Type4 hterm h1 h2 h3 =
     
    9561036
    9571037(** val bebit_inv_rect_Type3 :
    958     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1038    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9591039    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9601040let bebit_inv_rect_Type3 hterm h1 h2 h3 =
     
    9621042
    9631043(** val bebit_inv_rect_Type2 :
    964     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1044    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9651045    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9661046let bebit_inv_rect_Type2 hterm h1 h2 h3 =
     
    9681048
    9691049(** val bebit_inv_rect_Type1 :
    970     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1050    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9711051    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9721052let bebit_inv_rect_Type1 hterm h1 h2 h3 =
     
    9741054
    9751055(** val bebit_inv_rect_Type0 :
    976     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1056    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9771057    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9781058let bebit_inv_rect_Type0 hterm h1 h2 h3 =
  • extracted/byteValues.mli

    r2773 r2933  
    390390val word_of_list_beval : beval List.list -> Integers.int Errors.res
    391391
     392type add_or_sub =
     393| Do_add
     394| Do_sub
     395
     396val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     397
     398val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     399
     400val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     401
     402val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     403
     404val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     405
     406val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     407
     408val add_or_sub_inv_rect_Type4 :
     409  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     410
     411val add_or_sub_inv_rect_Type3 :
     412  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     413
     414val add_or_sub_inv_rect_Type2 :
     415  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     416
     417val add_or_sub_inv_rect_Type1 :
     418  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     419
     420val add_or_sub_inv_rect_Type0 :
     421  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     422
     423val add_or_sub_discr : add_or_sub -> add_or_sub -> __
     424
     425val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __
     426
     427val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool
     428
    392429type bebit =
    393430| BBbit of Bool.bool
    394431| BBundef
    395 | BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
     432| BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
    396433
    397434val bebit_rect_Type4 :
    398   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     435  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    399436  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    400437
    401438val bebit_rect_Type5 :
    402   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     439  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    403440  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    404441
    405442val bebit_rect_Type3 :
    406   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     443  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    407444  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    408445
    409446val bebit_rect_Type2 :
    410   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     447  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    411448  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    412449
    413450val bebit_rect_Type1 :
    414   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     451  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    415452  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    416453
    417454val bebit_rect_Type0 :
    418   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     455  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    419456  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    420457
    421458val bebit_inv_rect_Type4 :
    422   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     459  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    423460  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    424461
    425462val bebit_inv_rect_Type3 :
    426   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     463  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    427464  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    428465
    429466val bebit_inv_rect_Type2 :
    430   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     467  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    431468  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    432469
    433470val bebit_inv_rect_Type1 :
    434   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     471  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    435472  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    436473
    437474val bebit_inv_rect_Type0 :
    438   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     475  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    439476  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    440477
  • extracted/joint_semantics.ml

    r2890 r2933  
    19991999  match seq with
    20002000  | Joint.COMMENT x ->
     2001prerr_endline "COMMENT";
    20012002    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
    20022003  | Joint.MOVE dst_src ->
     2004prerr_endline "MOVE";
    20032005    Obj.magic
    20042006      (pair_reg_move (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    20052007        p.msu_pars st dst_src)
    20062008  | Joint.POP dst ->
     2009prerr_endline "POP";
    20072010    Obj.magic
    20082011      (Monad.m_bind2 (Monad.max_def Errors.res0)
     
    20122015            p.msu_pars dst v st')))
    20132016  | Joint.PUSH src ->
     2017prerr_endline "PUSH";
    20142018    Obj.magic
    20152019      (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    20192023        Obj.magic (push (msu_pars__o__st_pars p) st v)))
    20202024  | Joint.ADDRESS (id, ldest, hdest) ->
     2025prerr_endline "ADDRESS";
    20212026    let addr_block =
    20222027      Option.opt_safe
     
    20582063                  p.msu_pars dacc_b_reg v2' st'))))))
    20592064  | Joint.OP1 (op, dacc_a, sacc_a) ->
     2065prerr_endline "OP1";
    20602066    Obj.magic
    20612067      (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    20692075              p.msu_pars dacc_a v' st))))
    20702076  | Joint.OP2 (op, dacc_a, sacc_a, src) ->
     2077prerr_endline "OP2";
    20712078    Obj.magic
    20722079      (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    20812088            (Obj.magic (BackEndOps.be_op2 st.carry op v1 v2))
    20822089            (fun v' carry0 ->
     2090(if op = BackEndOps.Sub then
     2091(if carry0 = ByteValues.BBbit Bool.True then prerr_endline "CARRY = 1" else prerr_endline "CARRY = 0"));
    20832092            Monad.m_bind0 (Monad.max_def Errors.res0)
    20842093              (Obj.magic
     
    20882097                (set_carry p.msu_pars.st_pars carry0 st'))))))
    20892098  | Joint.CLEAR_CARRY ->
     2099prerr_endline "CLEAR_CARRY";
    20902100    Obj.magic
    20912101      (Monad.m_return0 (Monad.max_def Errors.res0)
    20922102        (set_carry (msu_pars__o__st_pars p) (ByteValues.BBbit Bool.False) st))
    20932103  | Joint.SET_CARRY ->
     2104prerr_endline "SET_CARRY";
    20942105    Obj.magic
    20952106      (Monad.m_return0 (Monad.max_def Errors.res0)
    20962107        (set_carry (msu_pars__o__st_pars p) (ByteValues.BBbit Bool.True) st))
    20972108  | Joint.LOAD (dst, addrl, addrh) ->
     2109prerr_endline "LOAD";
    20982110    Obj.magic
    20992111      (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    21172129                  p.msu_pars dst v st))))))
    21182130  | Joint.STORE (addrl, addrh, src) ->
     2131prerr_endline "STORE";
    21192132    Obj.magic
    21202133      (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    23112324    __ **)
    23122325let eval_return p globals ge0 curr_id curr_ret st =
     2326prerr_endline "eval_return";
    23132327  Monad.m_bind0 (Monad.max_def Errors.res0)
    23142328    (Obj.magic (p.msu_pars.pop_frame globals ge0 curr_id curr_ret st))
     
    23732387    (match s0 with
    23742388     | Joint.COST_LABEL x ->
     2389prerr_endline "COST";
    23752390       Obj.magic
    23762391         (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st))
    23772392     | Joint.CALL (f, args, dest) ->
     2393prerr_endline "CALL";
    23782394       Obj.magic (eval_call p g ge0 f args dest nxt st)
    23792395     | Joint.COND (a, l) ->
     2396prerr_endline "COND";
    23802397       IOMonad.err_to_io
    23812398         (Obj.magic
     
    24012418    (match s0 with
    24022419     | Joint.GOTO l ->
     2420prerr_endline "GOTO";
    24032421       IOMonad.err_to_io
    24042422         (goto p g
    24052423           (let p0 = p.spp in let globals = g in let g0 = ge0 in g0.ge) l st)
    24062424     | Joint.RETURN ->
     2425prerr_endline "RETURN";
    24072426       IOMonad.err_to_io
    24082427         (Obj.magic (eval_return p g ge0 curr_id curr_ret st.st_no_pc))
    24092428     | Joint.TAILCALL (f, args) ->
     2429prerr_endline "TAILCALL";
    24102430       Obj.magic (eval_tailcall p g ge0 f args curr_id curr_ret st))
    24112431  | Joint.FCOND (a, lbltrue, lblfalse) ->
     2432prerr_endline "FCOND";
    24122433    IOMonad.err_to_io
    24132434      (Obj.magic
     
    24432464       in
    24442465      Obj.magic x) (fun id fn s ->
     2466prerr_endline ("ID == " ^ string_of_int (Glue.int_of_matitapos id));
     2467       let res =
    24452468      Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    24462469        (let x =
     
    24502473        Obj.magic x) (fun st' ->
    24512474        let st'' = set_no_pc (msu_pars__o__st_pars p) st' st in
    2452         Obj.magic (eval_statement_advance p globals ge0 id fn s st''))))
     2475        Obj.magic (eval_statement_advance p globals ge0 id fn s st''))
     2476    in
     2477     match Obj.magic res with
     2478     | Wrong e ->
     2479        print_string "fun_";
     2480        print_int (Glue.int_of_matitapos id);
     2481        print_string ":";
     2482        let point = pc_offset (pc (msu_pars__o__st_pars p) st) in
     2483        print_int (Glue.int_of_matitapos point);
     2484        print_string ":";
     2485        res
     2486     | _ -> res))
    24532487
    24542488(** val is_final :
     
    24862520           | Joint.TAILCALL (x0, x1) -> Obj.magic (Errors.Error List.Nil))
    24872521        | Joint.FCOND (x0, x1, x2) -> Obj.magic (Errors.Error List.Nil))))
    2488 
  • extracted/rTL_semantics.ml

    r2890 r2933  
    436436          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
    437437          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
    438           let st0 =
    439             Util.foldl (fun st0 reg_val ->
    440               rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st
    441               reg_vals
    442           in
    443438          Monad.m_bind0 (Monad.max_def Errors.res0)
    444             (Obj.magic (Joint_semantics.sp rTL_state_params st0)) (fun sp ->
     439            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
    445440            let st1 =
    446441              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
     
    449444                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
    450445                    (Joint_semantics.set_m rTL_state_params
    451                       (GenMem.free st0.Joint_semantics.m
    452                         (Types.pi1 sp).Pointers.pblock) st0)))
     446                      (GenMem.free st.Joint_semantics.m
     447                        (Types.pi1 sp).Pointers.pblock) st)))
    453448            in
    454449            let pc = hd.fr_pc in
     450          let st1 =
     451            Util.foldl (fun st0 reg_val ->
     452prerr_endline ("SALVO IL REGISTRO: r_" ^ string_of_int (Glue.int_of_matitapos reg_val.Types.fst));
     453              rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st1
     454              reg_vals
     455          in
    455456            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
    456457              Types.snd = pc }))))
  • extracted/rTLabsToRTL.ml

    r2921 r2933  
    884884   | List.Cons (destr, x) ->
    885885     (fun _ ->
    886        let l = List.Cons ((Joint.OP1 (BackEndOps.Cmpl, (Obj.magic destr),
    887          (Obj.magic destr))), List.Nil)
     886       let l = List.Cons ((Joint.OP2 (BackEndOps.Xor, (Obj.magic destr),
     887         (Obj.magic (Joint.psd_argument_from_reg destr)),
     888         (Obj.magic
     889           (Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O)))))),
     890         List.Nil)
    888891       in
    889892       Bind_new.Bret l)) __
  • extracted/traces.ml

    r2890 r2933  
    142142    (AST.ident List.list -> Joint_semantics.sem_params ->
    143143    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    144 let rec evaluation_params_rect_Type4 h_mk_evaluation_params x_26086 =
    145   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    146     x_26086
    147   in
     144let rec evaluation_params_rect_Type4 h_mk_evaluation_params x_3 =
     145  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_3 in
    148146  h_mk_evaluation_params globals0 sparams0 ev_genv0
    149147
     
    151149    (AST.ident List.list -> Joint_semantics.sem_params ->
    152150    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    153 let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_26088 =
    154   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    155     x_26088
    156   in
     151let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_5 =
     152  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5 in
    157153  h_mk_evaluation_params globals0 sparams0 ev_genv0
    158154
     
    160156    (AST.ident List.list -> Joint_semantics.sem_params ->
    161157    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    162 let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_26090 =
    163   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    164     x_26090
    165   in
     158let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_7 =
     159  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_7 in
    166160  h_mk_evaluation_params globals0 sparams0 ev_genv0
    167161
     
    169163    (AST.ident List.list -> Joint_semantics.sem_params ->
    170164    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    171 let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_26092 =
    172   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    173     x_26092
    174   in
     165let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_9 =
     166  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_9 in
    175167  h_mk_evaluation_params globals0 sparams0 ev_genv0
    176168
     
    178170    (AST.ident List.list -> Joint_semantics.sem_params ->
    179171    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    180 let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_26094 =
    181   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    182     x_26094
     172let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_11 =
     173  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_11
    183174  in
    184175  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    187178    (AST.ident List.list -> Joint_semantics.sem_params ->
    188179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    189 let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_26096 =
    190   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    191     x_26096
     180let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_13 =
     181  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_13
    192182  in
    193183  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    279269    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    280270    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    281 let rec prog_params_rect_Type4 h_mk_prog_params x_26112 =
     271let rec prog_params_rect_Type4 h_mk_prog_params x_29 =
    282272  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    283     stack_sizes0 } = x_26112
     273    stack_sizes0 } = x_29
    284274  in
    285275  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    288278    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    289279    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    290 let rec prog_params_rect_Type5 h_mk_prog_params x_26114 =
     280let rec prog_params_rect_Type5 h_mk_prog_params x_31 =
    291281  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    292     stack_sizes0 } = x_26114
     282    stack_sizes0 } = x_31
    293283  in
    294284  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    297287    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    298288    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    299 let rec prog_params_rect_Type3 h_mk_prog_params x_26116 =
     289let rec prog_params_rect_Type3 h_mk_prog_params x_33 =
    300290  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    301     stack_sizes0 } = x_26116
     291    stack_sizes0 } = x_33
    302292  in
    303293  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    306296    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    307297    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    308 let rec prog_params_rect_Type2 h_mk_prog_params x_26118 =
     298let rec prog_params_rect_Type2 h_mk_prog_params x_35 =
    309299  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    310     stack_sizes0 } = x_26118
     300    stack_sizes0 } = x_35
    311301  in
    312302  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    315305    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    316306    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    317 let rec prog_params_rect_Type1 h_mk_prog_params x_26120 =
     307let rec prog_params_rect_Type1 h_mk_prog_params x_37 =
    318308  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    319     stack_sizes0 } = x_26120
     309    stack_sizes0 } = x_37
    320310  in
    321311  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    324314    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    325315    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    326 let rec prog_params_rect_Type0 h_mk_prog_params x_26122 =
     316let rec prog_params_rect_Type0 h_mk_prog_params x_39 =
    327317  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    328     stack_sizes0 } = x_26122
     318    stack_sizes0 } = x_39
    329319  in
    330320  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    555545        (match s with
    556546         | Joint.COST_LABEL x0 -> dummy
    557          | Joint.CALL (x0, x1, x2) -> dummy
     547         | Joint.CALL (f', args, dest) ->
     548           (match Obj.magic
     549                    (Monad.m_bind0 (Monad.max_def Errors.res0)
     550                      (Joint_semantics.block_of_call p.sparams p.globals
     551                        (let p0 = p.sparams.Joint_semantics.spp in
     552                        let globals0 = p.globals in
     553                        let g = p.ev_genv in g.Joint_semantics.ge) f'
     554                        st.Joint_semantics.st_no_pc) (fun bl ->
     555                      Obj.magic
     556                        (Joint_semantics.fetch_internal_function
     557                          (let p0 = p.sparams.Joint_semantics.spp in
     558                          let globals0 = p.globals in
     559                          let g = p.ev_genv in g.Joint_semantics.ge) bl))) with
     560            | Errors.OK i_f -> i_f.Types.fst
     561            | Errors.Error x0 -> dummy)
    558562         | Joint.COND (x0, x1) -> dummy
    559          | Joint.Step_seq s0 ->
    560            (match Joint.Step_seq
    561             s0 with
    562             | Joint.COST_LABEL x0 -> dummy
    563             | Joint.CALL (f', args, dest) ->
    564               (match Obj.magic
    565                        (Monad.m_bind0 (Monad.max_def Errors.res0)
    566                          (Joint_semantics.block_of_call p.sparams p.globals
    567                            (let p0 = p.sparams.Joint_semantics.spp in
    568                            let globals0 = p.globals in
    569                            let g = p.ev_genv in g.Joint_semantics.ge) f'
    570                            st.Joint_semantics.st_no_pc) (fun bl ->
    571                          Obj.magic
    572                            (Joint_semantics.fetch_internal_function
    573                              (let p0 = p.sparams.Joint_semantics.spp in
    574                              let globals0 = p.globals in
    575                              let g = p.ev_genv in g.Joint_semantics.ge) bl))) with
    576                | Errors.OK i_f -> i_f.Types.fst
    577                | Errors.Error x0 -> dummy)
    578             | Joint.COND (x0, x1) -> dummy
    579             | Joint.Step_seq x0 -> dummy))
     563         | Joint.Step_seq x0 -> dummy)
    580564      | Joint.Final x0 -> dummy
    581565      | Joint.FCOND (x0, x1, x2) -> dummy)
Note: See TracChangeset for help on using the changeset viewer.