(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé  Grenoble-INP, VERIMAG             *)
(*           Pierre Goutagny ENS-Lyon, VERIMAG                 *)
(*                                                             *)
(*  Copyright VERIMAG. All rights reserved.                    *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

(*

This file implements the [branch_target] oracle that identifies "nop" branches in a LTL function,
and computes their target node with the distance (ie the number of cummulated nops) toward this target.

See [LTLTunneling.v]

*)

open Coqlib
open LTL
open Maps
open Camlcoq
open Tunnelinglibs

module LANG = struct
  type code_unit = LTL.bblock
  type funct = LTL.coq_function
end

module OPT = struct
  let langname = "LTL"
  let limit_tunneling = None
  let debug_flag = ref false
  let final_dump = false
end

module Partial = Tunnelinglibs.Tunneling(LANG)(OPT)

module FUNS = struct
  let build_simplified_cfg c acc pc bb =
    match bb with
    | Lbranch s :: _ ->
       let ns = get_node c s in
       set_branch c pc ns;
       acc
    | Lcond (_, _, s1, s2, _) :: _ ->
       c.num_rems <- c.num_rems + 1;
       let ns1 = get_node c s1 in
       let ns2 = get_node c s2 in
       let npc = get_node c pc in
       npc.inst <- COND(ns1, ns2);
       npc::acc
    | _ -> acc

  let print_code_unit c println (pc, bb) =
    match bb with
    | Lbranch s::_ -> (if println then Partial.debug "\n"); Partial.debug "%d:Lbranch %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc); false
    | Lcond (_, _, s1, s2, _)::_ -> (if println then Partial.debug "\n"); Partial.debug "%d:Lcond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (string_of_labeli c.nodes pc); false
    | _ -> Partial.debug "%d " pc; true

  let fn_code f = f.fn_code
  let fn_entrypoint f = f.fn_entrypoint


  (*************************************************************)
  (* Copy-paste of the extracted code of the verifier          *)
  (* with [raise (BugOnPC (P.to_int pc))] instead of [Error.*] *)

  let check_code_unit td pc bb =
    match PTree.get pc td with
    | Some p ->
      let (tpc, dpc) = p in
      let dpc0 = dpc in
      (match bb with
       | [] ->
         raise (BugOnPC (P.to_int pc))
       | i :: _ ->
         (match i with
          | Lbranch s ->
            let (ts, ds) = get td s in
            if peq tpc ts
            then if zlt ds dpc0
                 then ()
                 else raise (BugOnPC (P.to_int pc))
            else raise (BugOnPC (P.to_int pc))
          | Lcond (_, _, s1, s2, _) ->
            let (ts1, ds1) = get td s1 in
            let (ts2, ds2) = get td s2 in
            if peq tpc ts1
            then if peq tpc ts2
                 then if zlt ds1 dpc0
                      then if zlt ds2 dpc0
                           then ()
                           else raise (BugOnPC (P.to_int pc))
                      else raise (BugOnPC (P.to_int pc))
                 else raise (BugOnPC (P.to_int pc))
            else raise (BugOnPC (P.to_int pc))
          | _ ->
            raise (BugOnPC (P.to_int pc))))
    | None -> ()
end

module T = Partial.T(FUNS)
let branch_target = T.branch_target