include "Clight/Cexec.ma". include "common/Animation.ma". definition myprog := mk_program (λ_.clight_fundef) ((list init_data) × type) [] [〈ident_of_nat 0 (* search *), CL_Internal ( mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ] (Ssequence (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) (Tint I8 Unsigned ))) (Ssequence (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Ebinop Osub (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned ))) (Tint I32 Signed )) (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) (Tint I32 Signed ))) (Tint I8 Unsigned ))) (Ssequence (Swhile (Expr (Ebinop Oge (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) (Tint I32 Signed )) (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) (Tint I32 Signed ))) (Tint I32 Signed )) (Ssequence (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Ebinop Odiv (Expr (Ebinop Oadd (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) (Tint I32 Signed )) (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) (Tint I32 Signed ))) (Tint I32 Signed )) (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) (Tint I32 Signed ))) (Tint I8 Unsigned ))) (Ssequence (Sifthenelse (Expr (Ebinop Oeq (Expr (Ecast (Tint I32 Signed ) (Expr (Ederef (Expr (Ebinop Oadd (Expr (Evar (ident_of_nat 4)) (Tpointer Any (Tint I8 Unsigned ))) (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))) (Tint I32 Signed )) (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned ))) (Tint I32 Signed ))) (Tint I32 Signed )) (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))) Sskip) (Ssequence (Sifthenelse (Expr (Ebinop Ogt (Expr (Ecast (Tint I32 Signed ) (Expr (Ederef (Expr (Ebinop Oadd (Expr (Evar (ident_of_nat 4)) (Tpointer Any (Tint I8 Unsigned ))) (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))) (Tint I32 Signed )) (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned ))) (Tint I32 Signed ))) (Tint I32 Signed )) (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Ebinop Osub (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) (Tint I32 Signed )) (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) (Tint I32 Signed ))) (Tint I8 Unsigned ))) Sskip) (Sifthenelse (Expr (Ebinop Olt (Expr (Ecast (Tint I32 Signed ) (Expr (Ederef (Expr (Ebinop Oadd (Expr (Evar (ident_of_nat 4)) (Tpointer Any (Tint I8 Unsigned ))) (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))) (Tint I32 Signed )) (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned ))) (Tint I32 Signed ))) (Tint I32 Signed )) (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Ebinop Oadd (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) (Tint I32 Signed )) (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) (Tint I32 Signed ))) (Tint I8 Unsigned ))) Sskip))))) (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned ) (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) (Tint I32 Signed ))) (Tint I8 Unsigned ))))))) )〉; 〈ident_of_nat 7 (* main *), CL_Internal ( mk_function (Tint I32 Signed ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ] (Ssequence (Sassign (Expr (Ederef (Expr (Ebinop Oadd (Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5)) (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) (Tint I8 Unsigned ))) (Ssequence (Sassign (Expr (Ederef (Expr (Ebinop Oadd (Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5)) (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed ))) (Tint I8 Unsigned ))) (Ssequence (Sassign (Expr (Ederef (Expr (Ebinop Oadd (Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5)) (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed ))) (Tint I8 Unsigned ))) (Ssequence (Sassign (Expr (Ederef (Expr (Ebinop Oadd (Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5)) (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))) (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed ))) (Tint I8 Unsigned ))) (Ssequence (Sassign (Expr (Ederef (Expr (Ebinop Oadd (Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5)) (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed ))) (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned )) (Expr (Ecast (Tint I8 Unsigned ) (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed ))) (Tint I8 Unsigned ))) (Ssequence (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned ))) (Expr (Evar (ident_of_nat 0)) (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned ))) [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5)); (Expr (Ecast (Tint I8 Unsigned ) (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed ))) (Tint I8 Unsigned )); (Expr (Ecast (Tint I8 Unsigned ) (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed ))) (Tint I8 Unsigned ))]) (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed ) (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned ))) (Tint I32 Signed )))))))))) )〉] (ident_of_nat 7) . example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]). normalize (* you can examine the result here *) @refl qed. include "Clight/toCminor.ma". include "Cminor/semantics.ma". example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])). (* example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]). *) normalize @refl qed. include "Cminor/toRTLabs.ma". include "RTLabs/semantics.ma". example e2: finishes_with (repr 3) ? ( do p1 ← clight_to_cminor myprog; bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ])). (* example e2: finishes_with (repr 3) ? ( do p1 ← clight_to_cminor myprog; do p2 ← cminor_to_rtlabs p1; exec_up_to RTLabs_fullexec p2 1000 [ ]).*) normalize @refl qed. (* example csc: True. letin yyy ≝ ( let xxx ≝ (clight_to_cminor myprog) in do p ← xxx ; cminor_to_rtlabs p) normalize in yyy; include "RTLabs/RTLabsToRTL.ma". example csc: True. letin xxx ≝ (clight_to_cminor myprog) letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p) letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p) @⊥ normalize in xxx; *)