From c5d27227d8d5832dcd2011d2826359df4bc47e0e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 20 Nov 2020 16:42:53 +0000
Subject: Add coverage output to short-circuiting operators

---
 src/jib/jib_compile.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index fb86333f..93071f69 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -828,27 +828,33 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      [iclear ctyp gs]
 
   | AE_short_circuit (SC_and, aval, aexp) ->
+     let branch_id, on_reached = coverage_branch_reached l in
      let left_setup, cval, left_cleanup = compile_aval l ctx aval in
      let right_setup, call, right_cleanup = compile_aexp ctx aexp in
+     let right_coverage = coverage_branch_taken branch_id aexp in
      let gs = ngensym () in
      left_setup
+     @ on_reached
      @ [ idecl CT_bool gs;
          iif l cval
-             (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
+             (right_coverage @ right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
              [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool false, CT_bool))]
              CT_bool ]
      @ left_cleanup,
      (fun clexp -> icopy l clexp (V_id (gs, CT_bool))),
      []
   | AE_short_circuit (SC_or, aval, aexp) ->
+     let branch_id, on_reached = coverage_branch_reached l in
      let left_setup, cval, left_cleanup = compile_aval l ctx aval in
      let right_setup, call, right_cleanup = compile_aexp ctx aexp in
+     let right_coverage = coverage_branch_taken branch_id aexp in
      let gs = ngensym () in
      left_setup
+     @ on_reached
      @ [ idecl CT_bool gs;
          iif l cval
              [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool true, CT_bool))]
-             (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
+             (right_coverage @ right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
              CT_bool ]
      @ left_cleanup,
      (fun clexp -> icopy l clexp (V_id (gs, CT_bool))),
-- 
cgit v1.2.3