Merge pull request #861 from mktnk3/pan-to-mc_updated

Pancake proof update for BaseAddr and some more

compiler/compilationLib.sml

@@ -211,9 +211,9 @@ fun compile_to_word_0 data_prog_def to_data_thm =
 fun compile_to_lab_new conf_tm word_0_tm lab_prog_name =
   let
     (* TODO: don't look up definition *)
-    val word_0_c_def = definition"word_0_c_def"
-    val word_0_p_def = definition"word_0_p_def"
-    val word_0_names_def = definition"word_0_names_def"
+    val word_0_c_def = definition"word_0_c_def" handle HOL_ERR _ => TRUTH
+    val word_0_p_def = definition"word_0_p_def" handle HOL_ERR _ => TRUTH
+    val word_0_names_def = definition"word_0_names_def" handle HOL_ERR _ => TRUTH
     val word_0_abbrevs = [word_0_c_def, word_0_p_def, word_0_names_def]
 
     val cs = compilation_compset()
@@ -1536,6 +1536,8 @@ val compile_x64   = compile x64_backend_config_def   cbv_to_bytes_x64
 
 (*
 
+val hello_prog_def = Define `hello_prog = []:ast$dec list`;
+
 val (backend_config_def,cbv_to_bytes,name,prog_def) =
     (x64_backend_config_def,cbv_to_bytes_x64,"hello",hello_prog_def)
 

examples/compilation/x64/helloCompileScript.sml

@@ -5,87 +5,6 @@ open preamble helloProgTheory compilationLib
 
 val _ = new_theory "helloCompile"
 
-(*
-val cs = compilation_compset()
-val conf_def = x64_backend_config_def
-val data_prog_name = "data_prog_x64"
-val prog_def = hello_prog_def
-
-time (compile_to_data cs conf_def prog_def) data_prog_name
-but n.b. these cannot be trusted because of parallelism!
-runtime: 2m35s,    gctime: 12.5s,     systime: 1.4s.
-runtime: 2m28s,    gctime: 8.4s,     systime: 1.2s.
-so, with wall clock time also:
-wall: 1m22s, runtime: 2m38s,    gctime: 12.7s,     systime: 0.96333s.
-wall: 1m23s, runtime: 2m37s,    gctime: 12.4s,     systime: 1.6s.
-wall: 1m23s, runtime: 2m38s,    gctime: 13.8s,     systime: 1.5s.
-
-time (cbv_compile_to_data cs conf_def prog_def) data_prog_name
-runtime: 1m53s,    gctime: 13.9s,     systime: 0.87667s.
-runtime: 1m49s,    gctime: 8.9s,     systime: 1.3s.
-with wall clock time also:
-wall: 1m50s, runtime: 1m50s,    gctime: 7.5s,     systime: 1.2s.
-wall: 1m53s, runtime: 1m51s,    gctime: 9.2s,     systime: 1.4s.
-wall: 1m51s, runtime: 1m50s,    gctime: 7.5s,     systime: 0.82000s.
-
-(times taken on gemma 17 May 17 i7-4790 CPU @ 3.60GHz, 32GB RAM)
-*)
-
-(*
-
-now, we use a smaller program, to get reasonable times for experimentation
-val (hello_prog_tm,hello_prog_ls) = dest_eq (concl hello_prog_def)
-val (ls,ty) = hello_prog_ls |> listSyntax.dest_list
-val hello_prog_shorter_def =
-  mk_thm([],mk_eq(hello_prog, listSyntax.mk_list(
-    List.take(ls,20),ty)))
-
-val to_data_shorter_thm =
-  compile_to_data cs conf_def hello_prog_shorter_def "data_prog_shorter_x64";
-val data_prog_shorter_x64_def = definition"data_prog_shorter_x64_def";
-
-(*
-val data_prog_x64_def = data_prog_shorter_x64_def
-val to_data_thm = to_data_shorter_thm
-*)
-
-time (compile_to_lab_x64 data_prog_shorter_x64_def) to_data_shorter_thm
-(these times are for taking the first 20 declarations - might want to try with even fewer)
-wall: 1m56s, runtime: 2m28s,    gctime: 11.0s,     systime: 0.85667s.
-wall: 1m46s, runtime: 2m13s,    gctime: 11.7s,     systime: 1.2s.
-wall: 1m45s, runtime: 2m13s,    gctime: 10.8s,     systime: 1.0s.
-wall: 1m45s, runtime: 2m13s,    gctime: 10.6s,     systime: 1.0s.
-
-time (cbv_compile_to_lab_x64 data_prog_shorter_x64_def) to_data_shorter_thm
-wall: 2m17s, runtime: 2m15s,    gctime: 9.6s,     systime: 1.1s.
-wall: 2m03s, runtime: 2m02s,    gctime: 8.6s,     systime: 0.80333s.
-wall: 2m04s, runtime: 2m03s,    gctime: 8.7s,     systime: 0.95000s.
-wall: 2m06s, runtime: 2m04s,    gctime: 8.7s,     systime: 0.91333s.
-
-(times taken on gemma 18 May 17 i7-4790 CPU @ 3.60GHz, 32GB RAM)
-*)
-
-(*
-val stack_to_lab_thm =
-  compile_to_lab_x64 data_prog_shorter_x64_def to_data_shorter_thm;
-val lab_prog_def = definition"lab_prog_def";
-val heap_mb = 500 val stack_mb = 500
-val filename = "hello";
-
-time (to_bytes_x64 stack_to_lab_thm lab_prog_def heap_mb stack_mb) filename
-(these times are for the first 20 declarations above)
-wall: 3m04s, runtime: 3m40s,    gctime: 23.5s,     systime: 2.3s. (this was cold, i.e., no encoder memoisation)
-wall: 2m09s, runtime: 2m23s,    gctime: 11.7s,     systime: 1.5s.
-wall: 2m12s, runtime: 2m26s,    gctime: 14.2s,     systime: 1.6s.
-
-time (cbv_to_bytes_x64 stack_to_lab_thm lab_prog_def heap_mb stack_mb) filename
-wall: 17s, runtime: 15.7s,    gctime: 2.9s,     systime: 0.26667s.  (hot, after the first run above)
-wall: 17s, runtime: 16.5s,    gctime: 3.6s,     systime: 0.49333s.
-wall: 16s, runtime: 15.8s,    gctime: 2.9s,     systime: 0.24333s.
-
-(times taken on gemma 18 May 17 i7-4790 CPU @ 3.60GHz, 32GB RAM)
-*)
-
 val hello_compiled = save_thm("hello_compiled",
   compile_x64 "hello" hello_prog_def);
 

pancake/README.md

@@ -44,8 +44,11 @@ Compilation from panLang to crepLang.
 [pan_to_crepScript.sml](pan_to_crepScript.sml):
 Compilation from panLang to crepLang.
 
+[pan_to_targetScript.sml](pan_to_targetScript.sml):
+Compiler from Pancake to machine code
+
 [pan_to_wordScript.sml](pan_to_wordScript.sml):
-Correctness proof for --
+Compiler from pan to word
 
 [proofs](proofs):
 Proofs files for compiling Pancake.
@@ -56,11 +59,23 @@ Semantics for Pancake and its intermediate languages.
 [taParserScript.sml](taParserScript.sml):
 Parser for compactDSL programs
 
+[ta_comp_exampleScript.sml](ta_comp_exampleScript.sml):
+This is an example compilation of a TA program
+
 [ta_progs](ta_progs):
-Same TA programs
+Some sample timed automata (TA) programs.
+
+[temp](temp):
+Temporary files
 
 [timeLangScript.sml](timeLangScript.sml):
 Abstract syntax for timeLang
 
+[time_evalScript.sml](time_evalScript.sml):
+Evaluation of compilation of a timeLang program
+
 [time_to_panScript.sml](time_to_panScript.sml):
 Compilation from timeLang to panLang
+
+[time_to_targetScript.sml](time_to_targetScript.sml):
+Compiler from timeLang to machine code

pancake/crepLangScript.sml

@@ -28,6 +28,7 @@ Datatype:
       | Op binop (exp list)
       | Cmp cmp exp exp
       | Shift shift exp num
+      | BaseAddr
 End
 
 Datatype:
@@ -119,7 +120,8 @@ Definition var_cexp_def:
   (var_cexp (LoadGlob a) = []) ∧
   (var_cexp (Op bop es) = FLAT (MAP var_cexp es)) ∧
   (var_cexp (Cmp c e1 e2) = var_cexp e1 ++ var_cexp e2) ∧
-  (var_cexp (Shift sh e num) = var_cexp e)
+  (var_cexp (Shift sh e num) = var_cexp e) ∧
+  (var_cexp BaseAddr = [])
 Termination
   wf_rel_tac `measure (\e. exp_size ARB e)` >>
   rpt strip_tac >>
@@ -167,7 +169,8 @@ Definition exps_def:
   (exps (LoadGlob a) = [LoadGlob a]) ∧
   (exps (Op bop es) = FLAT (MAP exps es)) ∧
   (exps (Cmp c e1 e2) = exps e1 ++ exps e2) ∧
-  (exps (Shift sh e num) = exps e)
+  (exps (Shift sh e num) = exps e) ∧
+  (exps BaseAddr = [BaseAddr])
 Termination
   wf_rel_tac `measure (\e. exp_size ARB e)` >>
   rpt strip_tac >>

pancake/crep_to_loopScript.sml

@@ -42,6 +42,7 @@ End
 
 
 Definition compile_exp_def:
+  (compile_exp ctxt tmp l ((BaseAddr):'a crepLang$exp) = ([], BaseAddr, tmp, l)) /\
   (compile_exp ctxt tmp l ((Const c):'a crepLang$exp) = ([], Const c, tmp, l)) /\
   (compile_exp ctxt tmp l (Var v) = ([], Var (find_var ctxt v), tmp, l)) /\
   (compile_exp ctxt tmp l (Label f) = ([LocValue tmp (find_lab ctxt f)],
@@ -201,11 +202,14 @@ Definition comp_func_def:
     compile (mk_ctxt vmap fs vmax) l body
 End
 
+Definition first_name_def:
+  first_name = 60:num
+End
 
 Definition make_funcs_def:
   make_funcs prog =
   let fnames = MAP FST prog;
-      fnums  = GENLIST I (LENGTH prog);
+      fnums  = GENLIST (λn. n + first_name) (LENGTH prog);
       lens = MAP (LENGTH o FST o SND) prog;
       fnums_lens = MAP2 (λx y. (x,y)) fnums lens;
       fs =  MAP2 (λx y. (x,y)) fnames fnums_lens in
@@ -214,7 +218,7 @@ End
 
 Definition compile_prog_def:
   compile_prog prog =
-  let fnums  = GENLIST I (LENGTH prog);
+  let fnums  = GENLIST (λn. n + first_name) (LENGTH prog);
       comp = comp_func (make_funcs prog) in
    MAP2 (λn (name, params, body).
          (n,

pancake/loopLangScript.sml

@@ -16,6 +16,7 @@ Datatype:
       | Load exp
       | Op binop (exp list)
       | Shift shift exp num
+      | BaseAddr
 End
 
 Datatype:
@@ -66,7 +67,8 @@ Definition locals_touched_def:
   (locals_touched (Lookup name) = []) /\
   (locals_touched (Load addr) = locals_touched addr) /\
   (locals_touched (Op op wexps) = FLAT (MAP locals_touched wexps)) /\
-  (locals_touched (Shift sh wexp n) = locals_touched wexp)
+  (locals_touched (Shift sh wexp n) = locals_touched wexp) ∧
+  (locals_touched BaseAddr = [])
 Termination
   wf_rel_tac `measure (\e. exp_size ARB e)` >>
   rpt strip_tac >>

pancake/loop_liveScript.sml

@@ -11,6 +11,7 @@ val _ = new_theory "loop_live";
 Definition vars_of_exp_def:
   vars_of_exp (loopLang$Var v) l = insert v () l ∧
   vars_of_exp (Const _) l = l ∧
+  vars_of_exp (BaseAddr) l = l ∧
   vars_of_exp (Lookup _) l = l ∧
   vars_of_exp (Load a) l = vars_of_exp a l ∧
   vars_of_exp (Op x vs) l = vars_of_exp_list vs l ∧

pancake/loop_to_wordScript.sml

@@ -28,6 +28,7 @@ Definition comp_exp_def :
   (comp_exp ctxt (loopLang$Const w) = wordLang$Const w) /\
   (comp_exp ctxt (Var n) = Var (find_var ctxt n)) /\
   (comp_exp ctxt (Lookup m) = Lookup (Temp m)) /\
+  (comp_exp ctxt (BaseAddr) = Lookup CurrHeap) /\
   (comp_exp ctxt (Load exp) = Load (comp_exp ctxt exp)) /\
   (comp_exp ctxt (Shift s exp n) = Shift s (comp_exp ctxt exp) n) /\
   (comp_exp ctxt (Op op wexps) =

pancake/panLangScript.sml

@@ -44,6 +44,7 @@ Datatype:
       | Op binop (exp list)
       | Cmp cmp exp exp
       | Shift shift exp num
+      | BaseAddr
 End
 
 Datatype:

pancake/pan_to_crepScript.sml

@@ -73,7 +73,8 @@ Definition compile_exp_def:
   (compile_exp ctxt (Shift sh e n) =
    case FST (compile_exp ctxt e) of
    | [] => ([Const 0w], One)
-   | e::es => ([Shift sh e n], One))
+   | e::es => ([Shift sh e n], One)) /\
+  (compile_exp ctxt BaseAddr = ([BaseAddr], One))
 Termination
   wf_rel_tac `measure (\e. panLang$exp_size ARB (SND e))` >>
   rpt strip_tac >>