Merge IL changes from upstream (WIP)

.github/workflows/ci-spectec.yml

@@ -6,7 +6,6 @@ on:
     paths: [ spectec/**, document/** ]
 
   pull_request:
-    branches: [ main ]
     paths: [ spectec/**, document/** ]
 
   # Allows you to run this workflow manually from the Actions tab
@@ -21,7 +20,11 @@ jobs:
       - name: Setup OCaml
         uses: ocaml/setup-ocaml@v3
         with:
+<<<<<<< HEAD
+          ocaml-compiler: 5.3.x
+=======
           ocaml-compiler: 5.04.x
+>>>>>>> upstream/main
       - name: Setup Dune
         run: opam install --yes dune menhir mdx zarith
       - name: Setup Latex

specification/wasm-1.0/8-reduction.spectec

@@ -8,12 +8,12 @@ relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
 relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:
-  z; instr*  ~>  z; instr'*
-  -- Step_pure: instr* ~> instr'*
+  z; admininstr*  ~>  z; admininstr'*
+  -- Step_pure: admininstr* ~> admininstr'*
 
 rule Step/read:
-  z; instr*  ~>  z; instr'*
-  -- Step_read: z; instr* ~> instr'*
+  z; admininstr*  ~>  z; admininstr'*
+  -- Step_read: z; admininstr* ~> admininstr'*
 
 rule Steps/refl:
   z; admininstr* ~>* z; admininstr*
@@ -155,12 +155,17 @@ rule Step_pure/trap-frame:
 ;; Context
 
 rule Step/ctxt-label:
-  z; (LABEL_ n `{instr_0*} instr*)  ~>  z'; (LABEL_ n `{instr_0*} instr'*)
-  -- Step: z; instr* ~> z'; instr'*
+  z; (LABEL_ n `{instr_0*} admininstr*)  ~>  z'; (LABEL_ n `{instr_0*} admininstr'*)
+  -- Step: z; admininstr* ~> z'; admininstr'*
 
 rule Step/ctxt-frame:
-  s; f; (FRAME_ n `{f'} instr*)  ~>  s'; f; (FRAME_ n `{f'} instr'*)
-  -- Step: s; f'; instr* ~> s'; f'; instr'*
+  s; f; (FRAME_ n `{f'} admininstr*)  ~>  s'; f; (FRAME_ n `{f''} admininstr'*)
+  -- Step: s; f'; admininstr* ~> s'; f''; admininstr'*
+
+rule Step/ctxt-instrs:
+  z; val* admininstr* admininstr_1*  ~>  z'; val* admininstr'* admininstr_1*
+  -- Step: z; admininstr* ~> z'; admininstr'*
+  -- if val* =/= eps \/ admininstr_1* =/= eps
 
 
 ;; Numeric instructions

specification/wasm-2.0/1-syntax.spectec

@@ -140,7 +140,7 @@ syntax valtype hint(desc "value type") =
 
 syntax Inn hint(show I#n) = I32 | I64
 syntax Fnn hint(show F#n) = F32 | F64
-syntax Vnn hint(show V#n) = V128
+syntax Vnn hint(show V#n) = vectype
 
 
 syntax resulttype hint(desc "result type") =
@@ -152,9 +152,9 @@ syntax resulttype hint(desc "result type") =
 syntax packtype hint(desc "packed type") = I8 | I16
 syntax lanetype hint(desc "lane type") = numtype | packtype
 
-syntax Pnn hint(show I#n) = I8 | I16
+syntax Pnn hint(show I#n) = packtype
 syntax Jnn hint(show I#n) = Inn | Pnn
-syntax Lnn hint(show I#n) = Inn | Fnn | Pnn
+syntax Lnn hint(show I#n) = lanetype
 
 
 ;; External types

specification/wasm-2.0/8-reduction.spectec

@@ -8,12 +8,12 @@ relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
 relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:
-  z; instr*  ~>  z; instr'*
-  -- Step_pure: instr* ~> instr'*
+  z; admininstr*  ~>  z; admininstr'*
+  -- Step_pure: admininstr* ~> admininstr'*
 
 rule Step/read:
-  z; instr*  ~>  z; instr'*
-  -- Step_read: z; instr* ~> instr'*
+  z; admininstr*  ~>  z; admininstr'*
+  -- Step_read: z; admininstr* ~> admininstr'*
 
 rule Steps/refl:
   z; admininstr* ~>* z; admininstr*
@@ -161,13 +161,17 @@ rule Step_pure/trap-frame:
 ;; Context
 
 rule Step/ctxt-label:
-  z; (LABEL_ n `{instr_0*} instr*)  ~>  z'; (LABEL_ n `{instr_0*} instr'*)
-  -- Step: z; instr* ~> z'; instr'*
+  z; (LABEL_ n `{instr_0*} admininstr*)  ~>  z'; (LABEL_ n `{instr_0*} admininstr'*)
+  -- Step: z; admininstr* ~> z'; admininstr'*
 
 rule Step/ctxt-frame:
-  s; f; (FRAME_ n `{f'} instr*)  ~>  s'; f; (FRAME_ n `{f'} instr'*)
-  -- Step: s; f'; instr* ~> s'; f'; instr'*
+  s; f; (FRAME_ n `{f'} admininstr*)  ~>  s'; f; (FRAME_ n `{f''} admininstr'*)
+  -- Step: s; f'; admininstr* ~> s'; f''; admininstr'*
 
+rule Step/ctxt-instrs:
+  z; val* admininstr* admininstr_1*  ~>  z'; val* admininstr'* admininstr_1*
+  -- Step: z; admininstr* ~> z'; admininstr'*
+  -- if val* =/= eps \/ admininstr_1* =/= eps
 
 ;; Numeric instructions
 

specification/wasm-3.0/1.2-syntax.types.spectec

@@ -52,9 +52,9 @@ syntax valtype/sem =
   | ... | BOT
 
 
-syntax Inn hint(show I#N) hint(macro "nt%") = I32 | I64
+syntax Inn hint(show I#N) hint(macro "nt%") = addrtype
 syntax Fnn hint(show F#N) hint(macro "nt%") = F32 | F64
-syntax Vnn hint(show V#N) hint(macro "nt%") = V128
+syntax Vnn hint(show V#N) hint(macro "nt%") = vectype
 syntax Cnn hint(show t) = Inn | Fnn | Vnn
 
 
@@ -94,7 +94,7 @@ syntax storagetype hint(desc "storage type") = valtype | packtype
 
 syntax Pnn hint(show I#N) hint(macro "nt%") = packtype
 syntax Jnn hint(show I#N) hint(macro "nt%") = Inn | Pnn
-syntax Lnn hint(show I#N) hint(macro "nt%") = Inn | Fnn | Pnn
+syntax Lnn hint(show I#N) hint(macro "nt%") = lanetype
 
 
 ;; Result types

spectec/src/backend-ast/print.ml

@@ -126,6 +126,7 @@ and exp e =
   | CatE (e1, e2) -> Node ("cat", [exp e1; exp e2])
   | CvtE (e1, nt1, nt2) -> Node ("cvt", [numtyp nt1; numtyp nt2; exp e1])
   | SubE (e1, t1, t2) -> Node ("sub", [typ t1; typ t2; exp e1])
+  | IfE (e1, e2, e3) -> Node ("if", [exp e1; exp e2; exp e3])
 
 and expfield (at, e) =
   Node ("field", [mixop (Mixop.Atom at); exp e])
@@ -165,6 +166,7 @@ and prem pr =
   | LetPr (e1, e2, _xs) -> Node ("let", [exp e1; exp e2])
   | ElsePr -> Atom "else"
   | IterPr (pr1, it) -> Node ("iter", [prem pr1] @ iterexp it)
+  | NegPr pr1 -> Node ("neg", [prem pr1])
 
 
 (* Definitions *)

spectec/src/backend-interpreter/interpreter.ml

@@ -179,7 +179,7 @@ and check_type ty v expr =
     boolV (ty = "val")
   (* numtype *)
   | CaseV (nt, []) when List.mem nt inn_types ->
-    boolV (ty = "Inn" || ty = "Jnn" || ty = "numtype" || ty = "valtype" || ty = "consttype")
+    boolV (ty = "Inn" || ty = "Jnn" || ty = "numtype" || ty = "valtype" || ty = "consttype" || ty = "addrtype")
   | CaseV (nt, []) when List.mem nt fnn_types ->
     boolV (ty = "Fnn" || ty = "numtype" || ty = "valtype" || ty = "consttype")
   | CaseV (vt, []) when List.mem vt vnn_types ->

spectec/src/exe-spectec/main.ml

@@ -19,15 +19,35 @@ type pass =
   | Totalize
   | Unthe
   | Sideconditions
+  | TypeFamilyRemoval
+  | Else
+  | Undep
+  | SubExpansion
+  | Uncaseremoval
+  | AliasDemut
+  | ImproveIds
+  | Ite
 
 (* This list declares the intended order of passes.
 
 Because passes have dependencies, and because some flags enable multiple
 passers (--all-passes, some targets), we do _not_ want to use the order of
 flags on the command line.
 *)
-let _skip_passes = [ Sub; Unthe ]  (* Not clear how to extend them to indexed types *)
-let all_passes = [ Totalize; Sideconditions ]
+let _skip_passes = [ Unthe ]  (* Not clear how to extend them to indexed types *)
+let all_passes = [
+  Ite;
+  TypeFamilyRemoval;
+  Undep;
+  Totalize;
+  Else;
+  Uncaseremoval;
+  Sideconditions;
+  SubExpansion;
+  Sub;
+  AliasDemut;
+  ImproveIds
+]
 
 type file_kind =
   | Spec
@@ -53,6 +73,7 @@ let print_el = ref false
 let print_elab_il = ref false
 let print_final_il = ref false
 let print_all_il = ref false
+let print_all_il_to = ref ""
 let print_al = ref false
 let print_al_o = ref ""
 let print_no_pos = ref false
@@ -65,6 +86,16 @@ let enable_pass pass = selected_passes := PS.add pass !selected_passes
 let print_il il =
   Printf.printf "%s\n%!" (Il.Print.string_of_script ~suppress_pos:(!print_no_pos) il)
 
+let print_il_to pass_name pass_count il =
+  let pass_name = if pass_name = "" then "elab" else pass_name in
+  let pass_name = Printf.sprintf "%02d-%s" pass_count pass_name in
+  if !print_all_il_to <> "" then
+    let filename = Str.replace_first (Str.regexp "%s") pass_name !print_all_il_to in
+    Out_channel.with_open_text filename (fun oc ->
+      Out_channel.output_string oc (Il.Print.string_of_script ~suppress_pos:(!print_no_pos) il);
+      Out_channel.output_string oc "\n"
+    )
+
 
 (* Il pass metadata *)
 
@@ -73,18 +104,43 @@ let pass_flag = function
   | Totalize -> "totalize"
   | Unthe -> "the-elimination"
   | Sideconditions -> "sideconditions"
+  | TypeFamilyRemoval -> "typefamily-removal"
+  | AliasDemut -> "alias-demut"
+  | Else -> "else"
+  | Undep -> "remove-indexed-types"
+  | SubExpansion -> "sub-expansion"
+  | Uncaseremoval -> "uncase-removal"
+  | ImproveIds -> "improve-ids"
+  | Ite -> "ite"
 
 let pass_desc = function
   | Sub -> "Synthesize explicit subtype coercions"
   | Totalize -> "Run function totalization"
   | Unthe -> "Eliminate the ! operator in relations"
   | Sideconditions -> "Infer side conditions"
+  | TypeFamilyRemoval -> "Transform Type families into sum types"
+  | Else -> "Eliminate the otherwise premise in relations"
+  | Undep -> "Transform indexed types into types with well-formedness predicates"
+  | SubExpansion -> "Expands subtype matching"
+  | Uncaseremoval -> "Eliminate the uncase expression"
+  | AliasDemut -> "Lifts type aliases out of mutual groups"
+  | ImproveIds -> "Disambiguates ids used from each other"
+  | Ite -> "If-then-else introduction"
+
 
 let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
   | Sub -> Middlend.Sub.transform
   | Totalize -> Middlend.Totalize.transform
   | Unthe -> Middlend.Unthe.transform
   | Sideconditions -> Middlend.Sideconditions.transform
+  | TypeFamilyRemoval -> Middlend.Typefamilyremoval.transform
+  | Else -> Middlend.Else.transform
+  | Undep -> Middlend.Undep.transform
+  | SubExpansion -> Middlend.Subexpansion.transform
+  | Uncaseremoval -> Middlend.Uncaseremoval.transform
+  | AliasDemut -> Middlend.AliasDemut.transform
+  | ImproveIds -> Middlend.Improveids.transform
+  | Ite -> Middlend.Ite.transform
 
 
 (* Argument parsing *)
@@ -150,6 +206,7 @@ let argspec = Arg.align (
   "--print-il", Arg.Set print_elab_il, " Print IL (after elaboration)";
   "--print-final-il", Arg.Set print_final_il, " Print final IL";
   "--print-all-il", Arg.Set print_all_il, " Print IL after each step";
+  "--print-all-il-to", Arg.Set_string print_all_il_to, " Print IL after each step to file (with %s replaced by pass numer and name)";
   "--print-al", Arg.Set print_al, " Print al";
   "--print-al-o", Arg.Set_string print_al_o, " Print al with given name";
   "--print-il-notes", Arg.Set Il.Print.print_notes, " Print IL with type annotations";
@@ -171,6 +228,7 @@ let log s = if !logging then Printf.printf "== %s\n%!" s
 let () =
   Printexc.record_backtrace true;
   let last_pass = ref "" in
+  let pass_count = ref 0 in
   try
     Arg.parse argspec add_arg usage;
     log "Parsing...";
@@ -180,6 +238,7 @@ let () =
     log "Elaboration...";
     let il, elab_env = Frontend.Elab.elab el in
     if !print_elab_il || !print_all_il then print_il il;
+    print_il_to !last_pass !pass_count il;
     log "IL Validation...";
     Il.Valid.valid il;
 
@@ -196,9 +255,11 @@ let () =
         if not (PS.mem pass !selected_passes) then il else
         (
           last_pass := pass_flag pass;
+          pass_count := !pass_count + 1;
           log ("Running pass " ^ pass_flag pass ^ "...");
           let il = run_pass pass il in
           if !print_all_il then print_il il;
+          print_il_to !last_pass !pass_count il;
           log ("IL Validation after pass " ^ pass_flag pass ^ "...");
           Il.Valid.valid il;
           il

spectec/src/frontend/det.ml

@@ -42,7 +42,7 @@ and det_exp e =
   ) @@ fun _ ->
   match e.it with
   | VarE x -> bound_varid x
-  | BoolE _ | NumE _ | TextE _ -> empty
+  | BoolE _ | NumE _ | TextE _ | IfE _ -> empty
   (* We consider arithmetic expressions determinate,
    * since we sometimes need to use invertible formulas. *)
   | CvtE (e1, _, _) | UnE (#Xl.Num.unop, _, e1) | TheE e1 | LiftE e1
@@ -121,7 +121,7 @@ and det_quant_exp e =
   ) @@ fun _ ->
   match e.it with
   | VarE x -> bound_varid x
-  | BoolE _ | NumE _ | TextE _ -> empty
+  | BoolE _ | NumE _ | TextE _ | IfE _ -> empty
   | UnE (_, _, e1) | ProjE (e1, _) | TheE e1 | LiftE e1 | LenE e1
   | CvtE (e1, _, _) | SubE (e1, _, _) ->
     det_quant_exp e1
@@ -189,7 +189,7 @@ and det_prem pr =
   | RulePr (_x, _as, _mixop, e) -> det_exp e
   | IfPr e -> det_cond_exp e
   | LetPr (e1, _e2, _xs) -> det_exp e1
-  | ElsePr -> empty
+  | ElsePr | NegPr _ -> empty
   | IterPr (pr1, ite) -> det_iterexp (det_prem pr1) ite
 
 

spectec/src/frontend/dim.ml

@@ -187,7 +187,8 @@ and check_exp dims ctx e =
   | CompE (e1, e2) ->
     check_exp dims ctx e1;
     check_exp dims ctx e2
-  | SliceE (e1, e2, e3) ->
+  | SliceE (e1, e2, e3)
+  | IfE (e1, e2, e3) ->
     check_exp dims ctx e1;
     check_exp dims ctx e2;
     check_exp dims ctx e3
@@ -265,6 +266,8 @@ and check_prem dims ctx prem =
     check_exp dims ctx e2
   | IterPr (prem1, ite) ->
     check_iterexp dims ctx check_prem prem1 ite
+  | NegPr prem1 ->
+    check_prem dims ctx prem1
 
 and check_arg dims ctx a =
   match a.it with
@@ -567,6 +570,11 @@ and annot_exp side dims e : exp * occur =
     | CaseE (atom, e1) ->
       let e1', occur1 = annot_exp side dims e1 in
       CaseE (atom, e1'), occur1
+    | IfE (e1, e2, e3) ->
+      let e1', occur1 = annot_exp side dims e1 in
+      let e2', occur2 = annot_exp side dims e2 in
+      let e3', occur3 = annot_exp side dims e3 in
+      IfE (e1', e2', e3'), union occur1 (union occur2 occur3)
     | CvtE (e1, nt1, nt2) ->
       let e1', occur1 = annot_exp side dims e1 in
       CvtE (e1', nt1, nt2), occur1
@@ -688,6 +696,9 @@ and annot_prem dims prem : prem * occur =
       let prem1', occur1 = annot_prem dims prem1 in
       let iter', occur' = annot_iterexp `Rhs dims occur1 iter prem.at in
       IterPr (prem1', iter'), occur'
+    | NegPr prem1 ->
+      let prem1', occur1 = annot_prem dims prem1 in
+      NegPr prem1', occur1
   in {prem with it}, occur
 
 (*

spectec/src/il/ast.ml

@@ -77,6 +77,7 @@ and exp' =
   | SliceE of exp * exp * exp               (* exp[exp : exp] *)
   | UpdE of exp * path * exp                (* exp[path = exp] *)
   | ExtE of exp * path * exp                (* exp[path =.. exp] *)
+  | IfE of exp * exp * exp                  (* `if` exp exp exp *)
   | CallE of id * arg list                  (* defid( arg* ) *)
   | IterE of exp * iterexp                  (* exp iter *)
   | CvtE of exp * numtyp * numtyp           (* exp : typ1 <:> typ2 *)
@@ -159,6 +160,7 @@ and prem' =
   | LetPr of exp * exp * string list                  (* binding *)
   | ElsePr                                            (* otherwise *)
   | IterPr of prem * iterexp                          (* iteration *)
+  | NegPr of prem                                     (* negated premise *)
 
 and hintdef = hintdef' phrase
 and hintdef' =

spectec/src/il/dune

@@ -1,5 +1,5 @@
 (library
   (name il)
   (libraries util zarith xl el)
-  (modules ast eq free fresh subst iter env eval print debug valid)
+  (modules ast eq free fresh subst iter walk env eval print debug valid)
 )