Changeset 3043 for extracted/joint.mli


Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.mli

    r2951 r3043  
    584584| POP of __
    585585| PUSH of __
    586 | ADDRESS of AST.ident * __ * __
     586| ADDRESS of AST.ident * BitVector.word * __ * __
    587587| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
    588588| OP1 of BackEndOps.op1 * __ * __
     
    596596val joint_seq_rect_Type4 :
    597597  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
    598   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
    599   'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
    600   (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
    601   'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
    602   (__ -> 'a1) -> joint_seq -> 'a1
     598  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
     599  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
     600  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
     601  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
     602  -> (__ -> 'a1) -> joint_seq -> 'a1
    603603
    604604val joint_seq_rect_Type5 :
    605605  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
    606   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
    607   'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
    608   (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
    609   'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
    610   (__ -> 'a1) -> joint_seq -> 'a1
     606  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
     607  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
     608  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
     609  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
     610  -> (__ -> 'a1) -> joint_seq -> 'a1
    611611
    612612val joint_seq_rect_Type3 :
    613613  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
    614   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
    615   'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
    616   (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
    617   'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
    618   (__ -> 'a1) -> joint_seq -> 'a1
     614  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
     615  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
     616  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
     617  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
     618  -> (__ -> 'a1) -> joint_seq -> 'a1
    619619
    620620val joint_seq_rect_Type2 :
    621621  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
    622   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
    623   'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
    624   (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
    625   'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
    626   (__ -> 'a1) -> joint_seq -> 'a1
     622  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
     623  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
     624  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
     625  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
     626  -> (__ -> 'a1) -> joint_seq -> 'a1
    627627
    628628val joint_seq_rect_Type1 :
    629629  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
    630   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
    631   'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
    632   (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
    633   'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
    634   (__ -> 'a1) -> joint_seq -> 'a1
     630  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
     631  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
     632  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
     633  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
     634  -> (__ -> 'a1) -> joint_seq -> 'a1
    635635
    636636val joint_seq_rect_Type0 :
    637637  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
    638   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
    639   'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
    640   (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
    641   'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
    642   (__ -> 'a1) -> joint_seq -> 'a1
     638  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
     639  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
     640  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
     641  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
     642  -> (__ -> 'a1) -> joint_seq -> 'a1
    643643
    644644val joint_seq_inv_rect_Type4 :
    645645  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
    646646  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
    647   'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
    648   __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
    649   'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
    650   (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
    651   'a1) -> (__ -> __ -> 'a1) -> 'a1
     647  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
     648  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
     649  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
     650  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
     651  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
    652652
    653653val joint_seq_inv_rect_Type3 :
    654654  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
    655655  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
    656   'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
    657   __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
    658   'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
    659   (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
    660   'a1) -> (__ -> __ -> 'a1) -> 'a1
     656  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
     657  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
     658  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
     659  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
     660  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
    661661
    662662val joint_seq_inv_rect_Type2 :
    663663  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
    664664  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
    665   'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
    666   __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
    667   'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
    668   (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
    669   'a1) -> (__ -> __ -> 'a1) -> 'a1
     665  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
     666  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
     667  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
     668  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
     669  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
    670670
    671671val joint_seq_inv_rect_Type1 :
    672672  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
    673673  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
    674   'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
    675   __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
    676   'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
    677   (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
    678   'a1) -> (__ -> __ -> 'a1) -> 'a1
     674  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
     675  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
     676  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
     677  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
     678  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
    679679
    680680val joint_seq_inv_rect_Type0 :
    681681  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
    682682  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
    683   'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
    684   __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
    685   'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
    686   (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
    687   'a1) -> (__ -> __ -> 'a1) -> 'a1
     683  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
     684  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
     685  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
     686  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
     687  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
    688688
    689689val joint_seq_discr :
     
    14051405type joint_function = joint_closed_internal_function AST.fundef
    14061406
    1407 type joint_program = { joint_prog : (joint_function, AST.init_data List.list)
     1407type joint_program = { jp_functions : AST.ident List.list;
     1408                       joint_prog : (joint_function, AST.init_data List.list)
    14081409                                    AST.program;
    14091410                       init_cost_label : CostLabel.costlabel }
    14101411
    14111412val joint_program_rect_Type4 :
    1412   params -> ((joint_function, AST.init_data List.list) AST.program ->
    1413   CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1413  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
     1414  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
    14141415
    14151416val joint_program_rect_Type5 :
    1416   params -> ((joint_function, AST.init_data List.list) AST.program ->
    1417   CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1417  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
     1418  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
    14181419
    14191420val joint_program_rect_Type3 :
    1420   params -> ((joint_function, AST.init_data List.list) AST.program ->
    1421   CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1421  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
     1422  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
    14221423
    14231424val joint_program_rect_Type2 :
    1424   params -> ((joint_function, AST.init_data List.list) AST.program ->
    1425   CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1425  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
     1426  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
    14261427
    14271428val joint_program_rect_Type1 :
    1428   params -> ((joint_function, AST.init_data List.list) AST.program ->
    1429   CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1429  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
     1430  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
    14301431
    14311432val joint_program_rect_Type0 :
    1432   params -> ((joint_function, AST.init_data List.list) AST.program ->
    1433   CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1433  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
     1434  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
     1435
     1436val jp_functions : params -> joint_program -> AST.ident List.list
    14341437
    14351438val joint_prog :
     
    14401443
    14411444val joint_program_inv_rect_Type4 :
    1442   params -> joint_program -> ((joint_function, AST.init_data List.list)
    1443   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1445  params -> joint_program -> (AST.ident List.list -> (joint_function,
     1446  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
     1447  'a1) -> 'a1
    14441448
    14451449val joint_program_inv_rect_Type3 :
    1446   params -> joint_program -> ((joint_function, AST.init_data List.list)
    1447   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1450  params -> joint_program -> (AST.ident List.list -> (joint_function,
     1451  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
     1452  'a1) -> 'a1
    14481453
    14491454val joint_program_inv_rect_Type2 :
    1450   params -> joint_program -> ((joint_function, AST.init_data List.list)
    1451   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1455  params -> joint_program -> (AST.ident List.list -> (joint_function,
     1456  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
     1457  'a1) -> 'a1
    14521458
    14531459val joint_program_inv_rect_Type1 :
    1454   params -> joint_program -> ((joint_function, AST.init_data List.list)
    1455   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1460  params -> joint_program -> (AST.ident List.list -> (joint_function,
     1461  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
     1462  'a1) -> 'a1
    14561463
    14571464val joint_program_inv_rect_Type0 :
    1458   params -> joint_program -> ((joint_function, AST.init_data List.list)
    1459   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1465  params -> joint_program -> (AST.ident List.list -> (joint_function,
     1466  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
     1467  'a1) -> 'a1
    14601468
    14611469val joint_program_discr : params -> joint_program -> joint_program -> __
     
    14831491  List.list) AST.program
    14841492
     1493val prog_names : params -> joint_program -> AST.ident List.list
     1494
     1495val transform_joint_program :
     1496  params -> params -> (AST.ident List.list -> joint_closed_internal_function
     1497  -> joint_closed_internal_function) -> joint_program -> joint_program
     1498
    14851499type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
    14861500
Note: See TracChangeset for help on using the changeset viewer.