2025-11-20 03:56:12 +09:00
|
|
|
use serde_json::json;
|
2025-11-22 05:33:40 +09:00
|
|
|
use std::collections::BTreeMap;
|
2025-11-20 03:56:12 +09:00
|
|
|
|
|
|
|
|
fn verify_program(label: &str, program: serde_json::Value) {
|
|
|
|
|
let src = serde_json::to_string(&program).expect("serialize program");
|
|
|
|
|
let module = nyash_rust::runner::json_v0_bridge::parse_json_v0_to_module_with_imports(
|
|
|
|
|
&src,
|
2025-11-22 05:33:40 +09:00
|
|
|
BTreeMap::new(),
|
2025-11-20 03:56:12 +09:00
|
|
|
)
|
|
|
|
|
.unwrap_or_else(|e| panic!("{}: failed to parse Program(JSON): {}", label, e));
|
|
|
|
|
|
|
|
|
|
let mut verifier = nyash_rust::mir::verification::MirVerifier::new();
|
|
|
|
|
if let Err(errors) = verifier.verify_module(&module) {
|
|
|
|
|
panic!(
|
|
|
|
|
"{}: MIR verification failed with errors: {:?}",
|
|
|
|
|
label, errors
|
|
|
|
|
);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn program_simple_loop() -> serde_json::Value {
|
|
|
|
|
json!({
|
|
|
|
|
"version": 0,
|
|
|
|
|
"kind": "Program",
|
|
|
|
|
"body": [
|
|
|
|
|
{ "type": "Local", "name": "loopCount", "expr": { "type": "Int", "value": 0 } },
|
|
|
|
|
{
|
|
|
|
|
"type": "Loop",
|
|
|
|
|
"cond": { "type": "Bool", "value": true },
|
|
|
|
|
"body": [
|
|
|
|
|
{ "type": "Break" }
|
|
|
|
|
]
|
|
|
|
|
},
|
|
|
|
|
{ "type": "Return", "expr": { "type": "Var", "name": "loopCount" } }
|
|
|
|
|
]
|
|
|
|
|
})
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn program_loop_with_continue() -> serde_json::Value {
|
|
|
|
|
json!({
|
|
|
|
|
"version": 0,
|
|
|
|
|
"kind": "Program",
|
|
|
|
|
"body": [
|
|
|
|
|
{ "type": "Local", "name": "cycles", "expr": { "type": "Int", "value": 0 } },
|
|
|
|
|
{
|
|
|
|
|
"type": "Loop",
|
|
|
|
|
"cond": { "type": "Bool", "value": true },
|
|
|
|
|
"body": [
|
|
|
|
|
{ "type": "Local", "name": "loopTick", "expr": { "type": "Int", "value": 1 } },
|
|
|
|
|
{
|
|
|
|
|
"type": "If",
|
|
|
|
|
"cond": { "type": "Bool", "value": true },
|
|
|
|
|
"then": [
|
|
|
|
|
{ "type": "Continue" }
|
|
|
|
|
],
|
|
|
|
|
"else": [
|
|
|
|
|
{ "type": "Break" }
|
|
|
|
|
]
|
|
|
|
|
}
|
|
|
|
|
]
|
|
|
|
|
},
|
|
|
|
|
{ "type": "Return", "expr": { "type": "Var", "name": "cycles" } }
|
|
|
|
|
]
|
|
|
|
|
})
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn program_loop_body_local_exit() -> serde_json::Value {
|
|
|
|
|
json!({
|
|
|
|
|
"version": 0,
|
|
|
|
|
"kind": "Program",
|
|
|
|
|
"body": [
|
|
|
|
|
{
|
|
|
|
|
"type": "Loop",
|
|
|
|
|
"cond": { "type": "Bool", "value": true },
|
|
|
|
|
"body": [
|
|
|
|
|
{ "type": "Local", "name": "bodyTemp", "expr": { "type": "Int", "value": 42 } },
|
|
|
|
|
{ "type": "Break" }
|
|
|
|
|
]
|
|
|
|
|
},
|
|
|
|
|
{ "type": "Return", "expr": { "type": "Var", "name": "bodyTemp" } }
|
|
|
|
|
]
|
|
|
|
|
})
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn json_loop_simple_verifies() {
|
|
|
|
|
verify_program("json_loop_simple", program_simple_loop());
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn json_loop_with_continue_verifies() {
|
|
|
|
|
verify_program("json_loop_with_continue", program_loop_with_continue());
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn json_loop_body_local_exit_verifies() {
|
|
|
|
|
verify_program("json_loop_body_local_exit", program_loop_body_local_exit());
|
|
|
|
|
}
|