Changeset 2967


Ignore:
Timestamp:
Mar 26, 2013, 6:54:12 PM (4 years ago)
Author:
sacerdot
Message:

Semantics changed so that a terminating joint program that returns an undefined
value is recognized as a terminating program that returns a dummy integer
(the maximum allowed one). This because the front-end type for termination is
int option and it does not discriminate between "non final" and "final with
no value". How is that possible in the front-end?

Files:
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/traces.ml

    r2960 r2967  
    157157    Joint_semantics.sem_params -> (AST.ident List.list ->
    158158    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    159 let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_55 =
    160   let { globals = globals0; ev_genv = ev_genv0 } = x_55 in
     159let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_3 =
     160  let { globals = globals0; ev_genv = ev_genv0 } = x_3 in
    161161  h_mk_evaluation_params globals0 ev_genv0
    162162
     
    164164    Joint_semantics.sem_params -> (AST.ident List.list ->
    165165    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    166 let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_57 =
    167   let { globals = globals0; ev_genv = ev_genv0 } = x_57 in
     166let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_5 =
     167  let { globals = globals0; ev_genv = ev_genv0 } = x_5 in
    168168  h_mk_evaluation_params globals0 ev_genv0
    169169
     
    171171    Joint_semantics.sem_params -> (AST.ident List.list ->
    172172    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    173 let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_59 =
    174   let { globals = globals0; ev_genv = ev_genv0 } = x_59 in
     173let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_7 =
     174  let { globals = globals0; ev_genv = ev_genv0 } = x_7 in
    175175  h_mk_evaluation_params globals0 ev_genv0
    176176
     
    178178    Joint_semantics.sem_params -> (AST.ident List.list ->
    179179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    180 let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_61 =
    181   let { globals = globals0; ev_genv = ev_genv0 } = x_61 in
     180let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_9 =
     181  let { globals = globals0; ev_genv = ev_genv0 } = x_9 in
    182182  h_mk_evaluation_params globals0 ev_genv0
    183183
     
    185185    Joint_semantics.sem_params -> (AST.ident List.list ->
    186186    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    187 let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_63 =
    188   let { globals = globals0; ev_genv = ev_genv0 } = x_63 in
     187let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_11 =
     188  let { globals = globals0; ev_genv = ev_genv0 } = x_11 in
    189189  h_mk_evaluation_params globals0 ev_genv0
    190190
     
    192192    Joint_semantics.sem_params -> (AST.ident List.list ->
    193193    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    194 let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_65 =
    195   let { globals = globals0; ev_genv = ev_genv0 } = x_65 in
     194let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_13 =
     195  let { globals = globals0; ev_genv = ev_genv0 } = x_13 in
    196196  h_mk_evaluation_params globals0 ev_genv0
    197197
     
    336336    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    337337    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    338 let rec prog_params_rect_Type4 h_mk_prog_params x_81 =
     338let rec prog_params_rect_Type4 h_mk_prog_params x_29 =
    339339  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    340     stack_sizes0 } = x_81
     340    stack_sizes0 } = x_29
    341341  in
    342342  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    345345    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    346346    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    347 let rec prog_params_rect_Type5 h_mk_prog_params x_83 =
     347let rec prog_params_rect_Type5 h_mk_prog_params x_31 =
    348348  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    349     stack_sizes0 } = x_83
     349    stack_sizes0 } = x_31
    350350  in
    351351  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    354354    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    355355    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    356 let rec prog_params_rect_Type3 h_mk_prog_params x_85 =
     356let rec prog_params_rect_Type3 h_mk_prog_params x_33 =
    357357  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    358     stack_sizes0 } = x_85
     358    stack_sizes0 } = x_33
    359359  in
    360360  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    363363    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    364364    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    365 let rec prog_params_rect_Type2 h_mk_prog_params x_87 =
     365let rec prog_params_rect_Type2 h_mk_prog_params x_35 =
    366366  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    367     stack_sizes0 } = x_87
     367    stack_sizes0 } = x_35
    368368  in
    369369  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    372372    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    373373    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    374 let rec prog_params_rect_Type1 h_mk_prog_params x_89 =
     374let rec prog_params_rect_Type1 h_mk_prog_params x_37 =
    375375  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    376     stack_sizes0 } = x_89
     376    stack_sizes0 } = x_37
    377377  in
    378378  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    381381    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    382382    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    383 let rec prog_params_rect_Type0 h_mk_prog_params x_91 =
     383let rec prog_params_rect_Type0 h_mk_prog_params x_39 =
    384384  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    385     stack_sizes0 } = x_91
     385    stack_sizes0 } = x_39
    386386  in
    387387  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    674674       (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
    675675     in
    676      Errors.res_to_opt
    677        (Obj.magic
    678          (Monad.m_bind0 (Monad.max_def Errors.res0)
    679            (Obj.magic
    680              (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
    681                pars.globals
    682                (let p0 = Joint_semantics.spp'__o__spp p in
    683                let globals0 = pars.globals in
    684                let g = ge in g.Joint_semantics.ge) ret
    685                st.Joint_semantics.st_no_pc)) (fun vals ->
    686            Obj.magic (ByteValues.word_of_list_beval vals))))
     676     (match Obj.magic
     677              (Monad.m_bind0 (Monad.max_def Errors.res0)
     678                (Obj.magic
     679                  (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
     680                    pars.globals
     681                    (let p0 = Joint_semantics.spp'__o__spp p in
     682                    let globals0 = pars.globals in
     683                    let g = ge in g.Joint_semantics.ge) ret
     684                    st.Joint_semantics.st_no_pc)) (fun vals ->
     685                Obj.magic (ByteValues.word_of_list_beval vals))) with
     686      | Errors.OK v -> Types.Some v
     687      | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize))
    687688   | Bool.False -> Types.None)
    688689
  • src/joint/Traces.ma

    r2952 r2967  
    235235 if eq_program_counter (pc … st) exit_pc' then
    236236   let ret ≝ call_dest_for_main ?? p in
    237    res_to_opt … (! vals ← read_result … ge ret st ;
     237   match (! vals ← read_result … ge ret st ;
    238238               Word_of_list_beval vals)
     239   with
     240   [ OK v ⇒ Some ? v
     241   | Error _ ⇒ Some … (maximum ?) ]
    239242 else None ?.
    240243
Note: See TracChangeset for help on using the changeset viewer.