Fixes for ffiname

CakeML · Dec 31, 2023 · 649fb21 · 649fb21
1 parent a4d55a8
commit 649fb21
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 17 deletions.
diff --git a/compiler/compilationLib.sml b/compiler/compilationLib.sml
@@ -1476,6 +1476,8 @@ fun eval_export word_directive target_export_defs code_def data_def syms_tm ffi_
       computeLib.Defs export_defs,
       computeLib.Defs target_export_defs ] cs;
     val exporter_tm = target_export_defs |> hd |> SPEC_ALL |> concl |> lhs |> strip_comb |> #1
+    (* the following line assumes all ffi_names are ExtCall *)
+    val ffi_names_tm = listSyntax.mk_list(listSyntax.dest_list ffi_names_tm |> fst |> map rand,stringSyntax.string_ty)
     val eval_export_tm =
       list_mk_comb(exporter_tm,
         [ffi_names_tm,
@@ -1487,6 +1489,11 @@ fun eval_export word_directive target_export_defs code_def data_def syms_tm ffi_
          (term_to_app_list word_directive eval code_def data_def app_list)
     end
 
+(*
+val (word_directive,add_encode_compset,backend_config_def,names_def,target_export_defs) =
+  ("quad",x64_targetLib.add_x64_encode_compset,x64_backend_config_def,x64_names_def,x64_export_defs)
+*)
+
 fun cbv_to_bytes word_directive add_encode_compset backend_config_def names_def target_export_defs
       stack_to_lab_thm lab_prog_def
       code_name data_name config_name filename =

diff --git a/examples/divScript.sml b/examples/divScript.sml
@@ -163,16 +163,16 @@ QED
 val names_def = Define `names = ["put_char"; "get_char"]`;
 
 val put_char_event_def = Define `
-  put_char_event c = IO_event "put_char" [n2w (ORD c)] []`;
+  put_char_event c = IO_event (ExtCall "put_char") [n2w (ORD c)] []`;
 
 val put_str_event_def = Define `
-  put_str_event cs = IO_event "put_char" (MAP (n2w o ORD) cs) []`;
+  put_str_event cs = IO_event (ExtCall "put_char") (MAP (n2w o ORD) cs) []`;
 
 val get_char_event_def = Define `
-  get_char_event c = IO_event "get_char" [] [0w, 1w; 0w, n2w (ORD c)]`;
+  get_char_event c = IO_event (ExtCall "get_char") [] [0w, 1w; 0w, n2w (ORD c)]`;
 
 val get_char_eof_event_def = Define `
-  get_char_eof_event = IO_event "get_char" [] [0w, 0w; 0w, 0w]`;
+  get_char_eof_event = IO_event (ExtCall "get_char") [] [0w, 0w; 0w, 0w]`;
 
 val update_def = PmatchHeuristics.with_classic_heuristic Define `
   (update "put_char" cs [] s = SOME (FFIreturn [] s)) /\

diff --git a/examples/filterProgScript.sml b/examples/filterProgScript.sml
@@ -509,13 +509,13 @@ val filter_ffi = Datatype `
 
 val filter_oracle = Define `
   (filter_oracle:filter_ffi oracle) port st conf bytes =
-  if port = "accept_call" then
+  if port = ExtCall "accept_call" then
     (if st.input = LNIL then Oracle_final FFI_diverged
      else if LENGTH bytes = 256 then
         Oracle_return (st with input := THE(LTL(st.input)))
                         (TAKE 256 (THE(LHD st.input)) ++ DROP (LENGTH(THE(LHD st.input))) bytes)
      else Oracle_final FFI_failed)
-  else if port = "emit_string" then
+  else if port = ExtCall "emit_string" then
     Oracle_return st bytes
   else Oracle_final FFI_failed
 `
@@ -544,7 +544,7 @@ val decode_oracle_state_def = Define `
 
 val filter_cf_oracle = Define `
   filter_cf_oracle port conf bytes ffi =
-  case filter_oracle port (decode_oracle_state ffi) conf bytes of
+  case filter_oracle (ExtCall port) (decode_oracle_state ffi) conf bytes of
       Oracle_final FFI_failed => NONE
     | Oracle_final FFI_diverged => SOME FFIdiverge
     | Oracle_return st' bytes => SOME(FFIreturn bytes (encode_oracle_state st'))`
@@ -555,7 +555,7 @@ val seL4_IO_def = Define `
     FFI_part
       (encode_oracle_state (<|input:=input|>))
       filter_cf_oracle
-      ["accept_call";"emit_string"]
+      ["accept_call"; "emit_string"]
       events)`
 
 Theorem decode_encode_oracle_state_11:
@@ -592,10 +592,10 @@ val LLENGTH_NONE_LTAKE = Q.prove(
   Induct >> Cases_on `ll` >> rw[]);
 
 val is_emit_def = Define
-  `is_emit (IO_event s _ _) = (s = "emit_string")`
+  `is_emit (IO_event s _ _) = (s = ExtCall "emit_string")`
 
 val output_event_of_def = Define
-  `output_event_of s = IO_event "emit_string" s []`
+  `output_event_of s = IO_event (ExtCall "emit_string") s []`
 
 val nth_arr_def = Define `nth_arr n ll =
  FST(FUNPOW (λ(l,ll).
@@ -671,9 +671,9 @@ val next_filter_events = Define
   `next_filter_events filter_fun last_input input =
    let new_input = TAKE 256 input ++ DROP (LENGTH input) last_input
    in
-    [IO_event "accept_call" [] (ZIP (last_input,new_input))] ++
+    [IO_event (ExtCall "accept_call") [] (ZIP (last_input,new_input))] ++
     if filter_fun(cut_at_null_w input) then
-      [IO_event "emit_string" (cut_at_null_w new_input) []]
+      [IO_event (ExtCall "emit_string") (cut_at_null_w new_input) []]
     else
       []`
 
@@ -834,7 +834,7 @@ Proof
            (encode_oracle_state
               <|input := THE (LDROP (SUC i) input)|>) filter_cf_oracle
            ["accept_call"; "emit_string"]
-           [IO_event "accept_call" [] (ZIP(inputbuff,
+           [IO_event (ExtCall "accept_call") [] (ZIP(inputbuff,
                                           ((TAKE 256 (THE (LHD (THE (LDROP i input)))) ++
                               DROP (LENGTH (THE (LHD (THE (LDROP i input))))) inputbuff))))]
            ))` >-
@@ -1147,7 +1147,7 @@ Proof
   qabbrev_tac `newinit = TAKE 256 h ++ DROP (LENGTH h) init` >>
   xlet `POSTv v. &UNIT_TYPE () v *
         W8ARRAY v' newinit * W8ARRAY dummyarr_loc [] *
-        seL4_IO (fromList l) (SNOC (IO_event "accept_call" [] (ZIP(init,newinit))) events)` >-
+        seL4_IO (fromList l) (SNOC (IO_event (ExtCall "accept_call") [] (ZIP(init,newinit))) events)` >-
     (xffi >> xsimpl >>
      simp[seL4_IO_def,Abbr `newinit`] >>
      qmatch_goalsub_abbrev_tac `one(FFI_part s u ns events)` >>
@@ -1224,8 +1224,8 @@ QED
 val seL4_proj1_def = Define `
   seL4_proj1 = (λffi.
     FEMPTY |++ (mk_proj1 (encode_oracle_state,decode_oracle_state,
-                          [("accept_call", filter_oracle "accept_call");
-                           ("emit_string", filter_oracle "emit_string")]) ffi))`;
+                          [("accept_call", filter_oracle (ExtCall "accept_call"));
+                           ("emit_string", filter_oracle (ExtCall "emit_string"))]) ffi))`;
 
 val seL4_proj2 = Define `seL4_proj2 =
   [(["accept_call";"emit_string"],filter_cf_oracle)]`
@@ -1366,7 +1366,7 @@ Theorem forward_matching_lines_ffidiv_semantics:
  semantics_prog (^(get_state st) with ffi := (filter_ffi <|input:=input|>)) ^(get_env st)
   [Dlet unknown_loc (Pcon NONE [])
            (App Opapp [Var (Short "forward_matching_lines"); Con NONE []])]
-  (Terminate (FFI_outcome(Final_event "accept_call" [] bytes FFI_diverged))
+  (Terminate (FFI_outcome(Final_event (ExtCall "accept_call") [] bytes FFI_diverged))
              events) /\
  LFILTER is_emit (fromList events) = LMAP (output_event_of o cut_at_null_w) (LFILTER (language o MAP (CHR o w2n) o cut_at_null_w) input)
 Proof