%{
(****************************************************************************)
(*                           the diy toolsuite                              *)
(*                                                                          *)
(* Jade Alglave, University College London, UK.                             *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France.                          *)
(*                                                                          *)
(* Copyright 2015-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved.                     *)
(*                                                                          *)
(* This software is governed by the CeCILL-B license under French law and   *)
(* abiding by the rules of distribution of free software. You can use,      *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL        *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt.            *)
(****************************************************************************)

let mk_sym s = Constant.mk_sym s

open CBase
open MemOrder
open CType
open MemOrderOrAnnot
%}

%token EOF
%token <string> NAME
%token <string> BASE_TYPE
%token <string> STRUCT_TYPE
%token <string> ATOMIC_TYPE
%token <string> CONSTVAR
%token <string> CODEVAR
%token <int> PROC
%token LPAR RPAR COMMA LBRACE RBRACE STAR
%token ATOMIC ATOMIC_BASE CHAR INT LONG VOID
%token MUTEX
%token VOLATILE CONST
%token STRUCT

/* Needed for memory mapped regions */
%token COLON SCOPES LEVELS REGIONS
/* Tokens only needed so we can reuse bellextrarules */
%token <int> NUM

/* For shallow parsing */
%token <string> BODY
%type <string CAst.t list * MiscParser.extra_data> shallow_main
%start shallow_main

/* For deep parsing */
%token <string> CONSTANT
%token SEMI EQ EQ_OP NEQ_OP LT LE GT GE
%token XOR PIPE
%token LAND NOT
%token ADD SUB
%token DIV
%token IF ELSE WHILE
%nonassoc LOWER_THAN_ELSE
%nonassoc ELSE
%token <MemOrder.t> MEMORDER
%token LD_EXPLICIT ST_EXPLICIT EXC_EXPLICIT FENCE LOCK UNLOCK SPINLOCK SPINUNLOCK SPINTRYLOCK SPINISLOCKED SCAS WCAS SCAS_EXPLICIT WCAS_EXPLICIT
%token LOAD STORE UNDERFENCE XCHG CMPXCHG
%token   UNDERATOMICOP  UNDERATOMICOPRETURN UNDERATOMICFETCHOP UNDERATOMICADDUNLESS
%token SRCU
%token <CBase.op> ATOMIC_FETCH_EXPLICIT

%left PIPE
%left XOR
%left LAND

%nonassoc EQ_OP NEQ_OP LT LE GT GE
%left ADD SUB
%left STAR DIV
%nonassoc CAST
%left ECALL
%left ESRCU
%left SEMI

%type <(CBase.pseudo list) CAst.test list * MiscParser.extra_data> deep_main
%start deep_main

%type <CBase.pseudo list> pseudo_seq
%start pseudo_seq

%type <CBase.macro list> macros
%start macros

%%

parameter_list:
| { [] }
| parameter_declaration { [ $1 ] }
| parameter_declaration COMMA parameter_list { $1 :: $3 }

parameter_declaration:
| typ_ptr NAME { {CAst.param_ty = $1; param_name = $2} }

typ_ptr:
| typ STAR { Pointer $1 }
| void STAR { Pointer $1 }

void:
| VOID { Base "void" }


typ_par:
|t=typ { t }
| LPAR t=typ RPAR { t }

typ:
| typ_ptr { $1 }
| typ_par VOLATILE { Volatile $1 }
| typ_par CONST { CType.Const $1 }
| ATOMIC base { Atomic $2 }
| VOLATILE base { Volatile $2 }
| CONST base { Const $2 }
| base0 { $1 }

base0:
| ATOMIC_TYPE { Atomic (Base $1) }
| ATOMIC_BASE LT BASE_TYPE GT { Atomic (Base $3) }
| BASE_TYPE { (Base $1) }
| STRUCT STRUCT_TYPE { Base ("struct " ^ $2) }
| ty_attr MUTEX { Base ($1 ^ "mutex") }
| ty_attr CHAR { Base ($1 ^ "char") }
| ty_attr INT { Base ($1 ^ "int") }
| ty_attr LONG { Base ($1 ^ "long") }



base:
| base0 { $1 }
| LPAR typ RPAR  { $2 }

ty_attr:
| { "" }

shallow_main:
| scopes_and_memory_map EOF { [], [MiscParser.BellExtra $1] }
| BODY shallow_main { CAst.Global $1 :: (fst $2), (snd $2) }
| voidopt PROC LPAR parameter_list RPAR BODY shallow_main
    { CAst.Test {CAst.proc = $2; params = $4; body = $6} :: (fst $7),
      (snd $7) }

voidopt:
| VOID { () }
| VOID STAR { () }
| { () }

declaration:
| typ NAME SEMI { DeclReg ($1,$2) }

initialisation:
| typ NAME EQ expr { StoreReg (Some $1,Some $2,$4) ; }
| expr_only { $1 }

expr_only:
| e=expr { StoreReg(None,None,e) }

atomic_op:
| ADD { Op.Add }
| SUB { Op.Sub }
| LAND { Op.And }
| XOR { Op.Xor }
| PIPE { Op.Or }
| LAND NOT { Op.AndNot2 }

annot:
| annot_base  { $1 }
| annot_base SUB annot { $1 ^ "-" ^ $3 }

annot_base :
| LOCK       { "lock" }
| UNLOCK     { "unlock" }
| ATOMIC_BASE { "atomic" }
| NAME { $1 }



annot_list:
| annot COMMA annot_list
  {$1::$3}
| annot
  {[$1]}

expr:
| expr0 { $1 }
| expr1 { $1 }

expr0:
| CONSTANT { CBase.Const(Constant.Concrete $1) }
| CONSTVAR { CBase.Const(mk_sym $1) }
| NAME { CBase.LoadReg $1 }
| STAR NAME { CBase.LoadMem (CBase.LoadReg $2,AN []) }
| LPAR expr RPAR { $2 }

expr1:
| LPAR typ RPAR e=expr %prec CAST { e }
| STAR LPAR typ RPAR NAME { LoadMem (LoadReg $5,AN []) }
| STAR LPAR expr RPAR { LoadMem ($3,AN []) }
| LOAD LBRACE annot_list RBRACE LPAR expr RPAR { LoadMem($6,AN $3) }
| SRCU LBRACE annot_list RBRACE LPAR expr RPAR %prec ESRCU { ExpSRCU($6,$3) }
| LD_EXPLICIT LPAR expr COMMA MEMORDER RPAR { LoadMem($3,MO $5) }
| expr STAR expr { Op(Op.Mul,$1,$3) }
| expr ADD expr { Op(Op.Add,$1,$3) }
| expr SUB expr { Op(Op.Sub,$1,$3) }
| expr DIV expr { Op(Op.Div,$1,$3) }
| expr LAND expr { Op(Op.And,$1,$3) }
| expr PIPE expr { Op(Op.Or,$1,$3) }
| expr XOR expr { Op(Op.Xor,$1,$3) }
| expr EQ_OP expr { Op(Op.Eq,$1,$3) }
| expr NEQ_OP expr { Op(Op.Ne,$1,$3) }
| expr LT expr { Op(Op.Lt,$1,$3) }
| expr GT expr { Op(Op.Gt,$1,$3) }
| expr LE expr { Op(Op.Le,$1,$3) }
| expr GE expr { Op(Op.Ge,$1,$3) }
| EXC_EXPLICIT LPAR expr COMMA expr COMMA MEMORDER RPAR
  { Exchange($3, $5, MO $7) }
| XCHG LBRACE annot_list RBRACE LPAR expr COMMA expr RPAR
  { Exchange($6,$8,AN $3) }
| CMPXCHG LBRACE annot_list RBRACE LPAR expr COMMA expr COMMA expr RPAR
  { CmpExchange($6,$8,$10,$3) }
| ATOMIC_FETCH_EXPLICIT LPAR expr COMMA expr COMMA MEMORDER RPAR
  { Fetch($3, $1, $5, $7) }
| NAME LPAR args RPAR %prec ECALL
  { ECall ($1,$3) }
| WCAS LPAR expr COMMA expr COMMA expr RPAR
  { ECas ($3,$5,$7,SC,SC,false) }
| WCAS_EXPLICIT LPAR expr COMMA expr COMMA expr COMMA MEMORDER COMMA MEMORDER  RPAR
  { ECas ($3,$5,$7,$9,$11,false) }
| SCAS LPAR expr COMMA expr COMMA expr RPAR
  { ECas ($3,$5,$7,SC,SC,true) }
| SCAS_EXPLICIT LPAR expr COMMA expr COMMA expr COMMA MEMORDER COMMA MEMORDER  RPAR
  { ECas ($3,$5,$7,$9,$11,true) }
| SPINTRYLOCK LPAR expr RPAR
  { TryLock ($3,MutexLinux) }
| SPINISLOCKED LPAR expr RPAR
  { IsLocked ($3,MutexLinux) }
| UNDERATOMICOPRETURN LBRACE annot_list RBRACE LPAR expr COMMA atomic_op COMMA expr RPAR
  { AtomicOpReturn($6,$8,$10,OpReturn,$3) }
| UNDERATOMICFETCHOP LBRACE annot_list RBRACE LPAR expr COMMA atomic_op COMMA expr RPAR
  { AtomicOpReturn($6,$8,$10,FetchOp,$3) }
| UNDERATOMICADDUNLESS LBRACE annot_list RBRACE LPAR expr COMMA expr COMMA expr RPAR
  { AtomicAddUnless($6,$8,$10,true,$3) }

args:
| { [] }
| args_ne { $1 }

args_ne:
| expr { [$1] }
| expr COMMA args_ne { $1 :: $3 }

location:
| NAME { LoadReg($1) }
| STAR location { LoadMem($2,AN []) }
| LPAR expr RPAR { $2 }

instruction:
| IF LPAR expr RPAR block_ins %prec LOWER_THAN_ELSE
  { If($3,$5,None) }
| IF LPAR expr RPAR block_ins ELSE block_ins
  { If($3,$5,Some $7) }
| WHILE expr0 block_ins
  { While ($2,$3,0) }
| initialisation SEMI
  { $1 }
| NAME EQ expr SEMI
  { StoreReg(None,Some $1,$3) }
| LPAR VOID RPAR expr SEMI
  { CastExpr $4 }
| STAR location EQ expr SEMI
  { StoreMem($2,$4,AN []) }
| STORE LBRACE annot_list RBRACE LPAR expr COMMA expr RPAR SEMI
  { StoreMem($6,$8,AN $3) }
| SRCU LBRACE annot_list RBRACE LPAR expr RPAR SEMI
  { InstrSRCU($6,$3,None) }
| SRCU LBRACE annot_list RBRACE LPAR expr COMMA expr RPAR SEMI
  { InstrSRCU($6,$3,Some $8) }
| ST_EXPLICIT LPAR expr COMMA expr COMMA MEMORDER RPAR SEMI
  { StoreMem($3, $5, MO $7) }
| LOCK LPAR expr RPAR SEMI
  { Lock ($3,MutexC11) }
| UNLOCK LPAR expr RPAR SEMI
  { Unlock ($3,MutexC11) }
| SPINLOCK LPAR expr RPAR SEMI
  { Lock ($3,MutexLinux) }
| SPINUNLOCK LPAR expr RPAR SEMI
  { Unlock ($3,MutexLinux) }
| UNDERFENCE LBRACE annot_list RBRACE SEMI
  { Fence(AN $3) }
| UNDERATOMICOP opt_annot LPAR expr COMMA atomic_op COMMA expr RPAR SEMI
  { AtomicOp($4,$6,$8,$2) }
| FENCE LPAR MEMORDER RPAR SEMI
  { Fence(MO $3) }
| CODEVAR SEMI
  { Symb $1 }
| NAME LPAR args RPAR SEMI
  { PCall ($1,$3) }

opt_annot:
// For variant lkmmv1, the annotation is simply droped, thus we can use the empty string
| { [""] }
| LBRACE annot_list RBRACE { $2 }

ins_seq:
| block_ins { [$1] }
| block_ins ins_seq { $1::$2 }
| declaration { [$1] }
| declaration ins_seq { $1::$2 }

block_ins:
| instruction { $1 }
| LBRACE ins_seq RBRACE { Seq($2,true) }

do_pseudo_seq:
| block_ins { [Instruction $1] }
| block_ins do_pseudo_seq { (Instruction $1)::$2 }
| declaration { [] }
| declaration do_pseudo_seq { $2 }

pseudo_seq:
| p=do_pseudo_seq EOF { p }

function_def:
| voidopt PROC LPAR parameter_list RPAR LBRACE do_pseudo_seq RBRACE
  { { CAst.proc = $2;
      CAst.params = $4;
      CAst.body = $7 } }

trans_unit:
| function_def
  { [$1] }
| trans_unit function_def
  { $1 @ [$2] }

deep_main:
| trans_unit scopes_and_memory_map EOF { $1, [MiscParser.BellExtra $2] }

formals_ne:
| NAME { [ $1 ] }
| NAME COMMA formals_ne { $1 :: $3 }

formals:
| { [] }
| formals_ne { $1 }

body:
| LBRACE ins_seq RBRACE { Seq ($2,true) }

macro:
| NAME LPAR formals RPAR expr { EDef ($1,$3,$5) }
| NAME LPAR formals RPAR body { PDef ($1,$3,$5) }

macros:
| ms=list(macro) EOF { ms }