Changeset 965 for src

Timestamp:

Jun 15, 2011, 4:15:56 PM (9 years ago)

Author:

campbell

Message:

Update some Clight examples.

Location:

src/Clight

Files:

• clightPrintMatita.ml (modified) (5 diffs)
• test/duff.c.ma (added)
• test/insertsort.c (modified) (1 diff)
• test/insertsort.c.ma (added)
• test/insertsort.ma (deleted)
• test/null-op.c.ma (moved) (moved from src/Clight/test/null-op.ma) (6 diffs)
• test/search.ma (deleted)
• test/sum.c.ma (moved) (moved from src/Clight/test/sum.ma) (6 diffs)

src/Clight/clightPrintMatita.ml

@@ -63 +63 @@
   | Ole  -> "Ole"
   | Oge  -> "Oge"
+
+let name_intsize = function
+  | I8  -> "I8"
+  | I16 -> "I16"
+  | I32 -> "I32"
 
 let name_inttype sz sg =
@@ -191 +196 @@
 
 let rec print_expr p (Expr (eb, ty)) =
-  fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descr eb (stype ty)
-and print_expr_descr p eb =
+  fprintf p "@[<hov 2>(Expr %a@ %s)@]" (print_expr_descr ty) eb (stype ty)
+and print_expr_descr ty p eb =
   match eb with
-  | Ecost (_, Expr (e, _)) -> print_expr_descr p e
+  | Ecost (_, Expr (e, ty)) -> print_expr_descr ty p e
   | Econst_int n ->
-      fprintf p "(Econst_int (repr %d))" n
+      fprintf p "(Econst_int %s (repr ? %d))"
+        (match ty with Tint (sz, _) -> name_intsize sz | _ -> "I32")
+        n
   | Econst_float f ->
       fprintf p "(Econst_float %F)" f
@@ -294 +301 @@
       fprintf p "@[<v 2>(LSdefault@ %a)@]" print_stmt s
   | LScase(lbl, s, rem) ->
-      fprintf p "@[<v 2>(LScase (repr %d)@ %a@ %a)@]"
+      fprintf p "@[<v 2>(LScase I32 (repr ? %d)@ %a@ %a)@]"
               lbl
               print_stmt s
@@ -348 +355 @@
 
 let print_init p = function
-  | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
-  | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
+  | Init_int8 n -> fprintf p "(Init_int8 (repr I8 %d))@ " n
+  | Init_int16 n -> fprintf p "(Init_int16 (repr I16 %d))@ " n
   (*| Init_null r -> fprintf p "(Init_null Any)@"*)
-  | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
+  | Init_int32 n -> fprintf p "(Init_int32 (repr I32 %d))@ " n
   | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
   | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
   | Init_space n -> fprintf p "(Init_space %d)@ " n
-  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof Any (ident_of_nat %i) (repr %d))" (id_i symb) ofs
+  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof Any (ident_of_nat %i) %d)" (id_i symb) ofs
 
 let re_string_literal = Str.regexp "__stringlit_[0-9]+"
@@ -466 +473 @@
   print_list print_globvar p prog.prog_vars;
   fprintf p "@;<0 -2>.@]@\n@\n";
-  fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).@\n";
+  fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).@\n";
   fprintf p "normalize  (* you can examine the result here *)@."
 

src/Clight/test/insertsort.c

@@ +1 @@
+/* Remove memory region for now. */
+#define __pdata
+
 struct list {
   unsigned char i;

src/Clight/test/null-op.c.ma

@@ -9 +9 @@
                   (Tpointer Any (Tint I8 Unsigned )))
          (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
-           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tpointer Any (Tint I8 Unsigned ))))
        (Ssequence
@@ -23 +23 @@
                         (Tpointer Any (Tint I8 Unsigned ))))
                       (Tint I32 Signed  ))
-         (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))))
+         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
+                               (Tint I32 Signed  ))))
          Sskip)
        (Ssequence
@@ -33 +34 @@
                           (Tpointer Any (Tint I8 Unsigned ))))
                         (Tint I32 Signed  ))
-                      (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+                      (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
                       (Tint I32 Signed  ))
-         (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))))
+         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
+                               (Tint I32 Signed  ))))
          Sskip)
        (Ssequence
@@ -42 +44 @@
          (Expr (Ebinop Oadd
            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
-           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tpointer Any (Tint I8 Unsigned ))))
        (Ssequence
        (Sassign (Expr (Evar (ident_of_nat 2))
                   (Tpointer Any (Tint I8 Unsigned )))
-         (Expr (Ebinop Oadd (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))
+         (Expr (Ebinop Oadd
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))))
            (Tpointer Any (Tint I8 Unsigned ))))
@@ -55 +58 @@
          (Expr (Ebinop Osub
            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
-           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tpointer Any (Tint I8 Unsigned ))))
        (Sreturn (Some expr (Expr (Ebinop Oeq
@@ -62 +65 @@
                              (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
                                (Expr (Ecast (Tpointer Any Tvoid)
-                                 (Expr (Econst_int (repr 0))
-                                   (Tint I32 Unsigned)))
+                                 (Expr (Econst_int I8 (repr ? 0))
+                                   (Tint I8 Unsigned )))
                                  (Tpointer Any Tvoid)))
                                (Tpointer Any (Tint I8 Unsigned ))))

src/Clight/test/sum.c.ma

@@ +1 @@
+include "Clight/Cexec.ma".
 include "common/Animation.ma".
-include "Clight/Cexec.ma".
 
 definition myprog := mk_program clight_fundef type
@@ -10 +10 @@
            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tint I8 Unsigned )))
-       (Ssequence
        (Ssequence
        (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
@@ -37 +36 @@
                        (Tarray Any (Tint I8 Unsigned ) 5))
                      (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
-                     (Tarray Any (Tint I8 Unsigned ) 5)))
+                     (Tpointer Any (Tint I8 Unsigned ))))
                    (Tint I8 Unsigned ))) (Tint I32 Signed  )))
                (Tint I32 Signed  ))) (Tint I8 Unsigned )))
        )
-       Sskip)
        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
                              (Expr (Evar (ident_of_nat 2))
@@ -51 +49 @@
   (ident_of_nat 0)
   [〈〈〈ident_of_nat 3 (* src *),
-     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 17)) ;
-     (Init_int8 (repr I8 8)) ; (Init_int8 (repr I8 4)) ]〉, Any〉,
+     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
+     (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
+     (Init_int8 (repr I8 4)) ]〉, Any〉,
      (Tarray Any (Tint I8 Unsigned ) 5)〉]
 .
@@ -64 +63 @@
 include "Cminor/semantics.ma".
 
-example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
+example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
 normalize
 @refl
@@ -72 +71 @@
 include "RTLabs/semantics.ma".
 
-example e2: finishes_with (repr 74) ? (
+example e2: finishes_with (repr I32 74) ? (
 do p1 ← clight_to_cminor myprog;
 do p2 ← cminor_to_rtlabs p1;