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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.