diff options
| author | Brian Campbell | 2020-11-20 16:42:53 +0000 |
|---|---|---|
| committer | Brian Campbell | 2020-11-20 18:14:10 +0000 |
| commit | c5d27227d8d5832dcd2011d2826359df4bc47e0e (patch) | |
| tree | 2beff6d815d3cfcdf48b5b269cd6aac7d259ed72 | |
| parent | 75c6d051de21b72089e4a10477d35b4c8a886266 (diff) | |
Add coverage output to short-circuiting operators
| -rw-r--r-- | src/jib/jib_compile.ml | 10 |
1 files 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))), |