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

Commit 29d9e42d authored by Adam Nelson's avatar Adam Nelson
Browse files

Tests can now load UIR files

parent dea983cd
......@@ -9,5 +9,9 @@ sig
(* Output: ``:bundle`` (that is, ``:environment -> environment or_error``) *)
val uir_bundle : 'a frag list -> term
val uir_bundle_s : string -> term
(* Load a bundle from a file *)
val load_uir_file : string -> term
end
......@@ -200,10 +200,9 @@ struct
raise ParseError "expected toplevel declaration"
end
fun uir_bundle (quotation : 'a frag list) : term =
fun uir_bundle_s (str : string) : term =
let
val ty_bind = or_error ty_env --> ty_bundle --> or_error ty_env
val str = unquote_all quotation
val lines = map tokenize (String.tokens (fn x => x = #"\n") str)
val decl_blocks = split_by_header (fn (Decl _::_) => true | _ => false)
(filter (fn l => l <> []) lines)
......@@ -221,5 +220,19 @@ struct
mk_list(types @ globals @ functions, ty_bundle)
]))
end
fun uir_bundle (quotation : 'a frag list) : term =
uir_bundle_s (unquote_all quotation)
fun load_uir_file (filename : string) : term =
let
val stream = TextIO.openIn filename
fun read() = case TextIO.inputLine stream of
SOME s => s ^ read()
| NONE => ""
in
uir_bundle_s (read())
handle ParseError e => raise ParseError ("[" ^ filename ^ "] " ^ e)
end
end
......@@ -16,14 +16,18 @@ sig
(* Output: ``:ssavar instruction or_error`` *)
val uir_inst : env_context -> 'a frag list -> term
val uir_inst_s : env_context -> string -> term
(* Output: ``:ssavar terminst or_error`` *)
val uir_terminst : env_context -> 'a frag list -> term
val uir_terminst_s : env_context -> string -> term
(* Output: (block name, ``:ssavar bblock or_error``) *)
val uir_block : env_context -> 'a frag list -> string * term
val uir_block_s : env_context -> string -> string * term
(* Second argument is a funcsig. Output: ``:function or_error`` *)
val uir_func : env_context -> term -> 'a frag list -> term
val uir_func_s : env_context -> term -> string -> term
end
......@@ -510,22 +510,28 @@ struct
])
end
fun uir_inst_s (env : env_context) (str : string) : term =
parse_inst env (tokenize str)
fun uir_inst (env : env_context) (quotation : 'a frag list) : term =
parse_inst env (tokenize (unquote_all quotation))
uir_inst_s env (unquote_all quotation)
fun uir_terminst_s (env : env_context) (str : string) : term =
parse_terminst env (tokenize str)
fun uir_terminst (env : env_context) (quotation : 'a frag list) : term =
parse_terminst env (tokenize (unquote_all quotation))
uir_terminst_s env (unquote_all quotation)
fun uir_block_s (env : env_context) (str : string) : string * term =
parse_block env (map tokenize (String.tokens (fn x => x = #"\n") str))
fun uir_block (env : env_context) (quotation : 'a frag list) : string * term =
let
val str = unquote_all quotation
val lines = map tokenize (String.tokens (fn x => x = #"\n") str)
in parse_block env lines end
uir_block_s env (unquote_all quotation)
fun uir_func_s (env : env_context) (fsig : term) (str : string) : term =
parse_func env fsig (map tokenize (String.tokens (fn x => x = #"\n") str))
fun uir_func (env : env_context) (fsig : term) (quotation : 'a frag list) : term =
let
val str = unquote_all quotation
val lines = map tokenize (String.tokens (fn x => x = #"\n") str)
in parse_func env fsig lines end
uir_func_s env fsig (unquote_all quotation)
end
......@@ -8,53 +8,18 @@ open EvalUtils
val _ = new_theory "basicMemoryOpsTest"
val _ = add_extra_eval_thms()
(* `// .` and `// .).)` are comments used to fix Vim syntax highlighting. The
syntax file doesn't understand that the quoted UIR code is not HOL code, and
attempts to parse @ as ∀. These comments can be safely ignored.
*)
val global_cell_test = uir_bundle`
.typedef @i8 = int<8>
.global @g <@i8>
.funcsig @main_sig = (@i8) -> (@i8) // .).)
.funcdef @main VERSION %v1 <@main_sig> { // .
%entry(<@i8> %a):
%ig = GETIREF <@i8> @g // .
STORE SEQ_CST <@i8> %ig %a
%b = LOAD SEQ_CST <@i8> %ig
RET (%b)
} // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
val global_cell_test = load_uir_file "uir/global-cell-store-load.uir"
|> to_env |> start_at "main" `[IntV 8 4w]`
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_result `OK (NOR [IntV 8 4w])`
val heap_alloc_test = uir_bundle`
.typedef @i8 = int<8>
.funcsig @main_sig = (@i8) -> (@i8) // .).)
.funcdef @main VERSION %v1 <@main_sig> { // .
%entry(<@i8> %a):
%heap = NEW <@i8>
%i = GETIREF <@i8> %heap
STORE SEQ_CST <@i8> %i %a
%b = LOAD SEQ_CST <@i8> %i
RET (%b)
} // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
val heap_alloc_test = load_uir_file "uir/heap-store-load.uir"
|> to_env |> start_at "main" `[IntV 8 4w]`
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_result `OK (NOR [IntV 8 4w])`
val stack_alloc_test = uir_bundle`
.typedef @i8 = int<8>
.funcsig @main_sig = (@i8) -> (@i8) // .).)
.funcdef @main VERSION %v1 <@main_sig> { // .
%entry(<@i8> %a):
%stack = ALLOCA <@i8>
%i = GETIREF <@i8> %stack
STORE SEQ_CST <@i8> %i %a
%b = LOAD SEQ_CST <@i8> %i
RET (%b)
} // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
val stack_alloc_test = load_uir_file "uir/stack-store-load.uir"
|> to_env |> start_at "main" `[IntV 8 4w]`
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_result `OK (NOR [IntV 8 4w])`
......
......@@ -8,22 +8,7 @@ open EvalUtils
val _ = new_theory "basicOpsTest"
val _ = add_extra_eval_thms()
(* `// .` and `// .).)` are comments used to fix Vim syntax highlighting. The
syntax file doesn't understand that the quoted UIR code is not HOL code, and
attempts to parse @ as ∀. These comments can be safely ignored.
*)
val bundle1 = uir_bundle`
.typedef @i8 = int<8>
.global @foo <@i8>
.const @two <@i8> = 2
.funcsig @add_two_sig = (@i8) -> (@i8) // .).)
.funcdef @add_two VERSION %v1 <@add_two_sig> {
%entry(<@i8> %n):
%res = ADD <@i8> %n @two // .
RET (%res)
} // .
`
val bundle1 = load_uir_file "uir/add-two.uir"
val state1 = bundle1 |> to_env |> start_at "add_two" `[IntV 8 3w]`
......
......@@ -14,7 +14,7 @@ open uvmIRTheory
val _ = new_theory "codeTest"
fun assert_parse_inst(s, i) =
let val i' = uir_inst mock_context [QUOTE ("(* *)" ^ s)]
let val i' = uir_inst_s mock_context s
handle HOL_ERR e => raise ParseError(
"failed to parse inst '" ^ s ^ "': " ^ #message e)
in
......@@ -25,7 +25,7 @@ fun assert_parse_inst(s, i) =
end
fun assert_parse_terminst(s, i) =
let val i' = uir_terminst mock_context [QUOTE ("(* *)" ^ s)]
let val i' = uir_terminst_s mock_context s
handle HOL_ERR e => raise ParseError(
"failed to parse terminst '" ^ s ^ "': " ^ #message e)
in
......
......@@ -8,70 +8,27 @@ open EvalUtils
val _ = new_theory "factorialTest"
val _ = add_extra_eval_thms()
(* `// .` and `// .).)` are comments used to fix Vim syntax highlighting. The
syntax file doesn't understand that the quoted UIR code is not HOL code, and
attempts to parse @ as ∀. These comments can be safely ignored.
*)
val fact_rec = uir_bundle`
.typedef @i16 = int<16>
.const @one <@i16> = 1
.funcsig @fact_sig = (@i16) -> (@i16) // .).)
.funcdef @fact VERSION %v1 <@fact_sig> { // .
%entry(<@i16> %n):
%is1 = ULE <@i16> %n @one // .
BRANCH2 %is1 %done() %recur(%n)
%recur(<@i16> %n):
%minus1 = SUB <@i16> %n @one // .
// CALL requires an exception clause, but fact can't throw an exception
// so the (unreachable) exception clause goes to %done.
%m = CALL <@fact_sig> @fact (%minus1) EXC (%mul(%n %m) %done()) // .
%mul(<@i16> %m <@i16> %n):
%result = MUL <@i16> %m %n
RET (%result)
%done():
RET (@one) // .)
} // .
` |> to_env
val bundle = load_uir_file "uir/factorial.uir" |> to_env
val fact2_rec_test =
fact_rec |> start_at "fact" `[IntV 16 2w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR [IntV 16 2w])`
bundle |> start_at "fact_rec" `[IntV 16 2w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR [IntV 16 2w])`
val fact5_rec_test =
fact_rec |> start_at "fact" `[IntV 16 5w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR [IntV 16 120w])`
val fact_iter = uir_bundle`
.typedef @i16 = int<16>
.const @one <@i16> = 1
.funcsig @fact_sig = (@i16) -> (@i16) // .).)
.funcdef @fact VERSION %v1 <@fact_sig> { // .
%entry(<@i16> %n):
BRANCH %loop(@one %n) // .)
%loop(<@i16> %total <@i16> %n):
%is1 = ULE <@i16> %n @one // .
BRANCH2 %is1 %done(%total) %mul(%total %n)
%mul(<@i16> %total <@i16> %n):
%total2 = MUL <@i16> %total %n
%n2 = SUB <@i16> %n @one // .
BRANCH %loop(%total2 %n2)
%done(<@i16> %total):
RET (%total)
} // .
` |> to_env
bundle |> start_at "fact_rec" `[IntV 16 5w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR [IntV 16 120w])`
val fact2_iter_test =
fact_iter |> start_at "fact" `[IntV 16 2w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR [IntV 16 2w])`
bundle |> start_at "fact_iter" `[IntV 16 2w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR [IntV 16 2w])`
val fact5_iter_test =
fact_iter |> start_at "fact" `[IntV 16 5w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR [IntV 16 120w])`
bundle |> start_at "fact_iter" `[IntV 16 5w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR [IntV 16 120w])`
val _ = export_theory()
// The simplest Mu IR test case.
// Defines a constant equal to 2, then adds another integer to it.
.typedef @i8 = int<8>
.const @two <@i8> = 2
.funcsig @add_two_sig = (@i8) -> (@i8)
.funcdef @add_two VERSION %v1 <@add_two_sig> {
%entry(<@i8> %n):
%res = ADD <@i8> %n @two
RET (%res)
}
// Two implementations of factorial, to test recursion and loops.
.typedef @i16 = int<16>
.const @one <@i16> = 1
.funcsig @fact_sig = (@i16) -> (@i16)
// The factorial function, defined recursively using CALL.
.funcdef @fact_rec VERSION %rec1 <@fact_sig> {
%entry(<@i16> %n):
%is1 = ULE <@i16> %n @one
BRANCH2 %is1 %done() %recur(%n)
%recur(<@i16> %n):
%minus1 = SUB <@i16> %n @one
%m = CALL <@fact_sig> @fact_rec (%minus1) EXC (%mul(%n %m))
%mul(<@i16> %m <@i16> %n):
%result = MUL <@i16> %m %n
RET (%result)
%done():
RET (@one)
}
// The factorial function, defined iteratively using a loop.
.funcdef @fact_iter VERSION %iter1 <@fact_sig> {
%entry(<@i16> %n):
BRANCH %loop(@one %n)
%loop(<@i16> %total <@i16> %n):
%is1 = ULE <@i16> %n @one
BRANCH2 %is1 %done(%total) %mul(%total %n)
%mul(<@i16> %total <@i16> %n):
%total2 = MUL <@i16> %total %n
%n2 = SUB <@i16> %n @one
BRANCH %loop(%total2 %n2)
%done(<@i16> %total):
RET (%total)
}
// Stores a value to a global cell, then loads it.
.typedef @i8 = int<8>
.global @g <@i8>
.funcsig @main_sig = (@i8) -> (@i8)
.funcdef @main VERSION %v1 <@main_sig> {
%entry(<@i8> %a):
%ig = GETIREF <@i8> @g
STORE SEQ_CST <@i8> %ig %a
%b = LOAD SEQ_CST <@i8> %ig
RET (%b)
}
// Stores a value to a heap-allocated location, then loads it.
.typedef @i8 = int<8>
.funcsig @main_sig = (@i8) -> (@i8)
.funcdef @main VERSION %v1 <@main_sig> {
%entry(<@i8> %a):
%heap = NEW <@i8>
%i = GETIREF <@i8> %heap
STORE SEQ_CST <@i8> %i %a
%b = LOAD SEQ_CST <@i8> %i
RET (%b)
}
// Stores a value in a stack-allocated location, then loads it.
.typedef @i8 = int<8>
.funcsig @main_sig = (@i8) -> (@i8)
.funcdef @main VERSION %v1 <@main_sig> {
%entry(<@i8> %a):
%stack = ALLOCA <@i8>
%i = GETIREF <@i8> %stack
STORE SEQ_CST <@i8> %i %a
%b = LOAD SEQ_CST <@i8> %i
RET (%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