To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit ba4f1d11 authored by Adam Nelson's avatar Adam Nelson
Browse files

Add parser for NEWTHREAD

parent 4732dc3b
......@@ -36,7 +36,7 @@ struct
"INSERTELEMENT", "SHUFFLEVECTOR", "NEW", "ALLOCA", "NEWHYBRID",
"ALLOCAHYBRID", "GETIREF", "GETFIELDIREF", "GETELEMENTIREF", "SHIFTIREF",
"GETVARPARTIREF", "LOAD", "STORE", "CMPXCHG", "ATOMICRMW", "FENCE",
"NEWTHREAD", "COMMINST"
"NEWTHREAD"
]
val terminsts = [
......@@ -96,10 +96,34 @@ struct
end
fun parse_mem_order (ord : string) : term =
if exists (fn x => x = ord) mem_orders then
mk_const(ord, mk_type("memory_order", []))
else
raise ParseError (ord ^ " is not a memory order")
if exists (fn x => x = ord) mem_orders then
mk_const(ord, mk_type("memory_order", []))
else
raise ParseError (ord ^ " is not a memory order")
fun parse_new_stack_clause (env : env_context) (tokens : uir_token list)
: (term * uir_token list) =
let
val ty = mk_type("new_stack_clause", [or_const ty_ssa])
val ty_pair = mk_prod(or_const ty_ssa, ty_type)
in
case tokens of
Word "PASS_VALUES" :: Type tys :: Parens vals :: rest =>
(mk_lift(mk_const("PassValues", ty_list ty_pair --> ty),
mk_sequence(
map (fn (ty, v) =>
case v of
SSA v => list_mk_lift(
mk_const(",", or_const ty_ssa --> ty_type --> ty_pair),
[ssa_var env ty v, ty])
| _ => raise ParseError "PASS_VALUES expected SSA arguments")
(ListPair.zipEq(parse_type_list env tys, vals)),
ty_pair)), rest)
| Word "THROW_EXC" :: SSA exc :: rest =>
(mk_lift(mk_const("ThrowExc", or_const ty_ssa --> ty),
ssa_var env (mk_return ``Ref (INL Void)``) exc), rest)
| _ => raise ParseError "expected newStackClause (PASS_VALUES or THROW_EXC)"
end
(* Parses a list of tokens into a Mu IR instruction. Returns a term of type
``:ssavar instruction or_error``.
......@@ -112,6 +136,10 @@ struct
val t_ptr = mk_return(mk_const("PTR", ty_reft))
val t_na = mk_return(mk_const("NOT_ATOMIC", mk_type("memory_order", [])))
val t_void = mk_return(mk_const("Void", ty_type))
val t_null = mk_return(infer_comb("INR", [infer_comb("RefV", [
mk_const("Void", ty_type),
mk_const("NONE", ``:addr option``)
], ty_val)], ``:ssavar or_const``))
fun two_tys tys =
let
val (t1, rest) = take_one_type tys
......@@ -244,6 +272,15 @@ struct
lhs1 "ALLOCAHYBRID", t1, t2, ssa_var env t2 len
], ty_inst)
end
(* New Thread *)
| Word "NEWTHREAD" :: SSA stack :: rest =>
let val (nsc, nil) = parse_new_stack_clause env rest in
case nil of
[] => ir_ap("NewThread", [
lhs1 "NEWTHREAD", ssa_var env (mk_return ``StackRef``) stack, t_null, nsc
], ty_inst)
| _ => raise ParseError "invalid arguments for NEWTHREAD"
end
(* Binary operations *)
| [Word opn, Type ty, SSA l, SSA r] =>
let val ty' = parse_type env ty in mk_assign(opn,
......
......@@ -3,7 +3,7 @@ open HolKernel UIRLexer ParserHelpers
signature TypeParser =
sig
val parse_type : env_context -> uir_tokens -> term
val parse_type_list : env_context -> uir_tokens -> term
val parse_type_list : env_context -> uir_tokens -> term list
val parse_funcsig : env_context -> uir_tokens -> term
val take_one_type : uir_tokens -> uir_tokens * uir_tokens
......
......@@ -65,19 +65,17 @@ struct
| Word w::cs => ([Word w], cs)
| _ => raise ParseError "expected type, got something else"
fun parse_type_list (env : env_context) (tokens : uir_tokens) : term =
let fun recur [] accum = accum
| recur ts accum =
let val (ty, rest) = take_one_type ts
in recur rest (accum @ [parse_type env ty]) end
in mk_sequence(recur tokens [], ty_type) end
fun parse_type_list (env : env_context) [] = []
| parse_type_list (env : env_context) (tokens : uir_tokens) =
let val (ty, rest) = take_one_type tokens
in parse_type env ty :: parse_type_list env rest end
fun parse_funcsig (env : env_context) [SSA (Global, name)] =
(#get_funcsig env) name
| parse_funcsig (env : env_context) [Parens lhs, Arrow, Parens rhs] =
lift_record(ty_sig, [
("arg_types", parse_type_list env lhs),
("return_types", parse_type_list env rhs)
("arg_types", mk_sequence(parse_type_list env lhs, ty_type)),
("return_types", mk_sequence(parse_type_list env rhs, ty_type))
])
| parse_funcsig _ _ = raise ParseError "expected funcsig, got something else"
......
......@@ -50,6 +50,12 @@ val _ =
``Assign [] (CmpOp UGT (Int 8) (Var (SSA "a")) (Var (SSA "b")))``);
assert_parse_inst("TRUNC <int<8> int<16>> %a",
``Assign [] (ConvOp TRUNC (Int 8) (Int 16) (Var (SSA "a")))``);
assert_parse_inst("%th = NEWTHREAD %st THROW_EXC %ex",
``NewThread (SSA "th") (Var (SSA "st")) (Const (RefV Void NONE))
(ThrowExc (Var (SSA "ex")))``);
assert_parse_inst("%th = NEWTHREAD %st PASS_VALUES <int<8> int<16>> (%a %b)",
``NewThread (SSA "th") (Var (SSA "st")) (Const (RefV Void NONE))
(PassValues [(Var (SSA "a"), Int 8); (Var (SSA "b"), Int 16)])``);
assert_parse_terminst("RET (%foo %bar)", ``Ret [Var (SSA "foo"); Var (SSA "bar")]``);
assert_parse_terminst("THROW %foo", ``Throw (Var (SSA "foo"))``);
assert_parse_terminst("BRANCH %label(%a %b)",
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment