let with_dummy_range x = with_range x dummy_range
let with_dummy_range x =
with_range x dummy_range
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.with_range Ast.dummy_range Ast.with_meta_t
(*
   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

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

/// Integer, hex and boolean constants
[@@ PpxDerivingYoJson ]
type constant =
  | Unit
  | Int : integer_type -> int -> constant
  | XInt: integer_type -> string -> constant   //hexadecimal constants
  | Bool of bool

/// Operators supported in refinement expressions
[@@ PpxDerivingYoJson ]
type op =
  | Eq
  | Neq
  | And
  | Or
  | Not
  | Plus of option integer_type
  | Minus of option integer_type
  | Mul of option integer_type
  | Division of option integer_type
  | Remainder of option integer_type
  | BitwiseAnd of option integer_type
  | BitwiseXor of option integer_type
  | BitwiseOr of option integer_type
  | BitwiseNot of option integer_type
  | ShiftRight of option integer_type
  | ShiftLeft of option integer_type
  | LT of option integer_type
  | GT of option integer_type
  | LE of option integer_type
  | GE of option integer_type
  | IfThenElse
  | BitFieldOf: sz: int -> order: bitfield_bit_order -> op //BitFieldOf_n(i, from, to); the integer is the size of i in bits
  | SizeOf
  | Cast : from:option integer_type -> to:integer_type -> op
  | Ext of string
  //OffsetOf ?

/// Expressions used in refinements
///   Expressions have no binding structure
///   Names are represented using concrete identifiers, i.e., strings
///   We enforce that all names are unique in a scope, i.e., no shadowing allowed
[@@ PpxDerivingYoJson ]
noeq
type expr' =
  | Constant of constant
  | Identifier of ident
  | Static of expr //the guard of a #if; must be made from compile-time constants only
  | This
  | App : op -> list expr -> expr'

and expr = with_meta_t expr'

/// A non-pointer type in the AST (see typ below) may be
///   - A spec type, i.e. a type that has an interpretation in 3d, that 3d understands
///   - An output type, may be used as the type of the parse tree constructed as part of actions
///     This includes structs and unions, and actions support assignment to fields of output types
///   - An extern type, an abstract, uninterpreted type

[@@ PpxDerivingYoJson ]
type t_kind =
  | KindSpec
  | KindOutput
  | KindExtern

/// Syntax for output expressions
///
/// Output expressions may appear as type parameters or as lhs of assignment actions

[@@ PpxDerivingYoJson ]
noeq
type out_expr' =
  | OE_id     : ident -> out_expr'
  | OE_star   : out_expr -> out_expr'
  | OE_addrof : out_expr -> out_expr'
  | OE_deref  : out_expr -> ident -> out_expr'  //deref a field
  | OE_dot    : out_expr -> ident -> out_expr'  //read a field

/// Output expressions maintain metadata
///   (base type, type of the expr and its bitwidth, in case the expression is of a bitfield type)
///
/// where base type is the type of the base identifier,
///       and type of the output expression
///
/// The metadata is initially None after parsing,
///   and is populated after typechecking (in Binding.fst)
///
/// It is used during emitting F* and C code
/// For each output expression, we emit an action (external function call)
///   whose signature requires all this
///
/// TODO: could we also store the source string for pretty printing?

and out_expr_meta_t = {
  out_expr_base_t : typ;
  out_expr_t : typ;
  out_expr_bit_width : option int;
}

and out_expr = { out_expr_node: with_meta_t out_expr';
                 out_expr_meta: option out_expr_meta_t }


/// A type parameter is either an expression or an output expression

and typ_param = either expr out_expr

/// Types: all types are named and fully instantiated to expressions only
///   i.e., no type-parameterized types
///
/// The t_kind field maintains the kind
///
/// It is set during the desugaring phase, the parser always sets it to KindSpec
///   We could move it to the parser itself
///
/// Keeping this makes it easy to check whether a type is an output type or an extern type
///   Alternatively we would have to carry some environment along


and typ' =
  | Type_app : ident -> t_kind -> list typ_param -> typ'
  | Pointer : typ -> typ'
and typ = with_meta_t typ'

let field_typ = t:typ { Type_app? t.v }

[@@ PpxDerivingYoJson ]
noeq
type atomic_action =
  | Action_return of expr
  | Action_abort
  | Action_field_pos_64
  | Action_field_pos_32
  | Action_field_ptr
  | Action_field_ptr_after: sz:expr -> write_to:out_expr -> atomic_action
  | Action_deref of ident
  | Action_assignment : lhs:out_expr -> rhs:expr -> atomic_action
  | Action_call : f:ident -> args:list expr -> atomic_action

noeq
[@@ PpxDerivingYoJson ]
type action' =
  | Atomic_action of atomic_action
  | Action_seq : hd:atomic_action -> tl:action -> action'
  | Action_ite : hd:expr -> then_:action -> else_:option action -> action'
  | Action_let : i:ident -> a:atomic_action -> k:action -> action'
  | Action_act : action -> action'
and action = with_meta_t action'
open FStar.List.Tot

let sequence_non_failing_actions (a0:action{Action_act? a0.v}) (a1:action {Action_act? a1.v})
  : a:action{Action_act? a.v}
  = let rec seq (a0:action) = 
      let w a = 
          with_range_and_comments a 
            a1.range
            (a0.comments @ a1.comments)
      in
      let Action_act a1 = a1.v in
      match a0.v with
      | Atomic_action a -> 
        w (Action_seq a a1)
  
      | Action_seq a0 tl ->
        w (Action_seq a0 (seq tl))
  
      | Action_ite hd th el ->
        let th = seq th in
        let el = 
          match el with
          | None -> Some a1
          | Some el -> Some (seq el)
        in
        w (Action_ite hd th el)
  
      | Action_let i a k ->
        w (Action_let i a (seq k))
  
      | Action_act a ->
        seq a
    in
    let res = seq a0 in
    with_range_and_comments (Action_act res)
      res.range
      res.comments
            

[@@ PpxDerivingYoJson ]
type qualifier =
  | Immutable
  | Mutable

/// Parameters: Type definitions can be parameterized by values
///   Parameters have a name and are always annoted with their type
[@@ PpxDerivingYoJson ]
type param =  typ & ident & qualifier

[@@ PpxDerivingYoJson ]
noeq
type bitfield_attr' = {
  bitfield_width : int;
  bitfield_identifier : int;
  bitfield_type : typ;
  bitfield_from : int;
  bitfield_to: int
}
and bitfield_attr = with_meta_t bitfield_attr'

[@@ PpxDerivingYoJson ]
let field_bitwidth_t = either (with_meta_t int) bitfield_attr

[@@ PpxDerivingYoJson ]
type array_qualifier =
  | ByteArrayByteSize  //[
  | ArrayByteSize      //[:byte-size
  | ArrayByteSizeAtMost //[:byte-size-at-most
  | ArrayByteSizeSingleElementArray //[:byte-size-single-element-array

[@@ PpxDerivingYoJson ]
noeq
type field_array_t =
  | FieldScalar
  | FieldArrayQualified of (expr & array_qualifier) //array size in bytes, the qualifier indicates whether this is a variable-length suffix or not
  | FieldString of (option expr)

[@@ PpxDerivingYoJson ]
noeq
type atomic_field' = {
  field_dependence:bool;   //computed; whether or not the rest of the struct depends on this field
  field_ident:ident;       //name of the field
  field_type:typ;          //type of the field
  field_array_opt: field_array_t;
  field_constraint:option expr; //refinement constraint
  field_bitwidth:option field_bitwidth_t;  //bits used for the field; elaborate from Inl to Inr
  field_action:option (action & bool); //boo indicates if the action depends on the field value
}

and atomic_field = with_meta_t atomic_field'

and field' =
  | AtomicField of atomic_field
  | RecordField : record -> ident -> field'
  | SwitchCaseField : switch_case -> ident -> field'

and field = with_meta_t field'

and record = list field

and case =
  | Case : expr -> field -> case
  | DefaultCase : field -> case

and switch_case = expr & list case


[@@ PpxDerivingYoJson ]
type attribute =
  | Entrypoint
  | Aligned

/// Typedefs are given 2 names by convention and can be tagged as an
/// "entrypoint" for the validator
///
///   E.g.,
///    typedef [entrypoint] struct _T { ... } T, *PTR_T;
[@@ PpxDerivingYoJson ]
noeq
type typedef_names = {
  typedef_name: ident;
  typedef_abbrev: ident;
  typedef_ptr_abbrev: ident;
  typedef_attributes: list attribute
}

[@@ PpxDerivingYoJson ]
let enum_case = ident & option (either int ident)

/// Specification of output types
///
/// Output types contain atomic fields with optional bitwidths for bitfield types,
///   but they may also contain anonymous structs and unions

[@@ PpxDerivingYoJson ]
noeq
type out_field =
  | Out_field_named: ident -> typ -> bit_width:option int -> out_field
  | Out_field_anon : list out_field -> is_union:bool -> out_field

[@@ PpxDerivingYoJson ]
noeq
type out_typ = {
  out_typ_names    : typedef_names;
  out_typ_fields   : list out_field;
  out_typ_is_union : bool;  //TODO: unclear if this field is needed
}

/// A 3d specification a list of declarations
///   - Define: macro definitions for constants
///   - TypeAbbrev: macro definition of types
///   - Enum: enumerated type using existing constants or newly defined constants
///   - Record: a struct with refinements
///   - CaseType: an untagged union
///
///   - OutputType: an output type definition
///       no validators are generated for these types,
///       they are used only in the parse trees construction in the actions
///   - ExternType: An abstract type declaration
///   - ExternFn: An abstract function declaration, may be used in the actions

[@@ PpxDerivingYoJson ]
noeq
type decl' =
  | ModuleAbbrev: ident -> ident -> decl'
  | Define: ident -> option typ -> constant -> decl'
  | TypeAbbrev: typ -> ident -> decl'
  | Enum: typ -> ident -> list enum_case -> decl'
  | Record: names:typedef_names -> params:list param -> where:option expr -> fields:record -> decl'
  | CaseType: typedef_names -> list param -> switch_case -> decl'

  | OutputType : out_typ -> decl'
  | ExternType : typedef_names -> decl'
  | ExternFn   : ident -> typ -> list param -> decl'

[@@ PpxDerivingYoJson ]
noeq
type decl = {
  d_decl : with_meta_t decl';
  d_exported : bool
}

let mk_decl (d:decl') r c (is_exported:bool) : decl =
  { d_decl = with_range_and_comments d r c;
    d_exported = is_exported }

let decl_with_v (d:decl) (v:decl') : decl =
  { d with d_decl = { d.d_decl with v = v } }

[@@ PpxDerivingYoJson ]
noeq
type type_refinement = {
  includes:list string;
  type_map:list (ident * option ident)
}

[@@ PpxDerivingYoJson ]
let prog = list decl & option type_refinement

////////////////////////////////////////////////////////////////////////////////
// Utilities
////////////////////////////////////////////////////////////////////////////////

(** Entrypoint and export definitions *)

let has_entrypoint (l:list attribute) : Tot bool =
  Some? (List.Tot.tryFind (function Entrypoint -> true | _ -> false) l)

let is_entrypoint_or_export d = match d.d_decl.v with
  | Record names _ _ _
  | CaseType names _ _ ->
    if has_entrypoint (names.typedef_attributes)
    then true
    else d.d_exported
  | _ -> d.d_exported

let is_entrypoint d = match d.d_decl.v with
  | Record names _ _ _
  | CaseType names _ _ ->
    has_entrypoint (names.typedef_attributes)
  | _ -> false

(** Determine if there are output type expressions: which cases in
   TranslateForInterpreter introduce the Output_type_expr constructor?
   *)

/// Matches translate_action_assignment, translate_action_field_ptr_after
let out_expr_is_out_type_expr (lhs: out_expr) : Tot bool =
  match lhs.out_expr_node.v with
  | OE_star ({out_expr_node = {v=OE_id i}}) -> false
  | _ -> true

/// Matches translate_atomic_action
let atomic_action_has_out_expr (a: atomic_action) : Tot bool =
  match a with
  | Action_field_ptr_after _ write_to
  | Action_assignment write_to _
    -> out_expr_is_out_type_expr write_to
  | _ -> false

/// Matches translate_action
let rec action_has_out_expr (a: action) : Tot bool =
  match a.v with
  | Atomic_action a -> atomic_action_has_out_expr a
  | Action_seq hd tl ->
    if atomic_action_has_out_expr hd
    then true
    else action_has_out_expr tl
  | Action_ite _ then_ (Some else_) ->
    if action_has_out_expr then_
    then true
    else action_has_out_expr else_
  | Action_ite _ then_ None ->
    action_has_out_expr then_
  | Action_let _ a k ->
    if atomic_action_has_out_expr a
    then true
    else action_has_out_expr k
  | Action_act a ->
    action_has_out_expr a

let field_action_has_out_expr 
  (f: option (action & bool))
: Tot bool
= match f with
  | None -> false
  | Some (a, _) -> action_has_out_expr a

/// Matches translate_atomic_field
let atomic_field_has_out_expr (f: atomic_field) : Tot bool =
  let sf = f.v in
  field_action_has_out_expr sf.field_action

/// Matches field_as_grouped_fields
let rec field_has_out_expr (f: field) : Tot bool =
  match f.v with
  | AtomicField af ->
    atomic_field_has_out_expr af
  | RecordField fs _ ->
    record_has_out_expr fs
  | SwitchCaseField sw _ ->
    switch_case_has_out_expr sw

and record_has_out_expr (fs: record) : Tot bool =
  match fs with
  | [] -> false
  | f :: fs' ->
    if field_has_out_expr f
    then true
    else record_has_out_expr fs'

and switch_case_has_out_expr (sw: switch_case) : Tot bool =
  let (_, c) = sw in
  cases_have_out_expr c

and cases_have_out_expr (cs: list case) : Tot bool =
  match cs with
  | [] -> false
  | c :: cs ->
    if case_has_out_expr c
    then true
    else cases_have_out_expr cs

and case_has_out_expr (c: case) : Tot bool =
  match c with
  | Case _ f
  | DefaultCase f
    ->
    field_has_out_expr f

/// Matches parse_field
let decl_has_out_expr (d: decl) : Tot bool =
  match d.d_decl.v with
  | Record _ _ _ ast_fields ->
    record_has_out_expr ast_fields
  | CaseType _ _ switch_case ->
    switch_case_has_out_expr switch_case
  | _ -> false

(** Equality on expressions and types **)

/// eq_expr partially decides equality on expressions, by requiring
/// syntactic equality

let rec eq_expr (e1 e2:expr) : Tot bool (decreases e1) =
  match e1.v, e2.v with
  | Constant i, Constant j -> i = j
  | Identifier i, Identifier j -> i.v = j.v
  | This, This -> true
  | App op1 es1, App op2 es2 ->
    op1 = op2
    && eq_exprs es1 es2
  | _ -> false

and eq_exprs (es1 es2:list expr) : Tot bool =
  match es1, es2 with
  | [], [] -> true
  | hd1::es1, hd2::es2 -> eq_expr hd1 hd2 && eq_exprs es1 es2
  | _ -> false

let eq_idents (i1 i2:ident) : Tot bool =
  i1.v.modul_name = i2.v.modul_name && i1.v.name = i2.v.name

/// eq_typ: syntactic equalty of types

let rec eq_out_expr (o1 o2:out_expr) : bool =
  match o1.out_expr_node.v, o2.out_expr_node.v with
  | OE_id i1, OE_id i2 -> eq_idents i1 i2
  | OE_star o1, OE_star o2
  | OE_addrof o1, OE_addrof o2 -> eq_out_expr o1 o2
  | OE_deref o1 i1, OE_deref o2 i2
  | OE_dot o1 i1, OE_dot o2 i2 -> eq_idents i1 i2 && eq_out_expr o1 o2
  | _ -> false

let eq_typ_param (p1 p2:typ_param) : bool =
  match p1, p2 with
  | Inl e1, Inl e2 -> eq_expr e1 e2
  | Inr o1, Inr o2 -> eq_out_expr o1 o2
  | _ -> false

let rec eq_typ_params (ps1 ps2:list typ_param) : bool =
  match ps1, ps2 with
  | [], [] -> true
  | p1::ps1, p2::ps2 -> eq_typ_param p1 p2 && eq_typ_params ps1 ps2
  | _ -> false

let rec eq_typ (t1 t2:typ) : Tot bool =
  match t1.v, t2.v with
  | Type_app hd1 k1 ps1, Type_app hd2 k2 ps2 ->
    eq_idents hd1 hd2
    && k1 = k2
    && eq_typ_params ps1 ps2
  | Pointer t1, Pointer t2 ->
    eq_typ t1 t2
  | _ -> false

(** Common AST constants and builders **)
val with_dummy_range : x: _ -> Ast.with_meta_t _
x: _ -> Ast.with_meta_t _