working/0.2/funCallScript.sml

167     saved_regs_list = [isR 0; isR 1; isR 2; isR 3; isR 4; isR 5; isR 6; isR 7; isR 8; isR fp; isR ip; isR lr]`;
172        MSUB R11 R12 (MC 1w)]                   (* sub fp ip 1 *)
286       fp | saved sp |
287          | saved fp |
642 (*   We need to keep track of how sp,fp and ip are changed.                        *)
643 (*   Note that r0-r8,fp,ip and lr are also pushed into the stack                   *)
857         run_cfl (BLK [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]) st)`,
880       run_cfl (BLK ((MSUB R13 R13 (MC (n2w k))) :: (APPEND (push_list l) [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]))) st)`,
895       [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++
915    `MSUB R13 R13 (MC (n2w k))::push_list (MAP conv_exp caller_i) ++ [MPUSH 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++
917     MSUB R13 R13 (MC (n2w k))::(push_list (MAP conv_exp caller_i) ++ [MPUSH 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]])
1058       [MSUB R13 R11 (MC 11w)] ++                      (* sub sp fp 12 *)
1059       [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++
1203       (run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) (regs,mem) =
1263       let st' = run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st in
1305      ((run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l')) st) ''
1309     Q.ABBREV_TAC `st1 = run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st` THEN
1353              ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++
1404     Q.ABBREV_TAC `st1 = run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st` THEN
1437      (st '' isM (w2n x - 1) = st0 '' isR fp) /\ (st '' isM (w2n x - 2) = st0 '' isR 8) /\
1460        let st' = run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]))) st in
1473     `(st '' isM (w2n x) = st0 '' isR ip) /\ (st '' isM (w2n x - 1) = st0 '' isR fp)` by
1487        let st' = run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l'))) st in
1524       ((run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l'))) st) ''
1528     `w2n (read (run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st) FP) = w2n(read st0 FP)`
1572            ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list (MAP conv_exp caller_o))))
1616           ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list (MAP conv_exp caller_o)))) st
1680         [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN
1706         [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN
1734         [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN
1901 (*  The values fp,ip and sp are recovered after the function call;                 *)