(**************************************************************************)
(*  This file is part of BINSEC.                                          *)
(*                                                                        *)
(*  Copyright (C) 2016-2019                                               *)
(*    CEA (Commissariat Ã  l'Ã©nergie atomique et aux Ã©nergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)


open Generic_decoder_sig;;

module Decode_Expr(I:Expr_Input) = struct

  open Dba
  open Binary_op
  open I

  let (>>=) = M.bind

  let rec expr:Dba.Expr.t -> I.binary M.m = fun e ->
    (* Logger.result "Expressions %a" Dba_printer.Ascii.pp_bl_term e; *)
    match e with
    | Expr.Cst(`Constant,bv) ->
      let size = Bitvector.size_of bv in
      I.Binary.biconst ~size (Bitvector.value_of bv)
    | Expr.Cst(_,_) -> assert false
    | Expr.Binary(bop,e1,e2) ->
      let size = Dba.Expr.size_of e1 in
      expr e1 >>= fun v1 ->
      expr e2 >>= fun v2 ->
      (match bop with
       (* Binary operations. *)
       | Plus -> I.Binary.biadd ~size v1 v2
       | Minus -> I.Binary.bisub ~size v1 v2
       | Mult -> I.Binary.bimul ~size v1 v2
       | DivU -> I.Binary.biudiv ~size v1 v2
       | DivS -> I.Binary.bisdiv ~size v1 v2
       | ModU -> I.Binary.biurem ~size v1 v2
       | ModS -> I.Binary.bisrem ~size v1 v2
       | Or -> I.Binary.bor ~size v1 v2
       | And -> I.Binary.band ~size v1 v2
       | Xor -> I.Binary.bxor ~size v1 v2
       | Concat -> I.Binary.bconcat
                     ~size1:(Dba.Expr.size_of e1) v1
                     ~size2:(Dba.Expr.size_of e2) v2
       | LShift -> I.Binary.bshl ~size v1 v2
       | RShiftU -> I.Binary.blshr ~size v1 v2
       | RShiftS -> I.Binary.bashr ~size v1 v2
       | LeftRotate -> I.Binary.bv_left_rotate ~size v1 v2
       | RightRotate -> I.Binary.bv_right_rotate ~size v1 v2

       (* Predicates. *)
       | Eq -> I.Binary.beq ~size v1 v2 >>= fun bool -> I.bin_of_bool bool
       | Diff ->
         I.Binary.beq ~size v1 v2 >>= fun bool ->
         I.Boolean.not bool >>= fun nbool ->
         I.bin_of_bool nbool
       | LeqU -> I.Binary.biule ~size v1 v2 >>= fun bool -> I.bin_of_bool bool
       | GeqU -> I.Binary.biule ~size v2 v1 >>= fun bool -> I.bin_of_bool bool
       | LeqS -> I.Binary.bisle ~size v1 v2 >>= fun bool -> I.bin_of_bool bool
       | GeqS -> I.Binary.bisle ~size v2 v1 >>= fun bool -> I.bin_of_bool bool
       | LtU -> I.Binary.biult  ~size v1 v2 >>= fun bool -> I.bin_of_bool bool
       | GtU -> I.Binary.biult  ~size v2 v1 >>= fun bool -> I.bin_of_bool bool
       | LtS -> I.Binary.bislt  ~size v1 v2 >>= fun bool -> I.bin_of_bool bool
       | GtS -> I.Binary.bislt  ~size v2 v1 >>= fun bool -> I.bin_of_bool bool)
    | Expr.Unary(op,e1) as e ->
      let size = Dba.Expr.size_of e in
      expr e1 >>= fun v1 ->
      (match op with
       | Unary_op.UMinus ->
         I.Binary.biconst ~size Bigint.zero_big_int >>= fun vz ->
         I.Binary.bisub ~size vz v1
       | Unary_op.Not ->
         I.Binary.biconst ~size Bigint.(minus_big_int unit_big_int) >>= fun ffff ->
         I.Binary.bxor ~size ffff v1
       | Unary_op.Uext n -> I.Binary.buext ~size:n ~oldsize:(Dba.Expr.size_of e1) v1
       | Unary_op.Sext n -> I.Binary.bsext ~size:n ~oldsize:(Dba.Expr.size_of e1) v1
       | Unary_op.Restrict {Interval.lo; Interval.hi;} ->
         I.Binary.bextract ~lo ~hi ~oldsize:(Dba.Expr.size_of e1) v1
      )
    | Expr.Var { name = var; size; _ } -> I.get_var ~size var
    | Expr.Load(size,endianness,e) ->
      expr e >>= fun address ->
      I.load ~size:(size * 8) endianness address
    | Expr.Ite(c,e1,e2) ->
      cond c >>= fun vc ->
      expr e1 >>= fun v1 ->
      expr e2 >>= fun v2 ->
      I.ite vc v1 v2

  and cond:Dba.Expr.t -> I.boolean M.m = fun e ->
    assert(Dba.Expr.size_of e == 1);
    let open Dba.Expr in
    match e with
    | Cst(_,x) when Bitvector.is_one x -> I.Boolean.true_
    | Cst(_,x) when Bitvector.is_zero x -> I.Boolean.false_
    | Cst(_,_) -> assert false
    | Unary(Unary_op.Not,x) -> cond x >>= fun v -> I.Boolean.not v
    | Unary(Unary_op.UMinus,x) -> cond x
    | Binary(And,a,b) ->
      cond a >>= fun va ->
      cond b >>= fun vb ->
      I.Boolean.(&&) va vb
    | Binary(Or,a,b) ->
      cond a >>= fun va ->
      cond b >>= fun vb ->
      I.Boolean.(||) va vb
    | e -> expr e >>= fun v -> I.bool_of_bin v



end

module Decode_Instr(S:Instr_Input):sig
  val instruction: S.State.t -> Dba.Instr.t -> (S.boolean,S.binary) Generic_decoder_sig.jump_kind * S.State.t
end

= struct

  module EDecode = Decode_Expr(struct
      include S
      module M = State_Monad(S.State)
    end)

  open Dba

  let write_lhs state value = function
    | LValue.Var {name; size; _} -> S.set_var ~size name value state
    | LValue.Restrict({name; size; _}, {Interval.lo; Interval.hi}) ->
      let value_size = size in
      let (old,state) = S.get_var ~size name state in
      let written_size = 1 + hi - lo in
      let (v,state) =
        if lo == 0 then (value,state)
        else let pold, state = S.Binary.bextract ~oldsize:value_size ~lo:0 ~hi:(lo-1) old state in
          S.Binary.bconcat ~size1:written_size ~size2:lo value pold state in
      let (v,state) =
        if hi == (size - 1) then (v,state)
        else let (pold,state) =
               S.Binary.bextract ~oldsize:value_size ~lo:(hi+1) ~hi:(size-1) old state in
          S.Binary.bconcat ~size1:(size -  hi) ~size2:hi pold v state in
      S.set_var ~size name v state
    | LValue.Store(size,endianness,address) ->
      let (vaddress,state) = EDecode.expr address state in
      S.store ~size:(size * 8) endianness vaddress value state



  let instruction state instr =
    let open! Generic_decoder_sig in
    let open Instr in
    (* Logger.result "Instruction %a" Dba_printer.Ascii.pp_instruction instr; *)
    match instr with
    | Assign(lhs,expr,id) ->
      let (v,state) = EDecode.expr expr state in
      let state = write_lhs state v lhs in
      (JKJump (Static (JInner id)),state)
    | SJump (target,_) ->
      (JKJump (Static target), state)
    | DJump(target,_) ->
      let (v,state) = EDecode.expr target state in
      (JKJump (Dynamic v), state)
    | If(Dba.Expr.Cst(_,bv),target,id) ->
      if Bitvector.is_one bv
      then (JKJump (Static( target))),state
      else (JKJump (Static( JInner id))), state
    | If(cond,target,id) ->
      let (v,state) = EDecode.cond cond state in
      (JKIf(v,Static target,Static (JInner id))),state
    | Stop _ -> JKStop, state
    | Assume(cond,id) | Assert(cond,id) ->
      let (v,state) = EDecode.cond cond state in
      JKAssume(v,Static (JInner id)),state
    | Nondet(lhs,_,id) ->
      let size = assert false in
      let (v,state) = S.unknown ~size state in
      let state = write_lhs state v lhs in
      (JKJump (Static (JInner id))),state
    | NondetAssume(l,cond,id) ->
      let size = assert false in
      let (acc,state) = List.fold_left (fun (acc,state) _lhs ->
          let (v,state) = S.unknown ~size state in
          v::acc,state) ([],state) l in
      let values = List.rev acc in
      let state = List.fold_left2 write_lhs state values l in
      let (cond,state) = EDecode.cond cond state in
      JKAssume (cond, Static (JInner id)),state
    | Undef(lhs,id) ->
      let size = Dba_types.LValue.unsafe_bitsize lhs in
      let (v,state) = S.undef ~size state in
      let state = write_lhs state v lhs in
      (JKJump (Static (JInner id)),state)
    | Serialize _ -> assert false
    | Malloc _ -> assert false
    | Free _ -> assert false
    | Print _ -> assert false

end
