Permalink
Browse files

Merge pull request #513 from CakeML/cf-ffidiv

Support for FFI-divergence in CF
  • Loading branch information...
xrchz committed Aug 22, 2018
2 parents e12dc54 + 1bc49af commit aaf2ed85060093cef59942b039fb2a53841b0c95
@@ -132,12 +132,12 @@ val CommandLine_cloop_spec = Q.store_thm("CommandLine_cloop_spec",
\\ fs[cfHeapsBaseTheory.IOx_def,cl_ffi_part_def,COMMANDLINE_def]
\\ xsimpl
\\ qmatch_goalsub_abbrev_tac`IO s u ns`
\\ map_every qexists_tac [`emp`, `s`, `s`, `u`, `ns`]
\\ map_every qexists_tac [`emp`, `s`, `u`, `ns`]
\\ xsimpl
\\ unabbrev_all_tac \\ fs []
\\ fs[cfHeapsBaseTheory.mk_ffi_next_def,ffi_get_arg_length_def,
GSYM cfHeapsBaseTheory.encode_list_def,LENGTH_EQ_NUM_compute]
\\ fs [wfcl_def])
\\ fs [wfcl_def] \\ xsimpl)
\\ rpt (xlet_auto THEN1 xsimpl)
\\ qmatch_goalsub_abbrev_tac`W8ARRAY av1 bytes`
\\ `strlen x < 65536` by
@@ -150,12 +150,12 @@ val CommandLine_cloop_spec = Q.store_thm("CommandLine_cloop_spec",
\\ qabbrev_tac `extra = W8ARRAY av [n2w (strlen x); n2w (strlen x DIV 256)]`
\\ xsimpl
\\ qmatch_goalsub_abbrev_tac`IO s u ns`
\\ map_every qexists_tac [`extra`, `s`, `s`, `u`, `ns`]
\\ map_every qexists_tac [`extra`, `s`, `u`, `ns`]
\\ xsimpl
\\ unabbrev_all_tac \\ fs []
\\ fs[cfHeapsBaseTheory.mk_ffi_next_def,ffi_get_arg_def,
GSYM cfHeapsBaseTheory.encode_list_def,LENGTH_EQ_NUM_compute]
\\ fs [wfcl_def,SUC_SUC_LENGTH,two_byte_sum])
\\ fs [wfcl_def,SUC_SUC_LENGTH,two_byte_sum] \\ xsimpl)
\\ xlet_auto
THEN1 (xsimpl \\ fs [SUC_SUC_LENGTH,two_byte_sum,mlstringTheory.LENGTH_explode])
\\ xlet_auto THEN1 (xcon \\ xsimpl)
@@ -196,12 +196,12 @@ val CommandLine_cline_spec = Q.store_thm("CommandLine_cline_spec",
\\ fs[cfHeapsBaseTheory.IOx_def,cl_ffi_part_def]
\\ xsimpl
\\ qmatch_goalsub_abbrev_tac`IO s u ns`
\\ map_every qexists_tac [`emp`, `s`, `s`, `u`, `ns`]
\\ map_every qexists_tac [`emp`, `s`, `u`, `ns`]
\\ xsimpl
\\ unabbrev_all_tac \\ fs []
\\ fs[cfHeapsBaseTheory.mk_ffi_next_def,ffi_get_arg_count_def,
GSYM cfHeapsBaseTheory.encode_list_def]
\\ fs [wfcl_def])
\\ fs [wfcl_def] \\ xsimpl)
\\ xlet_auto >- xsimpl
\\ xlet_auto THEN1 (xcon \\ xsimpl)
\\ xapp
@@ -1,5 +1,5 @@
open preamble ml_translatorLib ml_progLib std_preludeTheory
mloptionTheory
mloptionTheory basisFunctionsLib
val _ = new_theory"RuntimeProg"
@@ -23,7 +23,21 @@ val debugMsg_def = Define `
val () = next_ml_names := ["debugMsg"];
val result = translate debugMsg_def;
val sigs = module_signatures ["fullGC", "debugMsg"];
val exit =
``[Dletrec (unknown_loc)
["exit","i",
Let (SOME "y") (App (WordFromInt W8) [Var (Short "i")])
(Let (SOME "x") (App Aw8alloc [Lit(IntLit 1);
Var (Short "y")])
(App (FFI "exit") [Lit(StrLit ""); Var (Short "x")]))]]``
val _ = append_prog exit
val abort = process_topdecs `fun abort u = exit 1`
val _ = append_prog abort
val sigs = module_signatures ["fullGC", "debugMsg","exit","abort"];
val _ = ml_prog_update (close_module (SOME sigs));
@@ -0,0 +1,77 @@
open preamble
ml_translatorTheory ml_translatorLib ml_progLib cfLib basisFunctionsLib
mlstringTheory runtimeFFITheory RuntimeProgTheory
val _ = new_theory"RuntimeProof";
val _ = translation_extends "RuntimeProg";
val _ = option_monadsyntax.temp_add_option_monadsyntax();
(* heap predicate for the (trivial) runtime state *)
val RUNTIME_def = Define `
RUNTIME =
IOx runtime_ffi_part ()`
val RUNTIME_FFI_part_hprop = Q.store_thm("RUNTIME_FFI_part_hprop",
`FFI_part_hprop RUNTIME`,
rw [RUNTIME_def,cfHeapsBaseTheory.IO_def,cfMainTheory.FFI_part_hprop_def,
cfHeapsBaseTheory.IOx_def, runtime_ffi_part_def,
set_sepTheory.SEP_CLAUSES,set_sepTheory.SEP_EXISTS_THM,
set_sepTheory.cond_STAR ]
\\ fs[set_sepTheory.one_def]);
val st = get_ml_prog_state();
val Runtime_exit_spec = Q.store_thm("Runtime_exit_spec",
`INT i iv ==>
app (p:'ffi ffi_proj) ^(fetch_v "Runtime.exit" st) [iv]
(RUNTIME)
(POSTf n. λc b. RUNTIME * &(n = "exit" /\ c = [] /\ b = [i2w i]))`,
strip_tac \\ xcf "Runtime.exit" st
\\ xlet `POSTv wv. &WORD ((i2w i):word8) wv * RUNTIME`
THEN1
(simp[cf_wordFromInt_W8_def,cfTheory.app_wordFromInt_W8_def]
\\ irule local_elim \\ reduce_tac
\\ fs[ml_translatorTheory.INT_def] \\ xsimpl)
\\ xlet `POSTv loc. RUNTIME * W8ARRAY loc [i2w i]`
THEN1
(simp[cf_aw8alloc_def]
\\ irule local_elim \\ reduce_tac
\\ fs[WORD_def] \\ simp[app_aw8alloc_def]
\\ xsimpl \\ EVAL_TAC)
\\ simp[cf_ffi_def,local_def]
\\ rw[]
\\ qexists_tac `RUNTIME * W8ARRAY loc [i2w i]`
\\ qexists_tac `emp` \\ simp[app_ffi_def]
\\ simp[GSYM PULL_EXISTS]
\\ conj_tac
>- (fs[STAR_def,emp_def,SPLIT_emp2] >> metis_tac[])
\\ qexists_tac `(POSTf n. (λc b. RUNTIME * &(n = "exit" ∧ c = [] ∧ b = [i2w i]) * SEP_EXISTS loc. W8ARRAY loc [i2w i]))`
\\ rw[]
>- (fs[RUNTIME_def,runtime_ffi_part_def,IOx_def]
\\ xsimpl
\\ qmatch_goalsub_abbrev_tac `IO s u ns`
\\ MAP_EVERY qexists_tac [`loc`,`[]`,`[i2w i]`,`emp`,`s`,`u`,`ns`]
\\ conj_tac >- EVAL_TAC
\\ conj_tac >- EVAL_TAC
\\ unabbrev_all_tac
\\ fs[mk_ffi_next_def,encode_def,decode_def,ffi_exit_def]
\\ xsimpl \\ metis_tac[SEP_IMP_def])
\\ xsimpl);
val Runtime_abort_spec = Q.store_thm("Runtime_abort_spec",
`app (p:'ffi ffi_proj) ^(fetch_v "Runtime.abort" st) [uv]
(RUNTIME)
(POSTf n. λc b. RUNTIME * &(n = "exit" /\ c = [] /\ b = [1w]))`,
xcf "Runtime.abort" st
\\ xapp
\\ xsimpl \\ EVAL_TAC);
val RUNTIME_HPROP_INJ = Q.store_thm("RUNTIME_HPROP_INJ[hprop_inj]",
`!cl1 cl2. HPROP_INJ (RUNTIME) (RUNTIME) (T)`,
rw[HPROP_INJ_def,STAR_def,EQ_IMP_THM]
THEN1 (asm_exists_tac \\ rw[] \\ rw[SPLIT_emp1,cond_def])
\\ fs[SPLIT_emp1,cond_def] \\ metis_tac[]);
val _ = export_theory();
Oops, something went wrong.

0 comments on commit aaf2ed8

Please sign in to comment.