val size_and_alignment_of_atomic_field (env: env_t) (f: atomic_field) : ML (size & alignment)
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
val size_and_alignment_of_atomic_field (env: env_t) (f: atomic_field) : ML (size & alignment)
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
    (match n with
      | Some (Inr (_, k)) -> Fixed k
      | _ -> Variable)
  | FieldString (Some n)
  | FieldArrayQualified (n, ArrayByteSize)
  | FieldArrayQualified (n, ArrayByteSizeSingleElementArray) ->
    let n = value_of_const_expr env n in
    (match n with
      | Some (Inr (_, k)) -> Fixed k
      | _ -> Variable)
  | _ -> Variable
in
size, align
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.env_t Ast.atomic_field TypeSizes.size TypeSizes.alignment FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.tuple2 Ast.__proj__Mkatomic_field'__item__field_array_opt Ast.__proj__Mkwith_meta_t__item__v Ast.atomic_field' Ast.expr Ast.integer_type Prims.int TypeSizes.Fixed FStar.Pervasives.Native.option Ast.either Prims.bool TypeSizes.Variable TypeSizes.value_of_const_expr Prims.unit Prims.op_disEquality Ast.warning Ast.__proj__Mkwith_meta_t__item__range Ast.field_array_t TypeSizes.size_and_alignment_of_typ Ast.__proj__Mkatomic_field'__item__field_type
(*
   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)
val size_and_alignment_of_atomic_field (env: env_t) (f: atomic_field) : ML (size & alignment)
env: TypeSizes.env_t -> f: Ast.atomic_field -> FStar.All.ML (TypeSizes.size * TypeSizes.alignment)