Changeset 11


Ignore:
Timestamp:
Jul 7, 2010, 12:55:01 PM (9 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:
4 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r10 r11  
    322322and 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)) ≝
    323323  match e' with
    324   [ Evar id ⇒ Some ? (
    325       l ← opt_to_res ? (get ? PTree ? id en);:
    326       OK ? 〈l, zero〉)
     324  [ Evar id ⇒
     325      match (get ? PTree ? id en) with
     326      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol Genv ? ge id);: OK ? 〈l,zero〉) (* global *)
     327      | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
     328      ]
    327329  | Ederef a ⇒ Some ? (
    328330      v ← exec_expr ge en m a;:
     
    336338match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    337339nwhd; //;
    338 ##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
     340##[ napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
    339341    napply opt_OK;  #v ev; /2/;
    340 ##| napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
     342##| napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
    341343    napply opt_OK;  #v ev; /2/;
    342344##| napply sig_bind2_OK; #loc ofs H;
     
    355357    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    356358    ##]
    357 ##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
     359##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
     360##| napply eval_Evar_local; /2/
    358361##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
    359362    napply eval_Ederef; //
     
    555558  | _ ⇒ Some ? (Error ?)
    556559  ]
    557 | _ ⇒ Some ? (Error ?)
     560| Returnstate res k m ⇒
     561  match k with
     562  [ Kcall r f e k' ⇒
     563    match r with
     564    [ None ⇒
     565      match res with
     566      [ Vundef ⇒ Some ? (OK ? 〈E0, (State f Sskip k' e m)〉)
     567      | _ ⇒ Some ? (Error ?)
     568      ]
     569    | Some r' ⇒
     570      match r' with [ mk_pair locofs ty ⇒
     571        match locofs with [ mk_pair loc ofs ⇒ Some ? (
     572          m' ← opt_to_res ? (store_value_of_type ty m loc ofs res);:
     573          OK ? 〈E0, (State f Sskip k' e m')〉)
     574        ]
     575      ]
     576    ]
     577  | _ ⇒ Some ? (Error ?)
     578  ]
    558579]. nwhd; //;
    559580##[ nrewrite > c7; napply step_skip_call; //; napply c8;
     
    580601    napply sig_bind_OK; #m2 em1 Hbind;
    581602    nwhd; napply (step_internal_function … Halloc Hbind);
     603##| napply opt_bind_OK; #m' em'; napply step_returnstate_1; //;
    582604##]
    583605nqed.
  • C-semantics/Maps.ma

    r10 r11  
    185185naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A).
    186186naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B).
    187 naxiom assoc_elements: ∀A: Type. list (ident × A) → list (ident × A).
     187ndefinition assoc_elements: ∀A: Type. list (ident × A) → list (ident × A) ≝ λA,x.x.
    188188naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B.
    189189
  • C-semantics/compcert-1.7.1-matita.patch

    r9 r11  
    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
     1diff -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
    22--- compcert-1.7.1/cfrontend/PrintMatitaSyntax.ml       1970-01-01 01:00:00.000000000 +0100
    3 +++ compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml     2010-06-15 10:36:33.000000000 +0100
     3+++ compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml     2010-07-07 09:51:45.000000000 +0100
    44@@ -0,0 +1,471 @@
    55+(* *********************************************************************)
     
    144144+  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
    145145+  | Tstruct(name, fld) ->
    146 +      fieldlist "(Tstruct " name fld
     146+      fieldlist "(Tstruct (succ_pos_of_nat " name fld
    147147+  | Tunion(name, fld) ->
    148 +      fieldlist "(Tunion " name fld
     148+      fieldlist "(Tunion (succ_pos_of_nat " name fld
    149149+  | Tcomp_ptr name ->
    150 +      "(Tcomp_ptr " ^ Int32.to_string (camlint_of_positive name) ^ ")"
     150+      "(Tcomp_ptr (succ_pos_of_nat " ^ Int32.to_string (camlint_of_positive name) ^ "))"
    151151+ and typelist l =
    152152+    let b = Buffer.create 20 in
     
    165165+      Buffer.add_string b s;
    166166+      Buffer.add_string b (Int32.to_string (camlint_of_positive name));
    167 +      Buffer.add_char b ' ';
     167+      Buffer.add_string b ") ";
    168168+      let rec add_fields = function
    169169+        | Fnil -> Buffer.add_string b "Fnil"
    170170+        | Fcons(id, ty, tl) ->
    171 +            Buffer.add_string b "(Fcons ";
     171+            Buffer.add_string b "(Fcons (succ_pos_of_nat ";
    172172+            Buffer.add_string b (Int32.to_string (camlint_of_positive id));
    173 +            Buffer.add_char b ' ';
     173+            Buffer.add_string b ") ";
    174174+            Buffer.add_string b (stype ty);
    175175+            Buffer.add_char b ' ';
     
    193193+      fprintf p "(Econst_float %F)" f
    194194+  | Evar id ->
    195 +      fprintf p "(Evar %ld)" (camlint_of_positive id)
     195+      fprintf p "(Evar (succ_pos_of_nat %ld))" (camlint_of_positive id)
    196196+  | Eunop(op, e1) ->
    197197+      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
     
    225225+      fprintf p "(Esizeof %s)" (stype ty)
    226226+  | Efield(e1, id) ->
    227 +      fprintf p "(Efield %a %li)" print_expr e1 (camlint_of_positive id)
     227+      fprintf p "(Efield %a (succ_pos_of_nat %li))" print_expr e1 (camlint_of_positive id)
    228228+  end;
    229229+  fprintf p " %s)@]" (stype ty)
     
    286286+      fprintf p "(Sreturn (Some ? %a))" print_expr e
    287287+  | Slabel(lbl, s1) ->
    288 +      fprintf p "(Slabel %li@ %a)" (camlint_of_positive lbl) print_stmt s1
     288+      fprintf p "(Slabel (succ_pos_of_nat %li)@ %a)" (camlint_of_positive lbl) print_stmt s1
    289289+  | Sgoto lbl ->
    290 +      fprintf p "(Sgoto %li)" (camlint_of_positive lbl)
     290+      fprintf p "(Sgoto (succ_pos_of_nat %li))" (camlint_of_positive lbl)
    291291+
    292292+and print_cases p cases =
     
    307307+      | Coq_pair(id, ty) :: rem ->
    308308+          if not first then Buffer.add_string b "; ";
    309 +          Buffer.add_string b "mk_pair ?? ";
     309+          Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
    310310+          Buffer.add_string b (Int32.to_string (camlint_of_positive id));
    311 +          Buffer.add_char b ' ';
     311+          Buffer.add_string b ") ";
    312312+          Buffer.add_string b (stype ty);
    313313+          add_params false rem in
     
    324324+
    325325+let print_fundef p (Coq_pair(id, fd)) =
    326 +  fprintf p "@[<v 2>mk_pair ?? %li " (camlint_of_positive id);
     326+  fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %li) " (camlint_of_positive id);
    327327+  match fd with
    328328+  | External(id', args, res) ->
    329 +      fprintf p "(External %li %s %s)@]" (camlint_of_positive id) (typelist args) (stype res)
     329+      fprintf p "(External (succ_pos_of_nat %li) %s %s)@]" (camlint_of_positive id) (typelist args) (stype res)
    330330+  | Internal f ->
    331331+      fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
     
    360360+
    361361+let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
    362 +  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? %li@ %a)@ %s)@]"
     362+  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (succ_pos_of_nat %li)@ %a)@ %s)@]"
    363363+    (camlint_of_positive id)
    364364+    (print_list print_init) init
     
    469469+  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
    470470+  print_list print_fundef p prog.prog_funct;
    471 +  fprintf p "@\n%li@\n" (camlint_of_positive (Hashtbl.find atom_of_string "main"));
     471+  fprintf p "@\n(succ_pos_of_nat %li)@\n" (camlint_of_positive (Hashtbl.find atom_of_string "main"));
    472472+  print_list print_globvar p prog.prog_vars;
    473473+  fprintf p "@;<0 -2>.@]@."
    474474+
    475475+
    476 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
     476diff -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
    477477--- compcert-1.7.1/driver/Clflags.ml    2010-03-03 13:22:44.000000000 +0000
    478478+++ compcert-1.7.1-matitaout/driver/Clflags.ml  2010-06-14 15:50:27.000000000 +0100
     
    485485 let option_E = ref false
    486486 let option_S = ref false
    487 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
     487diff -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
    488488--- compcert-1.7.1/driver/Driver.ml     2010-03-30 13:19:52.000000000 +0100
    489489+++ compcert-1.7.1-matitaout/driver/Driver.ml   2010-06-14 15:51:34.000000000 +0100
  • C-semantics/extralib.ma

    r10 r11  
    267267##] nqed.
    268268
    269 naxiom Z_times : Z → Z → Z.
     269ndefinition Z_times : Z → Z → Z ≝
     270λx,y. match x with
     271[ OZ ⇒ OZ
     272| pos n ⇒
     273  match y with
     274  [ OZ ⇒ OZ
     275  | pos m ⇒ pos (n*m)
     276  | neg m ⇒ neg (n*m)
     277  ]
     278| neg n ⇒
     279  match y with
     280  [ OZ ⇒ OZ
     281  | pos m ⇒ neg (n*m)
     282  | neg m ⇒ pos (n*m)
     283  ]
     284].
    270285interpretation "integer multiplication" 'times x y = (Z_times x y).
    271286
Note: See TracChangeset for help on using the changeset viewer.