val bit_order_of (i: ident) : ML bitfield_bit_order
let bit_order_of (i:ident) : ML bitfield_bit_order =
  match maybe_bit_order_of i with
  | None -> error ("Unknown integer type: " ^ ident_to_string i) i.range
  | Some t -> t
val bit_order_of (i: ident) : ML bitfield_bit_order
let bit_order_of (i: ident) : ML bitfield_bit_order =
match maybe_bit_order_of i with
| None -> error ("Unknown integer type: " ^ ident_to_string i) i.range
| Some t -> t
Ast.fst.checked
prims.fst.checked Options.fsti.checked Hashtable.fsti.checked FStar.UInt.fsti.checked FStar.String.fsti.checked FStar.ST.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Ast.fst
Ast.ident Ast.maybe_bit_order_of Ast.error Ast.bitfield_bit_order Prims.op_Hat Ast.ident_to_string Ast.__proj__Mkwith_meta_t__item__range Ast.ident'
(*
   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 a 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 Ast
(* The source abstract syntax for the 3d frontend to EverParse *)

open FStar.All

let reserved_prefix = "___"

//redefining either because we need to serialize to Json
[@@ PpxDerivingYoJson ]
type either a b =
  | Inl of a
  | Inr of b

/// pos: Source locations
type pos = {
  filename: string;
  line:int;
  col:int
}

noeq
type comments_buffer_t = {
  push: string & pos & pos -> ML unit;
  flush: unit -> ML (list string);
  flush_until: pos -> ML (list string);
}

#push-options "--warn_error -272" //top-level effect; ok
let comments_buffer : comments_buffer_t =
  let buffer : ref (list (string & pos & pos)) = FStar.ST.alloc [] in
  let buffer_comment (c, s, p) =
    let c = String.substring c 2 (String.length c - 2) in
    buffer := (c, s, p) :: !buffer
  in
  let flush_comments () =
    let cs = !buffer in
    buffer := [];
    (List.rev cs) |> List.map (fun (c, _, _) -> c)
  in
  let flush_until pos : ML (list string) =
    let cs = !buffer in
    let preceding, following =
      List.partition (fun (c, _, end_pos) ->
        Options.debug_print_string
          (Printf.sprintf "Requesting comments until line %d,\nAt line %d we have comment (*%s*)\n"
            pos.line
            end_pos.line
            c);
          end_pos.line <= pos.line) cs
    in
    buffer := following;
    preceding |> List.map (fun (c, _, _) -> c)
  in
  {
    push = buffer_comment;
    flush = flush_comments;
    flush_until = flush_until
  }
#pop-options

let string_of_pos p =
  Printf.sprintf "%s:(%d,%d)" p.filename p.line p.col

/// range: A source extent
let range = pos * pos

/// comment: A list of line comments, i.e., a list of strings
let comments = list string

let string_of_range r =
  let p, q = r in
  if p.filename = q.filename
  then Printf.sprintf "%s:(%d,%d--%d,%d)"
              p.filename p.line p.col q.line q.col
  else Printf.sprintf "%s -- %s"
              (string_of_pos p)
              (string_of_pos q)

let dummy_pos = {
  filename="";
  line=0;
  col=0;
}

noeq
type with_meta_t 'a = {
  v:'a;
  range:range;
  comments: comments
}
(* Override the json serializers for with_meta_t to
   avoid polluting the generated JSON with ranges everywhere *)
let with_meta_t_of_yojson (#a #b #c:Type) (f:(a -> b)) (x:a)
  : ML c
  = failwith "No reading yojson"
let with_meta_t_to_yojson (f:('a -> 'b)) (x:with_meta_t 'a)
  : 'b
  = f x.v
let with_range_and_comments (x:'a) r c : with_meta_t 'a = {
  v = x;
  range = r;
  comments = c
}
let with_range (x:'a) (r:range) : with_meta_t 'a = with_range_and_comments x r []

[@@ PpxDerivingYoJson ]
type ident' = {
  modul_name : option string;
  name : string
}
[@@ PpxDerivingYoJson ]
let ident = with_meta_t ident'

let ident_to_string i = Printf.sprintf "%s%s"
  (match i.v.modul_name with
   | None -> ""
   | Some m -> m ^ ".")
  i.v.name

let ident_name i = i.v.name

exception Error of string

let error #a msg (r:range) : ML a =
  raise (Error (Printf.sprintf "%s: (Error) %s\n" (string_of_pos (fst r)) msg))

let warning msg (r:range) : ML unit =
  FStar.IO.print_string (Printf.sprintf "%s: (Warning) %s\n" (string_of_pos (fst r)) msg)

let check_reserved_identifier (i:ident) =
  let open FStar.String in
  let s = i.v.name in
  if length s >= 3
  && sub s 0 3 = reserved_prefix
  then error "Identifiers cannot begin with \"___\"" i.range

[@@ PpxDerivingYoJson ]
type integer_type =
  | UInt8
  | UInt16
  | UInt32
  | UInt64

let parse_int_suffix (i:string) : string * option integer_type =
    let l = String.length i in
    if l >= 2
    then let suffix = String.sub i (l - 2) 2 in
         let prefix = String.sub i 0 (l - 2) in
         match suffix with
         | "uy" -> prefix, Some UInt8
         | "us" -> prefix, Some UInt16
         | "ul" -> prefix, Some UInt32
         | "uL" -> prefix, Some UInt64
         | _ -> i, None
    else i, None

let smallest_integer_type_of r (i:int) : ML integer_type =
  if FStar.UInt.fits i 8 then UInt8
  else if FStar.UInt.fits i 16 then UInt16
  else if FStar.UInt.fits i 32 then UInt32
  else if FStar.UInt.fits i 64 then UInt64
  else error (Printf.sprintf
                 "Integer %d is too large for all supported fixed-width types"
                 i)
             r

let integer_type_lub (t1 t2: integer_type) : Tot integer_type =
  match t1, t2 with
  | UInt64, _
  | _, UInt64 -> UInt64
  | _, UInt32
  | UInt32, _ -> UInt32
  | _, UInt16
  | UInt16, _ -> UInt16
  | UInt8, UInt8 -> UInt8

let integer_type_leq (t1 t2: integer_type) : bool =
  integer_type_lub t1 t2 = t2

let maybe_as_integer_typ (i:ident) : Tot (option integer_type) =
  if i.v.modul_name <> None
  then None
  else
    match i.v.name with
    | "UINT8" -> Some UInt8
    | "UINT16" -> Some UInt16
    | "UINT32" -> Some UInt32
    | "UINT64" -> Some UInt64
    | "UINT8BE" -> Some UInt8
    | "UINT16BE" -> Some UInt16
    | "UINT32BE" -> Some UInt32
    | "UINT64BE" -> Some UInt64
    | _ -> None

let as_integer_typ (i:ident) : ML integer_type =
  match maybe_as_integer_typ i with
  | None -> error ("Unknown integer type: " ^ ident_to_string i) i.range
  | Some t -> t

/// Bit order for bitfields
[@@ PpxDerivingYoJson ]
type bitfield_bit_order =
  | LSBFirst (* Least-significant bit first (MSVC default) *)
  | MSBFirst (* Most-significant bit first (necessary for many IETF protocols) *)

let maybe_bit_order_of (i:ident) : Pure (option bitfield_bit_order)
  (requires True)
  (ensures (fun y ->
    Some? y == Some? (maybe_as_integer_typ i)
  ))
= if i.v.modul_name <> None
  then None
  else
    match i.v.name with
    | "UINT8" -> Some LSBFirst
    | "UINT16" -> Some LSBFirst
    | "UINT32" -> Some LSBFirst
    | "UINT64" -> Some LSBFirst
    | "UINT8BE" -> Some MSBFirst
    | "UINT16BE" -> Some MSBFirst
    | "UINT32BE" -> Some MSBFirst
    | "UINT64BE" -> Some MSBFirst
    | _ -> None
val bit_order_of (i: ident) : ML bitfield_bit_order
i: Ast.ident -> FStar.All.ML Ast.bitfield_bit_order