Changeset 11 for C-semantics

Timestamp:

Jul 7, 2010, 12:55:01 PM (10 years ago)

Author:

campbell

Message:

Fill in some axioms to aid executablity.
Implement global variable lookups and funtion returns.
Update compcert patch to use binary representation.

Location:

C-semantics

Files:

• Cexec.ma (modified) (5 diffs)
• Maps.ma (modified) (1 diff)
• compcert-1.7.1-matita.patch (modified) (11 diffs)
• extralib.ma (modified) (1 diff)

C-semantics/Cexec.ma

@@ -322 +322 @@
 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:block × int. eval_lvalue ge en m (Expr e' ty) (\fst r) (\snd r)) ≝
   match e' with
-  [ Evar id ⇒ Some ? (
-      l ← opt_to_res ? (get ? PTree ? id en);:
-      OK ? 〈l, zero〉)
+  [ Evar id ⇒ 
+      match (get ? PTree ? id en) with
+      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol Genv ? ge id);: OK ? 〈l,zero〉) (* global *)
+      | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
+      ]
   | Ederef a ⇒ Some ? (
       v ← exec_expr ge en m a;:
@@ -336 +338 @@
 match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
 nwhd; //;
-##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
+##[ napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
     napply opt_OK;  #v ev; /2/;
-##| napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
+##| napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
     napply opt_OK;  #v ev; /2/;
 ##| napply sig_bind2_OK; #loc ofs H;
@@ -355 +357 @@
     ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
     ##]
-##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
+##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
+##| napply eval_Evar_local; /2/
 ##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
     napply eval_Ederef; //
@@ -555 +558 @@
   | _ ⇒ Some ? (Error ?)
   ]
-| _ ⇒ Some ? (Error ?)
+| Returnstate res k m ⇒
+  match k with
+  [ Kcall r f e k' ⇒
+    match r with
+    [ None ⇒
+      match res with
+      [ Vundef ⇒ Some ? (OK ? 〈E0, (State f Sskip k' e m)〉)
+      | _ ⇒ Some ? (Error ?)
+      ]
+    | Some r' ⇒
+      match r' with [ mk_pair locofs ty ⇒
+        match locofs with [ mk_pair loc ofs ⇒ Some ? (
+          m' ← opt_to_res ? (store_value_of_type ty m loc ofs res);:
+          OK ? 〈E0, (State f Sskip k' e m')〉)
+        ]
+      ]
+    ]
+  | _ ⇒ Some ? (Error ?)
+  ]
 ]. nwhd; //;
 ##[ nrewrite > c7; napply step_skip_call; //; napply c8;
@@ -580 +601 @@
     napply sig_bind_OK; #m2 em1 Hbind;
     nwhd; napply (step_internal_function … Halloc Hbind);
+##| napply opt_bind_OK; #m' em'; napply step_returnstate_1; //;
 ##]
 nqed.

C-semantics/Maps.ma

@@ -185 +185 @@
 naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A).
 naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B).
-naxiom assoc_elements: ∀A: Type. list (ident × A) → list (ident × A).
+ndefinition assoc_elements: ∀A: Type. list (ident × A) → list (ident × A) ≝ λA,x.x.
 naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B.
 

C-semantics/compcert-1.7.1-matita.patch

@@ -1 @@
-diff -N --exclude=Configuration.ml --exclude=test --exclude=runtime --exclude='*~' --exclude=extraction --exclude=Makefile.config --exclude=ccomp --exclude=_build --exclude='*.vo' --exclude='*.glob' -ur compcert-1.7.1/cfrontend/PrintMatitaSyntax.ml compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml
+diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/cfrontend/PrintMatitaSyntax.ml compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml
 --- compcert-1.7.1/cfrontend/PrintMatitaSyntax.ml       1970-01-01 01:00:00.000000000 +0100
-+++ compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml     2010-06-15 10:36:33.000000000 +0100
++++ compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml     2010-07-07 09:51:45.000000000 +0100
 @@ -0,0 +1,471 @@
 +(* *********************************************************************)
@@ -144 +144 @@
 +  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
 +  | Tstruct(name, fld) ->
-+      fieldlist "(Tstruct " name fld
++      fieldlist "(Tstruct (succ_pos_of_nat " name fld
 +  | Tunion(name, fld) ->
-+      fieldlist "(Tunion " name fld
++      fieldlist "(Tunion (succ_pos_of_nat " name fld
 +  | Tcomp_ptr name ->
-+      "(Tcomp_ptr " ^ Int32.to_string (camlint_of_positive name) ^ ")"
++      "(Tcomp_ptr (succ_pos_of_nat " ^ Int32.to_string (camlint_of_positive name) ^ "))"
 + and typelist l =
 +    let b = Buffer.create 20 in
@@ -165 +165 @@
 +      Buffer.add_string b s;
 +      Buffer.add_string b (Int32.to_string (camlint_of_positive name));
-+      Buffer.add_char b ' ';
++      Buffer.add_string b ") ";
 +      let rec add_fields = function
 +        | Fnil -> Buffer.add_string b "Fnil"
 +        | Fcons(id, ty, tl) ->
-+            Buffer.add_string b "(Fcons ";
++            Buffer.add_string b "(Fcons (succ_pos_of_nat ";
 +            Buffer.add_string b (Int32.to_string (camlint_of_positive id));
-+            Buffer.add_char b ' ';
++            Buffer.add_string b ") ";
 +            Buffer.add_string b (stype ty);
 +            Buffer.add_char b ' ';
@@ -193 +193 @@
 +      fprintf p "(Econst_float %F)" f
 +  | Evar id ->
-+      fprintf p "(Evar %ld)" (camlint_of_positive id)
++      fprintf p "(Evar (succ_pos_of_nat %ld))" (camlint_of_positive id)
 +  | Eunop(op, e1) ->
 +      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
@@ -225 +225 @@
 +      fprintf p "(Esizeof %s)" (stype ty)
 +  | Efield(e1, id) ->
-+      fprintf p "(Efield %a %li)" print_expr e1 (camlint_of_positive id)
++      fprintf p "(Efield %a (succ_pos_of_nat %li))" print_expr e1 (camlint_of_positive id)
 +  end;
 +  fprintf p " %s)@]" (stype ty)
@@ -286 +286 @@
 +      fprintf p "(Sreturn (Some ? %a))" print_expr e
 +  | Slabel(lbl, s1) ->
-+      fprintf p "(Slabel %li@ %a)" (camlint_of_positive lbl) print_stmt s1
++      fprintf p "(Slabel (succ_pos_of_nat %li)@ %a)" (camlint_of_positive lbl) print_stmt s1
 +  | Sgoto lbl ->
-+      fprintf p "(Sgoto %li)" (camlint_of_positive lbl)
++      fprintf p "(Sgoto (succ_pos_of_nat %li))" (camlint_of_positive lbl)
 +
 +and print_cases p cases =
@@ -307 +307 @@
 +      | Coq_pair(id, ty) :: rem ->
 +          if not first then Buffer.add_string b "; ";
-+          Buffer.add_string b "mk_pair ?? ";
++          Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
 +          Buffer.add_string b (Int32.to_string (camlint_of_positive id));
-+          Buffer.add_char b ' ';
++          Buffer.add_string b ") ";
 +          Buffer.add_string b (stype ty);
 +          add_params false rem in
@@ -324 +324 @@
 +
 +let print_fundef p (Coq_pair(id, fd)) =
-+  fprintf p "@[<v 2>mk_pair ?? %li " (camlint_of_positive id);
++  fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %li) " (camlint_of_positive id);
 +  match fd with
 +  | External(id', args, res) ->
-+      fprintf p "(External %li %s %s)@]" (camlint_of_positive id) (typelist args) (stype res)
++      fprintf p "(External (succ_pos_of_nat %li) %s %s)@]" (camlint_of_positive id) (typelist args) (stype res)
 +  | Internal f ->
 +      fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
@@ -360 +360 @@
 +
 +let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
-+  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? %li@ %a)@ %s)@]"
++  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (succ_pos_of_nat %li)@ %a)@ %s)@]"
 +    (camlint_of_positive id)
 +    (print_list print_init) init
@@ -469 +469 @@
 +  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
 +  print_list print_fundef p prog.prog_funct;
-+  fprintf p "@\n%li@\n" (camlint_of_positive (Hashtbl.find atom_of_string "main"));
++  fprintf p "@\n(succ_pos_of_nat %li)@\n" (camlint_of_positive (Hashtbl.find atom_of_string "main"));
 +  print_list print_globvar p prog.prog_vars;
 +  fprintf p "@;<0 -2>.@]@."
 +
 +
-diff -N --exclude=Configuration.ml --exclude=test --exclude=runtime --exclude='*~' --exclude=extraction --exclude=Makefile.config --exclude=ccomp --exclude=_build --exclude='*.vo' --exclude='*.glob' -ur compcert-1.7.1/driver/Clflags.ml compcert-1.7.1-matitaout/driver/Clflags.ml
+diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/driver/Clflags.ml compcert-1.7.1-matitaout/driver/Clflags.ml
 --- compcert-1.7.1/driver/Clflags.ml    2010-03-03 13:22:44.000000000 +0000
 +++ compcert-1.7.1-matitaout/driver/Clflags.ml  2010-06-14 15:50:27.000000000 +0100
@@ -485 +485 @@
  let option_E = ref false
  let option_S = ref false
-diff -N --exclude=Configuration.ml --exclude=test --exclude=runtime --exclude='*~' --exclude=extraction --exclude=Makefile.config --exclude=ccomp --exclude=_build --exclude='*.vo' --exclude='*.glob' -ur compcert-1.7.1/driver/Driver.ml compcert-1.7.1-matitaout/driver/Driver.ml
+diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/driver/Driver.ml compcert-1.7.1-matitaout/driver/Driver.ml
 --- compcert-1.7.1/driver/Driver.ml     2010-03-30 13:19:52.000000000 +0100
 +++ compcert-1.7.1-matitaout/driver/Driver.ml   2010-06-14 15:51:34.000000000 +0100

C-semantics/extralib.ma

@@ -267 +267 @@
 ##] nqed.
 
-naxiom Z_times : Z → Z → Z.
+ndefinition Z_times : Z → Z → Z ≝
+λx,y. match x with
+[ OZ ⇒ OZ
+| pos n ⇒
+  match y with
+  [ OZ ⇒ OZ
+  | pos m ⇒ pos (n*m)
+  | neg m ⇒ neg (n*m)
+  ]
+| neg n ⇒
+  match y with
+  [ OZ ⇒ OZ
+  | pos m ⇒ neg (n*m)
+  | neg m ⇒ pos (n*m)
+  ]
+].
 interpretation "integer multiplication" 'times x y = (Z_times x y).