Changeset 765

Timestamp:

Apr 20, 2011, 5:39:00 PM (9 years ago)

Author:

campbell

Message:

Remove superfluous register in RTLabs return statements.

Also fix up RTLabs prototype pretty printer's handling of global variables.

Location:

src/RTLabs

Files:

• RTLabsMatitaPrinter.ml (modified) (8 diffs)
• import.ma (modified) (1 diff)
• semantics.ma (modified) (5 diffs)
• syntax.ma (modified) (1 diff)
• test/search.ma (modified) (2 diffs)
• test/sum.ma (added)

src/RTLabs/RTLabsMatitaPrinter.ml

@@ +1 @@
+
+let next_id = ref 0
+let fresh () = let i = !next_id in next_id := i+1; i
 
 let n_spaces n = String.make n ' '
@@ -4 +7 @@
 
 let print_global (x, size) =
-  Printf.sprintf "pair ?? (pair ?? (pair ?? %s [ ]) Any) %d" x size
+  Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x size
 
 let print_globals n globs =
@@ -105 +108 @@
   | RTLabs.Aindexed off -> Printf.sprintf "Aindexed (repr %d)" off
   | RTLabs.Aindexed2 -> "Aindexed2"
-  | RTLabs.Aglobal (id, off) -> Printf.sprintf "Aglobal %s (repr %d)" id off
-  | RTLabs.Abased (id, off) -> Printf.sprintf "Abased %s (repr %d)" id off
+  | RTLabs.Aglobal (id, off) -> Printf.sprintf "Aglobal id_%s (repr %d)" id off
+  | RTLabs.Abased (id, off) -> Printf.sprintf "Abased id_%s (repr %d)" id off
   | RTLabs.Ainstack off -> Printf.sprintf "Ainstack (repr %d)" off
 
@@ -209 +212 @@
         (Register.print rs)
         (print_table tbl)
-  | RTLabs.St_return rs -> Printf.sprintf "make_St_return %s" (Register.print rs)
+  | RTLabs.St_return rs -> "make_St_return" (* rs should always be the function's result register, anyway *)
 
 let print_cost_labels n c =
@@ -246 +249 @@
   "[\n" ^ Label.Map.fold f c ""
 
-let print_internal_decl n f def m =
+let print_internal_decl n f def =
   Printf.sprintf
     "%sdefinition id_%s := ident_of_nat %d.\n%s%s\n\n%sdefinition pre_%s := mk_pre_internal_function\n%s(%s)\n%s(Some ? %s)\n%s%s\n%s%s\n%s%s\n%s%d\n%s%s\n%s%s\n%s%s."
     (n_spaces n)
     f
-    m
+    (fresh ())
     (print_labels n def.RTLabs.f_graph)
     (print_cost_labels n def.RTLabs.f_graph)
@@ -277 +280 @@
 
 
-let print_external_decl n f def m =
+let print_external_decl n f def =
   Printf.sprintf "%sdefinition id_%s := ident_of_nat %d.\n%sdefinition f_%s := External (mk_external_function id_%s (%s)).\n"
     (n_spaces n)
     f
-    m
+    (fresh ())
     (n_spaces n)
     f
@@ -288 +291 @@
 
 
-let print_fun_decl n (f, def) m = match def with
-  | RTLabs.F_int def -> print_internal_decl n f def m
-  | RTLabs.F_ext def -> print_external_decl n f def m
-
-let print_fun_decls n functs =
-  snd (List.fold_left (fun (i,s) f -> i+1, s ^ (print_fun_decl n f i) ^ "\n\n") (0,"")
-    functs)
+let print_fun_decl n (f, def) = match def with
+  | RTLabs.F_int def -> print_internal_decl n f def
+  | RTLabs.F_ext def -> print_external_decl n f def
+
+let print_fun_decls n =
+  List.fold_left (fun s f -> s ^ (print_fun_decl n f) ^ "\n\n") ""
 
 let print_fun n functs =
@@ -317 +319 @@
     (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
 
+let define_var_id (id,_) =
+  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
+
+let define_var_ids =
+  List.fold_left (fun s v -> s ^ (define_var_id v)) ""
+
 let print_program p =
-  Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n(*program:*)\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n(%s)\n%s\n%s\n).\n"
+  Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n(%s)\n%s\n%s\n).\n"
+    (define_var_ids p.RTLabs.vars)
     (print_fun_decls 2 p.RTLabs.functs)
     (print_fun 2 p.RTLabs.functs)

src/RTLabs/import.ma

@@ -121 +121 @@
 let rec make_St_cond2 op src1 src2 ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src1' ← r src1; do src2' ← r src2; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond2 op src1' src2' ltrue' lfalse').
 let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
-let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; OK statement (St_return src').
+definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return.
 

src/RTLabs/semantics.ma

@@ -37 +37 @@
    state
 | Returnstate :
-   ∀ rtv : val.
+   ∀ rtv : option val.
    ∀ dst : option register.
    ∀ stk : list frame.
@@ -177 +177 @@
       ]
 
-  | St_return src ⇒
-      ! v ← reg_retrieve (locals f) src;
+  | St_return ⇒
+      ! v ← match f_result (func f) with
+            [ None ⇒ ret ? (None ?)
+            | Some r ⇒ ! v ← reg_retrieve (locals f) r; ret ? (Some ? v)
+            ];
       ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
   ]
@@ -190 +193 @@
         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
         ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
-        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) dst fs m〉
-
+        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
     ]
 | Returnstate v dst fs m ⇒
@@ -197 +199 @@
     [ nil ⇒ Error ? (* Already in final state *)
     | cons f fs' ⇒
-        ! locals ← match dst with [ None ⇒ OK ? (locals f)
-                                  | Some d ⇒ reg_store d v (locals f) ];
+        ! locals ← match dst with
+                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
+                                         | _ ⇒ Error ? ]
+                   | Some d ⇒ match v with [ None ⇒ Error ?
+                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
         ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
     ]
@@ -208 +213 @@
 | Callstate _ _ _ _ _ ⇒ None ?
 | Returnstate v _ fs _ ⇒
-    match fs with [ nil ⇒ match v with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | cons _ _ ⇒ None ? ]
+    match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
 ].
 

src/RTLabs/syntax.ma

@@ -54 +54 @@
 | St_cond2 : binary_operation → register → register → label → label → statement
 | St_jumptable : register → list label → statement
-| St_return : register → statement
+| St_return : statement
 .
 

src/RTLabs/test/search.ma

@@ -132 +132 @@
     (pair ?? search10 (make_St_cond2 (Ocmp Clt) 12 13 search9 search5));
     (pair ?? search1 (make_St_op1 Onegint 8 9 search0));
-    (pair ?? search0 (make_St_return 8))
+    (pair ?? search0 (make_St_return))
 ]
 
@@ -233 +233 @@
     (pair ?? main10 (make_St_const 11 (Ointconst (repr 1)) main9));
     (pair ?? main1 (make_St_op1 Ocast8unsigned 2 1 main0));
-    (pair ?? main0 (make_St_return 2))
+    (pair ?? main0 make_St_return)
 ]