let sum_size (n : size) (m:size)
  = match n with
    | Variable
    | WithVariableSuffix _ -> n
    | Fixed n ->
      match m with
      | Fixed m -> Fixed (n + m)
      | WithVariableSuffix m -> WithVariableSuffix (n + m)
      | Variable -> WithVariableSuffix n
let sum_size (n m: size) =
match n with
| Variable | WithVariableSuffix _ -> n
| Fixed n ->
  match m with
  | Fixed m -> Fixed (n + m)
  | WithVariableSuffix m -> WithVariableSuffix (n + m)
  | Variable -> WithVariableSuffix n
TypeSizes.fst.checked
prims.fst.checked Options.fsti.checked Hashtable.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked Binding.fsti.checked Ast.fst.checked
TypeSizes.fst
TypeSizes.size Prims.int TypeSizes.Fixed Prims.op_Addition TypeSizes.WithVariableSuffix
(*
   Copyright 2019 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain as copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module TypeSizes
open FStar.All
open Ast
open FStar.Mul
module H = Hashtable
module B = Binding

let product_size (base:size) (n:int) =
  match base with
  | Variable
  | WithVariableSuffix _ ->
    Variable
  | Fixed k ->
    Fixed (k * n)

let typename = ident'

let alignment = option (x:int{x == 1 \/ x == 2 \/ x == 4 \/ x == 8})

type size_env = H.t typename (size & alignment)

//TODO: size of pointer is platform-dependent
let pointer_alignment : alignment = Some 8

let initial_senv () =
  let i = [
       ("unit",     (Fixed 0,  None));
       ("Bool",     (Fixed 1,  Some 1));
       ("UINT8",    (Fixed 1,  Some 1));
       ("UINT16",   (Fixed 2,  Some 2));
       ("UINT32",   (Fixed 4,  Some 4));
       ("UINT64",   (Fixed 8,  Some 8));
       ("UINT8BE",   (Fixed 1,  Some 1));
       ("UINT16BE",   (Fixed 2,  Some 2));
       ("UINT32BE",   (Fixed 4,  Some 4));
       ("UINT64BE",   (Fixed 8,  Some 8));
       ("field_id", (Fixed 4,  Some 4));
       ("all_bytes", (Variable, None));
       ("all_zeros", (Variable, None));
       ("PUINT8",   (Variable, pointer_alignment))
  ]
  in
  let senv = H.create 17 in
  List.iter (fun (i, k) -> H.insert senv (to_ident' i) k) i;
  senv

let size_and_alignment_of_typename (env:env_t) (i:ident)
  : ML (size & alignment)
  = match H.try_find (snd env) i.v with
    | Some s -> s
    | None ->
      failwith (Printf.sprintf "size_of_typename: Identifier %s not found" (ident_to_string i))

let size_of_typename (env:env_t) (i:ident)
  : ML size
  = fst (size_and_alignment_of_typename env i)

let print_size =
  function
  | Fixed n -> Printf.sprintf "(Fixed %d)" n
  | WithVariableSuffix n -> Printf.sprintf "(WithVariableSuffix %d)" n
  | Variable -> "Variable"

let extend_with_size_of_ident (env:env_t) (i:ident) (n:size) (a:alignment)
  : ML unit
  = Options.debug_print_string
     (Printf.sprintf "***** Size of %s = %s\n"
                     (ident_to_string i) (print_size n));
    H.insert (snd env) i.v (n, a)

let extend_with_size_of_typedef_names (env:env_t) (names:typedef_names) (size:size) (a:alignment)
  : ML unit
  = extend_with_size_of_ident env names.typedef_name size a;
    extend_with_size_of_ident env names.typedef_abbrev size a;
    extend_with_size_of_ident env names.typedef_ptr_abbrev Variable a

let size_and_alignment_of_typ (env:env_t) (t:typ)
  : ML (size & alignment)
  = match t.v with
    | Type_app i _ _ -> size_and_alignment_of_typename env i
    | Pointer _ -> Variable, Some 8

let size_of_typ (env:env_t) (t:typ)
  : ML size
  = fst (size_and_alignment_of_typ env t)

let rec value_of_const_expr (env:env_t) (e:expr)
  : ML (option (either bool (integer_type & int)))
  =
  match e.v with
  | Constant (Int t n) -> Some (Inr (t, n))
  | Constant (Bool b) -> Some (Inl b)
  | App op [e1; e2] ->
    let v1 = value_of_const_expr env e1 in
    let v2 = value_of_const_expr env e2 in
    begin
    match op, v1, v2 with
    | Plus _,  Some (Inr (t1, n1)), Some (Inr (t2, n2)) -> Some (Inr (integer_type_lub t1 t2, n1 + n2))
    | Minus _, Some (Inr (t1, n1)), Some (Inr (t2, n2)) -> Some (Inr (integer_type_lub t1 t2, n1 - n2))
    | Mul _,   Some (Inr (t1, n1)), Some (Inr (t2, n2)) -> Some (Inr (integer_type_lub t1 t2, n1 * n2))
    | Division _, Some (Inr (t1, n1)), Some (Inr (t2, n2)) ->
      if n2 = 0
      then error ("Division by zero in constant expression") e2.range
      else Some (Inr (integer_type_lub t1 t2, n1 / n2))
    | GT _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 > n2))
    | LT _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 < n2))
    | GE _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 >= n2))
    | LE _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 <= n2))
    | And, Some (Inl b1), Some (Inl b2) -> Some (Inl (b1 && b2))
    | Or, Some (Inl b1), Some (Inl b2) -> Some (Inl (b1 || b2))
    | _ -> None
    end
  | App Not [e] ->
    let v = value_of_const_expr env e in
    begin
    match v with
    | Some (Inl b) -> Some (Inl (not b))
    | _ -> None
    end
  | App SizeOf [{v=Identifier t}] ->
    begin
    try
      match size_of_typ env (with_range (Type_app t KindSpec []) t.range) with
      | Fixed n
      | WithVariableSuffix n -> Some (Inr (UInt32, n))
      | _ -> None
    with
      | _ -> None
    end
  | App (Cast _ t) [e] ->
    let v = value_of_const_expr env e in
    begin
    match v with
    | Some (Inr (_, n)) ->
      Some (Inr (t, n))
    | _ -> None
    end
  | Identifier i ->
    begin
    match B.lookup_macro_definition (fst env) i with
    | Some e ->
      value_of_const_expr env e
    | _ -> None
    end
  | _ -> None

let size_and_alignment_of_atomic_field (env:env_t) (f:atomic_field)
  : ML (size & alignment)
  = let base_size, align = size_and_alignment_of_typ env f.v.field_type in
    let size =
      match f.v.field_array_opt with
      | FieldScalar ->
        base_size

      | FieldArrayQualified (n, ByteArrayByteSize) ->
        if base_size <> Fixed 1
        then warning "Expected a byte array; if the underlying array elements are larger than a byte, use the '[:byte-size' notation"
                     f.range;
        let n = value_of_const_expr env n in
        begin
        match n with
        | Some (Inr (_, k)) ->
          Fixed k
        | _ ->
          Variable
        end

      | FieldString (Some n)
      | FieldArrayQualified (n, ArrayByteSize)
      | FieldArrayQualified (n, ArrayByteSizeSingleElementArray) ->
        let n = value_of_const_expr env n in
        begin
        match n with
        | Some (Inr (_, k)) -> Fixed k

        | _ ->
          Variable
        end

      | _ -> Variable
    in
    size, align

#push-options "--warn_error -272"
let gen_alignment_ident
  : unit -> ML ident
  = let ctr : ref int = alloc 0 in
    fun () ->
      let next = !ctr in
      ctr := next + 1;
      with_range
        (to_ident' (Printf.sprintf "%salignment_padding_%d" Ast.reserved_prefix next))
        dummy_range
#pop-options

let padding_field (env:env_t) (diag_enclosing_type_name:ident (* for diagnostics only *)) (padding_msg:string) (n:int)
  : ML (list field)
  =
  if n <= 0
  then []
  else (
    let field_name = gen_alignment_ident() in
    let n_expr = with_range (Constant (Int UInt32 n)) dummy_range in
    let nm = ident_to_string diag_enclosing_type_name in
    FStar.IO.print_string
      (Printf.sprintf "Adding padding field in %s for %d bytes at %s\n"
                       nm
                       n
                       padding_msg);
    let sf = {
      field_dependence = false;
      field_ident = field_name;
      field_type = tuint8;
      field_array_opt=(if n = 1 then FieldScalar else FieldArrayQualified(n_expr, ByteArrayByteSize));
      field_constraint=None;
      field_bitwidth=None;
      field_action=None
    } in
    let af = with_dummy_range sf in
    let f = with_dummy_range (AtomicField af) in
    [f]
  )

let should_align (td:typedef_names)
  : bool
  = List.Tot.Base.mem Aligned td.typedef_attributes

let alignment_padding env (should_align:bool) 
                          (diag_enclosing_type_name:ident (* for diagnostics only *))
                          (msg:string)
                          (offset:size)
                          (a:alignment)
  : ML (int & list field)
  = if not should_align
    then 0, []
    else (
      let pad_size =
          match offset, a with
          | _, None ->
            0 //no alignment for this type
          | Fixed o, Some n ->
            if o % n = 0
            then 0 //already aligned
            else n - (o % n)
          | _ ->
            //variable offset;
            //this is beyond what is expressed in C
            //no alignment needed
            0
      in
      pad_size,
      padding_field env diag_enclosing_type_name msg pad_size
    )
val sum_size : n: TypeSizes.size -> m: TypeSizes.size -> TypeSizes.size
n: TypeSizes.size -> m: TypeSizes.size -> TypeSizes.size