classify invalid target IR before relation comparison

src/audit.ml

@@ -44,8 +44,8 @@ let obligation_status_to_string = function
 let has_obligation kind obligations =
   List.exists (fun (o : Pipeline.obligation) -> o.Pipeline.kind = kind) obligations
 
-let classify typecheck compiled comparison =
+let classify validation compiled comparison =
-  match typecheck with
+  match validation with
   | Error msg -> Type_error msg
   | Ok () ->
       begin match comparison.Relation.verdict with
@@ -70,7 +70,7 @@ let status_for_obligation failure_mode (obligation : Pipeline.obligation) =
   | Strictness_shift, Pipeline.Strictness_risk ->
       { obligation; status = Refuted; note = "counterexample changes termination by forcing a recursive payload" }
   | Type_error msg, _ ->
-      { obligation; status = Refuted; note = "source program failed typechecking: " ^ msg }
+      { obligation; status = Refuted; note = "program failed validation: " ^ msg }
   | Other_failure msg, _ ->
       { obligation; status = Assumed; note = "unclassified failure: " ^ msg }
   | _, Pipeline.Preserve_relation ->
@@ -84,15 +84,37 @@ let status_for_obligation failure_mode (obligation : Pipeline.obligation) =
 
 let audit_case (case : Corpus.case) =
   let compiled = Pipeline.compile case.Corpus.flags case.Corpus.ty case.Corpus.source in
-  let comparison =
-    Relation.compare_programs case.Corpus.relation case.Corpus.ty case.Corpus.source compiled.Pipeline.target_program
-  in
   let source_trace = Source.evaluate case.Corpus.source in
   let specialised_trace = Source.evaluate compiled.Pipeline.specialised in
   let inlined_trace = Source.evaluate compiled.Pipeline.inlined in
-  let target_trace = Target.evaluate compiled.Pipeline.target_program in
+  let comparison =
+    match Target.validate compiled.Pipeline.target_program with
+    | Ok () ->
+        Relation.compare_programs case.Corpus.relation case.Corpus.ty case.Corpus.source compiled.Pipeline.target_program
+    | Error errors ->
+        {
+          Relation.source_outcome = source_trace.Source.outcome;
+          target_outcome = Target.Stuck ("invalid target IR: " ^ String.concat "; " errors);
+          verdict = Relation.Unrelated "invalid target IR";
+        }
+  in
+  let target_trace =
+    match Target.validate compiled.Pipeline.target_program with
+    | Ok () -> Target.evaluate compiled.Pipeline.target_program
+    | Error errors ->
+        {
+          Target.steps = [compiled.Pipeline.target_program];
+          outcome = Target.Stuck ("invalid target IR: " ^ String.concat "; " errors);
+        }
+  in
   let typecheck = Typecheck.check case.Corpus.ty case.Corpus.source in
-  let failure_mode = classify typecheck compiled comparison in
+  let validation =
+    match typecheck, Target.validate compiled.Pipeline.target_program with
+    | Error msg, _ -> Error ("source typecheck: " ^ msg)
+    | Ok (), Error errors -> Error ("target IR: " ^ String.concat "; " errors)
+    | Ok (), Ok () -> Ok ()
+  in
+  let failure_mode = classify validation compiled comparison in
   let obligations = List.map (status_for_obligation failure_mode) compiled.Pipeline.obligations in
   { case; compiled; comparison; source_trace; specialised_trace; inlined_trace; target_trace; typecheck; failure_mode; obligations }
 
@@ -146,4 +168,3 @@ let emit_matrix audits =
        "| --- | --- | --- | --- | --- |";
      ]
      @ List.map row audits)
-