Changeset 2903
- Timestamp:
- Mar 19, 2013, 1:25:59 AM (8 years ago)
- Location:
- extracted
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/measurable.ml
r2890 r2903 254 254 let intensional_events_of_events tr = 255 255 List.flatten (List.map intensional_event_of_event tr) 256 257 (** val intensional_state_change : 258 classified_system -> AST.ident List.list -> __ -> (AST.ident List.list, 259 StructuredTraces.intensional_event List.list) Types.prod **) 260 let intensional_state_change c callstack s = 261 (match c.cs_classify s with 262 | StructuredTraces.Cl_return -> 263 (fun x -> 264 match callstack with 265 | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil } 266 | List.Cons (id, tl) -> 267 { Types.fst = tl; Types.snd = (List.Cons ((StructuredTraces.IEVret 268 id), List.Nil)) }) 269 | StructuredTraces.Cl_jump -> 270 (fun x -> { Types.fst = callstack; Types.snd = List.Nil }) 271 | StructuredTraces.Cl_call -> 272 (fun callee -> 273 let id = callee __ in 274 { Types.fst = (List.Cons (id, callstack)); Types.snd = (List.Cons 275 ((StructuredTraces.IEVcall id), List.Nil)) }) 276 | StructuredTraces.Cl_tailcall -> 277 (fun x -> { Types.fst = callstack; Types.snd = List.Nil }) 278 | StructuredTraces.Cl_other -> 279 (fun x -> { Types.fst = callstack; Types.snd = List.Nil })) (fun _ -> 280 cs_callee0 c s) 256 281 257 282 (** val intensional_trace_of_trace : … … 264 289 let { Types.fst = s; Types.snd = tr } = str in 265 290 let { Types.fst = callstack0; Types.snd = call_event } = 266 (match c.cs_classify s with 267 | StructuredTraces.Cl_return -> 268 (fun x -> 269 match callstack with 270 | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil } 271 | List.Cons (id, tl0) -> 272 { Types.fst = tl0; Types.snd = (List.Cons 273 ((StructuredTraces.IEVret id), List.Nil)) }) 274 | StructuredTraces.Cl_jump -> 275 (fun x -> { Types.fst = callstack; Types.snd = List.Nil }) 276 | StructuredTraces.Cl_call -> 277 (fun callee -> 278 let id = callee __ in 279 { Types.fst = (List.Cons (id, callstack)); Types.snd = (List.Cons 280 ((StructuredTraces.IEVcall id), List.Nil)) }) 281 | StructuredTraces.Cl_tailcall -> 282 (fun x -> { Types.fst = callstack; Types.snd = List.Nil }) 283 | StructuredTraces.Cl_other -> 284 (fun x -> { Types.fst = callstack; Types.snd = List.Nil })) (fun _ -> 285 cs_callee0 c s) 291 intensional_state_change c callstack s 286 292 in 287 293 let other_events = intensional_events_of_events tr in -
extracted/measurable.mli
r2803 r2903 185 185 Events.trace -> StructuredTraces.intensional_event List.list 186 186 187 val intensional_state_change : 188 classified_system -> AST.ident List.list -> __ -> (AST.ident List.list, 189 StructuredTraces.intensional_event List.list) Types.prod 190 187 191 val intensional_trace_of_trace : 188 192 classified_system -> AST.ident List.list -> (cs_state, Events.trace) -
extracted/rTLabs_abstract.ml
r2873 r2903 541 541 (match s' with 542 542 | RTLabs_semantics.State (f, x, x0) -> 543 (fun _ _ -> assert false (* absurd case *)) 544 | RTLabs_semantics.Callstate (x, fd, x0, x1, x2, x3) -> 545 (match stk with 546 | List.Nil -> (fun _ _ -> assert false (* absurd case *)) 547 | List.Cons (b, x4) -> 548 (fun _ _ _ -> Globalenvs.symbol_of_function_block ge b)) __ 543 (fun _ -> assert false (* absurd case *)) 544 | RTLabs_semantics.Callstate (fid, x, x0, x1, x2, x3) -> (fun _ -> fid) 549 545 | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> 550 (fun _ _-> assert false (* absurd case *))546 (fun _ -> assert false (* absurd case *)) 551 547 | RTLabs_semantics.Finalstate x -> 552 (fun _ _ -> assert false (* absurd case *))) __) __548 (fun _ -> assert false (* absurd case *)))) __ 553 549 554 550 (** val rTLabs_status : -
extracted/rTLabs_semantics.ml
r2827 r2903 777 777 Registers.register Types.option -> frame List.list -> GenMem.mem -> 778 778 Pointers.block Types.sig0 **) 779 let func_block_of_exec ge clearme t vffd args dst fs m =779 let func_block_of_exec ge clearme t fid fd args dst fs m = 780 780 (match clearme with 781 781 | State (clearme0, x, x0) -> … … 783 783 dst0 } = clearme0 784 784 in 785 (fun fs0 m0 tr fid fd0 args0 dst' fs' m' ->785 (fun fs0 m0 tr fid0 fd0 args0 dst' fs' m' -> 786 786 (match next_instruction { func = func0; locals = locals0; next = next0; 787 787 sp = sp0; retdst = dst0 } with … … 791 791 (build_state { func = func0; locals = locals0; next = next0; sp = 792 792 sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst = 793 tr; Types.snd = (Callstate (fid , fd0, args0, dst', fs', m')) })793 tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) 794 794 (fun _ -> 795 795 Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst = … … 797 797 (build_state { func = func0; locals = locals0; next = next0; 798 798 sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value 799 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,799 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 800 800 dst', fs', m')) }) __ (fun _ -> 801 801 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; … … 803 803 (build_state { func = func0; locals = locals0; next = next0; 804 804 sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr; 805 Types.snd = (Callstate (fid , fd0, args0, dst', fs', m')) } __806 (fun _ ->805 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } 806 __ (fun _ -> 807 807 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> 808 808 Obj.magic state_jmdiscr (State 809 809 ((adv l { func = func0; locals = locals0; next = next0; 810 sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid,811 fd0, args0, dst', fs', m')) __) tr __ __))))810 sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate 811 (fid0, fd0, args0, dst', fs', m')) __) tr __ __)))) 812 812 | RTLabs_syntax.St_cost (c, l) -> 813 813 (fun _ _ -> … … 816 816 (build_state { func = func0; locals = locals0; next = next0; sp = 817 817 sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst = 818 tr; Types.snd = (Callstate (fid , fd0, args0, dst', fs', m')) })818 tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) 819 819 (fun _ -> 820 820 Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst = … … 822 822 (build_state { func = func0; locals = locals0; next = next0; 823 823 sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value 824 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,824 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 825 825 dst', fs', m')) }) __ (fun _ -> 826 826 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = … … 828 828 (build_state { func = func0; locals = locals0; next = next0; 829 829 sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr; 830 Types.snd = (Callstate (fid , fd0, args0, dst', fs', m')) } __831 (fun _ ->830 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } 831 __ (fun _ -> 832 832 Logic.eq_rect_Type0 (List.Cons ((Events.EVcost c), List.Nil)) 833 833 (fun _ _ _ -> 834 834 Obj.magic state_jmdiscr (State 835 835 ((adv l { func = func0; locals = locals0; next = next0; 836 sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid,837 fd0, args0, dst', fs', m')) __) tr __ __))))836 sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate 837 (fid0, fd0, args0, dst', fs', m')) __) tr __ __)))) 838 838 | RTLabs_syntax.St_const (t0, r, c, l) -> 839 839 (fun _ _ -> … … 848 848 Events.e0; Types.snd = (State ({ func = func0; locals = 849 849 locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))) 850 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0, dst',850 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', 851 851 fs', m')) } (fun v _ _ -> 852 852 bind_ok (reg_store r v locals0) (fun x1 -> … … 855 855 Events.e0; Types.snd = (State ({ func = func0; locals = x1; 856 856 next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })) 857 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,857 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 858 858 dst', fs', m')) } (fun locals' _ _ -> 859 859 jmeq_hackT … … 862 862 locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) 863 863 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 864 (Callstate (fid , fd0, args0, dst', fs', m')) })) (fun _ ->864 (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> 865 865 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = 866 866 Events.e0; Types.snd = (State ({ func = func0; locals = 867 867 locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) 868 (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid ,868 (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, 869 869 fd0, args0, dst', fs', m')) }) __ (fun _ -> 870 870 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; 871 871 Types.snd = (State ({ func = func0; locals = locals'; 872 872 next = l; sp = sp0; retdst = dst0 }, fs0, m0)) } 873 { Types.fst = tr; Types.snd = (Callstate (fid , fd0,873 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, 874 874 args0, dst', fs', m')) } __ (fun _ -> 875 875 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> 876 876 Obj.magic state_jmdiscr (State ({ func = func0; 877 877 locals = locals'; next = l; sp = sp0; retdst = 878 dst0 }, fs0, m0)) (Callstate (fid , fd0, args0, dst',878 dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0, dst', 879 879 fs', m')) __) tr __ __)))))) 880 880 | RTLabs_syntax.St_op1 (t1, t2, op, r1, r2, l) -> … … 891 891 Events.e0; Types.snd = (State ({ func = func0; locals = 892 892 locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))) 893 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0, dst',893 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', 894 894 fs', m')) } (fun v _ _ -> 895 895 bind_ok … … 902 902 Events.e0; Types.snd = (State ({ func = func0; locals = 903 903 locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))) 904 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,904 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 905 905 dst', fs', m')) } (fun v' _ _ -> 906 906 bind_ok (reg_store r1 v' locals0) (fun x1 -> … … 909 909 Events.e0; Types.snd = (State ({ func = func0; locals = 910 910 x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })) 911 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,911 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 912 912 dst', fs', m')) } (fun loc _ _ -> 913 913 jmeq_hackT … … 916 916 loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) 917 917 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 918 (Callstate (fid , fd0, args0, dst', fs', m')) }))918 (Callstate (fid0, fd0, args0, dst', fs', m')) })) 919 919 (fun _ -> 920 920 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = 921 921 Events.e0; Types.snd = (State ({ func = func0; locals = 922 922 loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) 923 (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,924 fd0, args0, dst', fs', m')) }) __ (fun _ ->923 (Errors.OK { Types.fst = tr; Types.snd = (Callstate 924 (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> 925 925 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = 926 926 Events.e0; Types.snd = (State ({ func = func0; locals = 927 927 loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) } 928 { Types.fst = tr; Types.snd = (Callstate (fid , fd0,928 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, 929 929 args0, dst', fs', m')) } __ (fun _ -> 930 930 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> 931 931 Obj.magic state_jmdiscr (State ({ func = func0; 932 932 locals = loc; next = l; sp = sp0; retdst = dst0 }, 933 fs0, m0)) (Callstate (fid , fd0, args0, dst', fs',933 fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', 934 934 m')) __) tr __ __))))))) 935 935 | RTLabs_syntax.St_op2 (t1, t2, t', op, r1, r2, r3, l) -> … … 950 950 locals1; next = l; sp = sp0; retdst = dst0 }, fs0, 951 951 m0)) }))))) { Types.fst = tr; Types.snd = (Callstate 952 (fid , fd0, args0, dst', fs', m')) } (fun v1 _ _ ->952 (fid0, fd0, args0, dst', fs', m')) } (fun v1 _ _ -> 953 953 bind_ok (reg_retrieve locals0 r3) (fun x1 -> 954 954 Obj.magic … … 964 964 locals1; next = l; sp = sp0; retdst = dst0 }, fs0, 965 965 m0)) })))) { Types.fst = tr; Types.snd = (Callstate 966 (fid , fd0, args0, dst', fs', m')) } (fun v2 _ _ ->966 (fid0, fd0, args0, dst', fs', m')) } (fun v2 _ _ -> 967 967 bind_ok 968 968 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) … … 975 975 locals1; next = l; sp = sp0; retdst = dst0 }, fs0, 976 976 m0)) }))) { Types.fst = tr; Types.snd = (Callstate 977 (fid , fd0, args0, dst', fs', m')) } (fun v' _ _ ->977 (fid0, fd0, args0, dst', fs', m')) } (fun v' _ _ -> 978 978 bind_ok (reg_store r1 v' locals0) (fun x1 -> 979 979 Obj.magic … … 982 982 func0; locals = x1; next = l; sp = sp0; retdst = 983 983 dst0 }, fs0, m0)) })) { Types.fst = tr; Types.snd = 984 (Callstate (fid , fd0, args0, dst', fs', m')) }984 (Callstate (fid0, fd0, args0, dst', fs', m')) } 985 985 (fun loc _ _ -> 986 986 jmeq_hackT … … 990 990 dst0 }, fs0, m0)) }) 991 991 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 992 (Callstate (fid , fd0, args0, dst', fs', m')) }))992 (Callstate (fid0, fd0, args0, dst', fs', m')) })) 993 993 (fun _ -> 994 994 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = … … 996 996 loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) 997 997 (Errors.OK { Types.fst = tr; Types.snd = (Callstate 998 (fid , fd0, args0, dst', fs', m')) }) __ (fun _ ->998 (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> 999 999 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = 1000 1000 Events.e0; Types.snd = (State ({ func = func0; 1001 1001 locals = loc; next = l; sp = sp0; retdst = dst0 }, 1002 1002 fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate 1003 (fid , fd0, args0, dst', fs', m')) } __ (fun _ ->1003 (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> 1004 1004 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> 1005 1005 Obj.magic state_jmdiscr (State ({ func = func0; 1006 1006 locals = loc; next = l; sp = sp0; retdst = 1007 dst0 }, fs0, m0)) (Callstate (fid , fd0, args0,1007 dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0, 1008 1008 dst', fs', m')) __) tr __ __)))))))) 1009 1009 | RTLabs_syntax.St_load (ch, r1, r2, l) -> … … 1020 1020 Events.e0; Types.snd = (State ({ func = func0; locals = 1021 1021 locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))) 1022 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0, dst',1022 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', 1023 1023 fs', m')) } (fun v _ _ -> 1024 1024 bind_ok … … 1031 1031 Events.e0; Types.snd = (State ({ func = func0; locals = 1032 1032 locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))) 1033 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,1033 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 1034 1034 dst', fs', m')) } (fun v' _ _ -> 1035 1035 bind_ok (reg_store r2 v' locals0) (fun x1 -> … … 1038 1038 Events.e0; Types.snd = (State ({ func = func0; locals = 1039 1039 x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })) 1040 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,1040 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 1041 1041 dst', fs', m')) } (fun loc _ _ -> 1042 1042 jmeq_hackT … … 1045 1045 loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) 1046 1046 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 1047 (Callstate (fid , fd0, args0, dst', fs', m')) }))1047 (Callstate (fid0, fd0, args0, dst', fs', m')) })) 1048 1048 (fun _ -> 1049 1049 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = 1050 1050 Events.e0; Types.snd = (State ({ func = func0; locals = 1051 1051 loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) 1052 (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,1053 fd0, args0, dst', fs', m')) }) __ (fun _ ->1052 (Errors.OK { Types.fst = tr; Types.snd = (Callstate 1053 (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> 1054 1054 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = 1055 1055 Events.e0; Types.snd = (State ({ func = func0; locals = 1056 1056 loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) } 1057 { Types.fst = tr; Types.snd = (Callstate (fid , fd0,1057 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, 1058 1058 args0, dst', fs', m')) } __ (fun _ -> 1059 1059 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> 1060 1060 Obj.magic state_jmdiscr (State ({ func = func0; 1061 1061 locals = loc; next = l; sp = sp0; retdst = dst0 }, 1062 fs0, m0)) (Callstate (fid , fd0, args0, dst', fs',1062 fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', 1063 1063 m')) __) tr __ __))))))) 1064 1064 | RTLabs_syntax.St_store (ch, r1, r2, l) -> … … 1076 1076 (build_state { func = func0; locals = locals0; next = 1077 1077 next0; sp = sp0; retdst = dst0 } fs0 m'0 l) })))) 1078 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0, dst',1078 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', 1079 1079 fs', m')) } (fun v _ _ -> 1080 1080 bind_ok (reg_retrieve locals0 r2) (fun x1 -> … … 1088 1088 (build_state { func = func0; locals = locals0; next = 1089 1089 next0; sp = sp0; retdst = dst0 } fs0 m'0 l) }))) 1090 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,1090 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 1091 1091 dst', fs', m')) } (fun v' _ _ -> 1092 1092 bind_ok … … 1098 1098 (build_state { func = func0; locals = locals0; next = 1099 1099 next0; sp = sp0; retdst = dst0 } fs0 x1 l) })) 1100 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,1100 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 1101 1101 dst', fs', m')) } (fun loc _ _ -> 1102 1102 jmeq_hackT … … 1106 1106 next0; sp = sp0; retdst = dst0 } fs0 loc l) }) 1107 1107 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 1108 (Callstate (fid , fd0, args0, dst', fs', m')) }))1108 (Callstate (fid0, fd0, args0, dst', fs', m')) })) 1109 1109 (fun _ -> 1110 1110 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = … … 1112 1112 (build_state { func = func0; locals = locals0; next = 1113 1113 next0; sp = sp0; retdst = dst0 } fs0 loc l) }) 1114 (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,1115 fd0, args0, dst', fs', m')) }) __ (fun _ ->1114 (Errors.OK { Types.fst = tr; Types.snd = (Callstate 1115 (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> 1116 1116 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = 1117 1117 Events.e0; Types.snd = 1118 1118 (build_state { func = func0; locals = locals0; next = 1119 1119 next0; sp = sp0; retdst = dst0 } fs0 loc l) } 1120 { Types.fst = tr; Types.snd = (Callstate (fid , fd0,1120 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, 1121 1121 args0, dst', fs', m')) } __ (fun _ -> 1122 1122 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> … … 1124 1124 ((adv l { func = func0; locals = locals0; next = 1125 1125 next0; sp = sp0; retdst = dst0 }), fs0, loc)) 1126 (Callstate (fid , fd0, args0, dst', fs', m')) __) tr1127 __ __)))))))1126 (Callstate (fid0, fd0, args0, dst', fs', m')) __) 1127 tr __ __))))))) 1128 1128 | RTLabs_syntax.St_call_id (x1, rs, or0, l) -> 1129 1129 (fun _ _ -> … … 1148 1148 ((adv l { func = func0; locals = locals0; next = next0; 1149 1149 sp = sp0; retdst = dst0 }), fs0)), m0)) })))) 1150 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0, dst',1150 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', 1151 1151 fs', m')) } (fun v _ _ -> 1152 1152 bind_ok … … 1164 1164 ((adv l { func = func0; locals = locals0; next = next0; 1165 1165 sp = sp0; retdst = dst0 }), fs0)), m0)) }))) 1166 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,1166 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 1167 1167 dst', fs', m')) } (fun fd' _ _ -> 1168 1168 bind_ok … … 1176 1176 ((adv l { func = func0; locals = locals0; next = next0; 1177 1177 sp = sp0; retdst = dst0 }), fs0)), m0)) })) 1178 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,1178 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 1179 1179 dst', fs', m')) } (fun vs _ _ -> 1180 1180 jmeq_hackT … … 1185 1185 sp = sp0; retdst = dst0 }), fs0)), m0)) }) 1186 1186 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 1187 (Callstate (fid , fd0, args0, dst', fs', m')) }))1187 (Callstate (fid0, fd0, args0, dst', fs', m')) })) 1188 1188 (fun _ -> 1189 1189 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = … … 1191 1191 (List.Cons ({ func = func0; locals = locals0; next = l; 1192 1192 sp = sp0; retdst = dst0 }, fs0)), m0)) }) (Errors.OK 1193 { Types.fst = tr; Types.snd = (Callstate (fid , fd0,1193 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, 1194 1194 args0, dst', fs', m')) }) __ (fun _ -> 1195 1195 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil; … … 1197 1197 ({ func = func0; locals = locals0; next = l; sp = sp0; 1198 1198 retdst = dst0 }, fs0)), m0)) } { Types.fst = tr; 1199 Types.snd = (Callstate (fid , fd0, args0, dst', fs',1199 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', 1200 1200 m')) } __ (fun _ -> 1201 1201 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> … … 1203 1203 (List.Cons ({ func = func0; locals = locals0; 1204 1204 next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) 1205 (Callstate (fid , fd0, args0, dst', fs', m')) __1205 (Callstate (fid0, fd0, args0, dst', fs', m')) __ 1206 1206 (fun _ -> 1207 Extralib.eq_rect_Type0_r fid (fun _ _ _ _ _ _ _ ->1207 Extralib.eq_rect_Type0_r fid0 (fun _ _ _ _ _ _ _ -> 1208 1208 Extralib.eq_rect_Type0_r fd0 (fun _ _ _ _ _ -> 1209 1209 Extralib.eq_rect_Type0_r args0 … … 1218 1218 Logic.streicherK (Errors.OK 1219 1219 { Types.fst = List.Nil; Types.snd = 1220 (Callstate (fid , fd0, args0, dst',1220 (Callstate (fid0, fd0, args0, dst', 1221 1221 (List.Cons ({ func = func0; locals = 1222 1222 locals0; next = l; sp = sp0; retdst = … … 1224 1224 (Logic.streicherK { Types.fst = 1225 1225 List.Nil; Types.snd = (Callstate 1226 (fid , fd0, args0, dst', (List.Cons1226 (fid0, fd0, args0, dst', (List.Cons 1227 1227 ({ func = func0; locals = locals0; 1228 1228 next = l; sp = sp0; retdst = 1229 1229 dst0 }, fs0)), m')) } 1230 (Logic.streicherK (Callstate (fid ,1230 (Logic.streicherK (Callstate (fid0, 1231 1231 fd0, args0, dst', (List.Cons 1232 1232 ({ func = func0; locals = … … 1252 1252 ((adv l { func = func0; locals = locals0; next = next0; 1253 1253 sp = sp0; retdst = dst0 }), fs0)), m0)) })))) 1254 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0, dst',1254 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', 1255 1255 fs', m')) } (fun v _ _ -> 1256 1256 bind_ok … … 1266 1266 ((adv l { func = func0; locals = locals0; next = next0; 1267 1267 sp = sp0; retdst = dst0 }), fs0)), m0)) }))) 1268 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,1268 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 1269 1269 dst', fs', m')) } (fun fd' _ _ -> 1270 1270 bind_ok … … 1278 1278 ((adv l { func = func0; locals = locals0; next = next0; 1279 1279 sp = sp0; retdst = dst0 }), fs0)), m0)) })) 1280 { Types.fst = tr; Types.snd = (Callstate (fid , fd0, args0,1280 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, 1281 1281 dst', fs', m')) } (fun vs _ _ -> 1282 1282 jmeq_hackT … … 1287 1287 sp = sp0; retdst = dst0 }), fs0)), m0)) }) 1288 1288 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 1289 (Callstate (fid , fd0, args0, dst', fs', m')) }))1289 (Callstate (fid0, fd0, args0, dst', fs', m')) })) 1290 1290 (fun _ -> 1291 1291 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = … … 1294 1294 locals = locals0; next = l; sp = sp0; retdst = dst0 }, 1295 1295 fs0)), m0)) }) (Errors.OK { Types.fst = tr; Types.snd = 1296 (Callstate (fid , fd0, args0, dst', fs', m')) }) __1296 (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ 1297 1297 (fun _ -> 1298 1298 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil; … … 1300 1300 vs, or0, (List.Cons ({ func = func0; locals = locals0; 1301 1301 next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) } 1302 { Types.fst = tr; Types.snd = (Callstate (fid , fd0,1302 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, 1303 1303 args0, dst', fs', m')) } __ (fun _ -> 1304 1304 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> … … 1306 1306 fd'.Types.fst, vs, or0, (List.Cons ({ func = func0; 1307 1307 locals = locals0; next = l; sp = sp0; retdst = 1308 dst0 }, fs0)), m0)) (Callstate (fid , fd0, args0,1308 dst0 }, fs0)), m0)) (Callstate (fid0, fd0, args0, 1309 1309 dst', fs', m')) __ (fun _ -> 1310 1310 Logic.eq_rect_Type0 fd'.Types.snd (fun _ _ _ _ -> … … 1374 1374 (fun _ -> b)) __)))) m0 __ __ 1375 1375 __) fs' __ __ __) or0 __ __ __ __) vs 1376 __ __ __ __) fd0 __ __ __) fid __ __ __)) tr1376 __ __ __ __) fd0 __ __ __) fid0 __ __ __)) tr 1377 1377 __ __))))))) 1378 1378 | RTLabs_syntax.St_cond (r, l1, l2) -> … … 1389 1389 | Bool.True -> l1 1390 1390 | Bool.False -> l2)) }))) { Types.fst = tr; Types.snd = 1391 (Callstate (fid , fd0, args0, dst', fs', m')) } (fun v _ _ ->1391 (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ -> 1392 1392 bind_ok (Values.eval_bool_of_val v) (fun x1 -> 1393 1393 Obj.magic … … 1399 1399 | Bool.True -> l1 1400 1400 | Bool.False -> l2)) })) { Types.fst = tr; Types.snd = 1401 (Callstate (fid , fd0, args0, dst', fs', m')) } (fun b _ _ ->1401 (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun b _ _ -> 1402 1402 jmeq_hackT 1403 1403 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = … … 1409 1409 | Bool.False -> l2)) }) 1410 1410 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 1411 (Callstate (fid , fd0, args0, dst', fs', m')) })) (fun _ ->1411 (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> 1412 1412 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = 1413 1413 Events.e0; Types.snd = … … 1417 1417 | Bool.True -> l1 1418 1418 | Bool.False -> l2)) }) (Errors.OK { Types.fst = tr; 1419 Types.snd = (Callstate (fid , fd0, args0, dst', fs', m')) })1420 __ (fun _ ->1419 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', 1420 m')) }) __ (fun _ -> 1421 1421 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; 1422 1422 Types.snd = … … 1426 1426 | Bool.True -> l1 1427 1427 | Bool.False -> l2)) } { Types.fst = tr; Types.snd = 1428 (Callstate (fid , fd0, args0, dst', fs', m')) } __1428 (Callstate (fid0, fd0, args0, dst', fs', m')) } __ 1429 1429 (fun _ -> 1430 1430 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> … … 1435 1435 | Bool.False -> l2) { func = func0; locals = 1436 1436 locals0; next = next0; sp = sp0; retdst = dst0 }), 1437 fs0, m0)) (Callstate (fid , fd0, args0, dst', fs',1437 fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', 1438 1438 m')) __) tr __ __)))))) 1439 1439 | RTLabs_syntax.St_return -> … … 1455 1455 Events.e0; Types.snd = (Returnstate (v, dst0, fs0, 1456 1456 (GenMem.free m0 sp0))) })) { Types.fst = tr; Types.snd = 1457 (Callstate (fid , fd0, args0, dst', fs', m')) } (fun v ->1457 (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v -> 1458 1458 match func0.RTLabs_syntax.f_result with 1459 1459 | Types.None -> … … 1464 1464 (GenMem.free m0 sp0))) }) 1465 1465 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 1466 (Callstate (fid , fd0, args0, dst', fs', m')) }))1466 (Callstate (fid0, fd0, args0, dst', fs', m')) })) 1467 1467 (fun _ -> 1468 1468 Obj.magic Errors.res_discr (Errors.OK Types.None) … … 1471 1471 Events.e0; Types.snd = (Returnstate (v, dst0, fs0, 1472 1472 (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr; 1473 Types.snd = (Callstate (fid , fd0, args0, dst', fs',1473 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', 1474 1474 m')) }) __ (fun _ -> 1475 1475 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = 1476 1476 Events.e0; Types.snd = (Returnstate (v, dst0, fs0, 1477 1477 (GenMem.free m0 sp0))) } { Types.fst = tr; 1478 Types.snd = (Callstate (fid , fd0, args0, dst', fs',1478 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', 1479 1479 m')) } __ (fun _ -> 1480 1480 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> 1481 1481 Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0, 1482 (GenMem.free m0 sp0))) (Callstate (fid , fd0,1482 (GenMem.free m0 sp0))) (Callstate (fid0, fd0, 1483 1483 args0, dst', fs', m')) __) tr __ __))))) 1484 1484 | Types.Some clearme1 -> … … 1494 1494 (GenMem.free m0 sp0))) }) 1495 1495 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = 1496 (Callstate (fid , fd0, args0, dst', fs', m')) }))1496 (Callstate (fid0, fd0, args0, dst', fs', m')) })) 1497 1497 (fun _ -> 1498 1498 Obj.magic Errors.res_discr (Errors.OK (Types.Some v0)) … … 1501 1501 Events.e0; Types.snd = (Returnstate (v, dst0, fs0, 1502 1502 (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr; 1503 Types.snd = (Callstate (fid , fd0, args0, dst', fs',1503 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', 1504 1504 m')) }) __ (fun _ -> 1505 1505 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = 1506 1506 Events.e0; Types.snd = (Returnstate (v, dst0, fs0, 1507 1507 (GenMem.free m0 sp0))) } { Types.fst = tr; 1508 Types.snd = (Callstate (fid , fd0, args0, dst', fs',1508 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', 1509 1509 m')) } __ (fun _ -> 1510 1510 Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> 1511 1511 Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0, 1512 (GenMem.free m0 sp0))) (Callstate (fid , fd0,1512 (GenMem.free m0 sp0))) (Callstate (fid0, fd0, 1513 1513 args0, dst', fs', m')) __) tr __ __))))))))) __)) 1514 1514 x x0 1515 | Callstate (vf 0, clearme0, x, x0, x1, x2) ->1515 | Callstate (vf, clearme0, x, x0, x1, x2) -> 1516 1516 (match clearme0 with 1517 1517 | AST.Internal fn -> … … 1710 1710 ErrorMessages.FinalState), List.Nil))) (IOMonad.Value { Types.fst = 1711 1711 tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __)) 1712 t vffd args dst fs m __1713 1712 t fid fd args dst fs m __ 1713
Note: See TracChangeset
for help on using the changeset viewer.