Skip to content

Commit

Permalink
Merge branch 'main' into al-valid
Browse files Browse the repository at this point in the history
  • Loading branch information
@ShinWonho
ShinWonho committed Jul 31, 2024
2 parents da87cca + 6fe39f1 commit 9cfcce3
Show file tree
Hide file tree
Showing 7 changed files with 1,513 additions and 1,636 deletions.
Binary file added spectec/a.out
View file
Binary file not shown.
12 changes: 12 additions & 0 deletions spectec/src/al/al_util.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,6 +163,18 @@ let iter_type_of_value: value -> iter = function
| OptV _ -> Opt
| v -> fail_value "iter_type_of_value" v

let rec typ_to_var_name ty =
match ty.it with
(* TODO: guess this for "var" in el? *)
| Il.Ast.VarT (id, _) -> id.it
| Il.Ast.BoolT -> "b"
| Il.Ast.NumT NatT -> "n"
| Il.Ast.NumT IntT -> "i"
| Il.Ast.NumT RatT -> "q"
| Il.Ast.NumT RealT -> "r"
| Il.Ast.TextT -> "s"
| Il.Ast.TupT tys -> List.map typ_to_var_name (List.map snd tys) |> String.concat "_"
| Il.Ast.IterT (t, _) -> typ_to_var_name t

(* Destruct *)

Expand Down
17 changes: 3 additions & 14 deletions spectec/src/il2al/il2il.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,13 @@ open Util.Source
type rgroup = (exp * exp * (prem list)) phrase list

(* Helpers *)

(*
let take_prefix n str =
if String.length str < n then
str
else
String.sub str 0 n

*)

(* Walker-based transformer *)

Expand Down Expand Up @@ -94,23 +94,12 @@ let to_right_assoc_cat =
(* Unifying lhs *)

(* Estimate appropriate id name for a given type *)
let rec type_to_id ty = match ty.it with
(* TODO: guess this for "var" in el? *)
| VarT (id, _) -> take_prefix 5 id.it
| BoolT -> "b"
| NumT NatT -> "n"
| NumT IntT -> "i"
| NumT RatT -> "q"
| NumT RealT -> "r"
| TextT -> "s"
| TupT tys -> List.map type_to_id (List.map snd tys) |> String.concat "_"
| IterT (t, _) -> type_to_id t

let unified_prefix = "u"
let _unified_idx = ref 0
let init_unified_idx () = _unified_idx := 0
let get_unified_idx () = let i = !_unified_idx in _unified_idx := (i+1); i
let gen_new_unified ty = (type_to_id ty) ^ "_" ^ unified_prefix ^ (string_of_int (get_unified_idx())) $ no_region
let gen_new_unified ty = (Al.Al_util.typ_to_var_name ty) ^ "_" ^ unified_prefix ^ (string_of_int (get_unified_idx())) $ no_region
let is_unified_id id = String.split_on_char '_' id |> Util.Lib.List.last |> String.starts_with ~prefix:unified_prefix

let rec overlap e1 e2 = if eq_exp e1 e2 then e1 else
Expand Down
102 changes: 1 addition & 101 deletions spectec/src/il2al/manual.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,107 +25,7 @@ let eval_expr =
]
) $ no_region

(* Helper for the manual array_new.data algorithm *)

let group_bytes_by =
let n = varE "n" in
let n' = varE "n'" in

let bytes_ = iterE (varE "byte", ["byte"], List) in
let bytes_left = listE [accE (bytes_, sliceP (numE Z.zero, n))] in
let bytes_right = callE
(
"group_bytes_by",
[ n; accE (bytes_, sliceP (n, binE (SubOp, n', n))) ]
)
in

FuncA (
"group_bytes_by",
[n; bytes_],
[
letI (n', lenE bytes_);
ifI (
binE (GeOp, n', n),
[ returnI (Some (catE (bytes_left, bytes_right))) ],
[]
);
returnI (Some (listE []));
]
) $ no_region

let array_new_data =
let i32 = caseE (atom_of_name "I32" "numtype", []) in

let x = varE "x" in
let y = varE "y" in
let z = varE "z" in

let n = varE "n" in
let i = varE "i" in

let y_0 = varE "y_0" in
let mut = varE "mut" in
let zt = varE "zt" in

let cnn = varE "cnn" in

let c = varE "c" in

let bstar = iterE (varE "b", ["b"], List) in
let gb = varE "gb" in
let gbstar = iterE (gb, ["gb"], List) in
let cn = iterE (c, ["c"], ListN (n, None)) in

let expanddt_with_type = callE ("expanddt", [callE ("type", [z; x])]) in
let zsize = callE ("zsize", [zt]) in
let cunpack = callE ("cunpack", [zt]) in
let data = callE ("data", [z; y]) in
let group_bytes_by = callE ("group_bytes_by", [binE (DivOp, zsize, numE (Z.of_int 8)); bstar]) in
let inverse_of_bytes_ = iterE (callE ("inverse_of_ibytes", [zsize; gb]), ["gb"], List) in

RuleA (
atom_of_name "ARRAY.NEW_DATA" "admininstr",
"Step_read/array.new_data",
[x; y],
[
assertI (topValueE (Some i32));
popI (caseE (atom_of_name "CONST" "admininstr", [i32; n]));
assertI (topValueE (Some i32));
popI (caseE (atom_of_name "CONST" "admininstr", [i32; i]));
ifI (
isCaseOfE (expanddt_with_type, atom_of_name "ARRAY" "comptype"),
[
letI (caseE (atom_of_name "ARRAY" "comptype", [y_0]), expanddt_with_type);
letI (tupE [ mut; zt ], y_0);
ifI (
binE (
GtOp,
binE (AddOp, i, binE (DivOp, binE (MulOp, n, zsize), numE (Z.of_int 8))),
lenE (accE (callE ("data", [z; y]), dotP (atom_of_name "BYTES" "datainst")))
),
[ trapI () ],
[]
);
letI (cnn, cunpack);
letI (
bstar,
accE (
accE (data, dotP (atom_of_name "BYTES" "datainst")),
sliceP (i, binE (DivOp, binE (MulOp, n, zsize), numE (Z.of_int 8)))
)
);
letI (gbstar, group_bytes_by);
letI (cn, inverse_of_bytes_);
pushI (iterE (caseE (atom_of_name "CONST" "admininstr", [cnn; c]), ["c"], ListN (n, None)));
executeI (caseE (atom_of_name "ARRAY.NEW_FIXED" "admininstr", [x; n]));
],
[]
);
]
) $ no_region

let manual_algos = [eval_expr; group_bytes_by;]
let manual_algos = [eval_expr]

let return_instrs_of_instantiate config =
let store, frame, rhs = config in
Expand Down
13 changes: 4 additions & 9 deletions spectec/src/il2al/translate.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -513,15 +513,10 @@ let lhs_id_ref = ref 0
(* let lhs_prefix = "y_" *)
let init_lhs_id () = lhs_id_ref := 0
let get_lhs_name e =
let rec variable_name_of_typ typ =
match typ.it with
| Il.Ast.VarT (id, _) -> id.it
| Il.Ast.IterT (typ', _) -> variable_name_of_typ typ'
| _ -> Il.Print.string_of_typ typ
in
let lhs_id = !lhs_id_ref in
lhs_id_ref := lhs_id + 1;
varE (variable_name_of_typ e.note ^ "_" ^ string_of_int lhs_id) ~note:e.note
lhs_id_ref := (lhs_id + 1);
varE (typ_to_var_name e.note ^ "_" ^ string_of_int lhs_id) ~note:e.note


(* Helper functions *)
let rec contains_name e = match e.it with
Expand Down Expand Up @@ -671,7 +666,7 @@ and handle_call_lhs lhs rhs free_ids =

let base_typ, map_iters = get_base_typ_and_iters lhs.note rhs.note in
(* TODO: Better name using type *)
let var_name = "tmp" in
let var_name = typ_to_var_name base_typ in
let var_expr = VarE var_name $$ no_region % base_typ in
let to_iter_expr =
List.fold_right
Expand Down
Loading

0 comments on commit 9cfcce3

Please sign in to comment.