diff --git a/.gitattributes b/.gitattributes index d070f9fe..099cffef 100644 --- a/.gitattributes +++ b/.gitattributes @@ -5,3 +5,14 @@ dune.generated linguist-generated mill linguist-generated mill.bat linguist-generated + +libASL/bnfc/AbsSemantics.ml linguist-generated +libASL/bnfc/LexSemantics.mll linguist-generated +libASL/bnfc/ParSemantics.mly linguist-generated +libASL/bnfc/SkelSemantics.ml linguist-generated +libASL/bnfc/PrintSemantics.ml linguist-generated +libASL/bnfc/ShowSemantics.ml linguist-generated +libASL/bnfc/TestSemantics.ml linguist-generated +libASL/bnfc/BNFC_Util.ml linguist-generated +libASL/bnfc/Makefile linguist-generated + diff --git a/libASL/bnfc/.gitignore b/libASL/bnfc/.gitignore new file mode 100644 index 00000000..a05a8705 --- /dev/null +++ b/libASL/bnfc/.gitignore @@ -0,0 +1,4 @@ +*.bak +*.cmo +*.cmi +/TestSemantics diff --git a/libASL/bnfc/AbsSemantics.ml b/libASL/bnfc/AbsSemantics.ml new file mode 100644 index 00000000..74726c83 --- /dev/null +++ b/libASL/bnfc/AbsSemantics.ml @@ -0,0 +1,166 @@ +(* File generated by the BNF Converter (bnfc 2.9.5). *) + +type binary = Binary of string +and stmtLines = + StmtLinesStmt of stmt + +and stmt = + Stmt_Assign of lexpr * expr + | Stmt_ConstDecl of typeT * string * expr + | Stmt_VarDecl of typeT * string * expr + | Stmt_VarDeclsNoInit of typeT * string list + | Stmt_Assert of expr + | Stmt_Throw of string + | Stmt_TCall of callName * int list * expr list + | Stmt_If of expr * stmt list * stmt list + +and regTypeSlices = + Slice_HiLo of expr + +and typeT = + Type_Bits of int + | Type_Boolean + | Type_Constructor of string + +and lexpr = + Lexpr_KnownVar of varName + | Lexpr_LocalVar of string + | Lexpr_Field of structName * structField + | Lexpr_Array of arrayName * int + +and expr = + Expr_True + | Expr_False + | Expr_KnownVar of varName + | Expr_LocalVar of string + | Expr_Prim of primName * int list * expr list + | Expr_VecPrim of vecPrimName * int list * expr list + | Expr_Slices of expr * slice + | Expr_Field of structName * structField + | Expr_Array of arrayName * int + | Expr_LitInt of int + | Expr_LitBits of binary + +and slice = + Slice_LoWd of int * int + +and varName = + Var_PC + | Var_SP_EL0 + | Var_FPCR + | Var_FPSR + | Var_BTypeCompatible + | Var_BranchTaken + | Var_BTypeNext + | Var_ExclusiveLocal + +and structName = + Struct_Pstate + +and structField = + Field_N + | Field_Z + | Field_C + | Field_V + | Field_A + | Field_D + | Field_DIT + | Field_F + | Field_I + | Field_PAN + | Field_SP + | Field_SSBS + | Field_TCO + | Field_UAO + | Field_BTYPE + +and arrayName = + Array_R + | Array_Z + +and callName = + Call_Mem_set + | Call_AtomicStart + | Call_AtomicEnd + | Call_Memtag_read + | Call_Memtag_set + +and primName = + Prim_Mem_read + | Prim_and_bool + | Prim_or_bool + | Prim_not_bool + | Prim_cvt_bits_uint + | Prim_eq_bits + | Prim_ne_bits + | Prim_not_bits + | Prim_cvt_bool_bv + | Prim_or_bits + | Prim_eor_bits + | Prim_and_bits + | Prim_add_bits + | Prim_sub_bits + | Prim_sdiv_bits + | Prim_sle_bits + | Prim_slt_bits + | Prim_mul_bits + | Prim_append_bits + | Prim_lsr_bits + | Prim_lsl_bits + | Prim_asr_bits + | Prim_replicate_bits + | Prim_ZeroExtend + | Prim_SignExtend + | Prim_FPCompare + | Prim_FPCompareEQ + | Prim_FPCompareGE + | Prim_FPCompareGT + | Prim_FPAdd + | Prim_FPSub + | Prim_FPMulAdd + | Prim_FPMulAddH + | Prim_FPMulX + | Prim_FPMul + | Prim_FPDiv + | Prim_FPMin + | Prim_FPMinNum + | Prim_FPMax + | Prim_FPMaxNum + | Prim_FPRecpX + | Prim_FPSqrt + | Prim_FPRecipEstimate + | Prim_UnsignedRSqrtEstimate + | Prim_FPRSqrtEstimate + | Prim_BFAdd + | Prim_BFMul + | Prim_FPConvertBF + | Prim_FPRecipStepFused + | Prim_FPRSqrtStepFused + | Prim_FPToFixed + | Prim_FixedToFP + | Prim_FPConvert + | Prim_FPRoundInt + | Prim_FPRoundIntN + | Prim_FPToFixedJS_impl + +and vecPrimName = + VecPrim_Elem_set + | VecPrim_Elem_read + | VecPrim_add_vec + | VecPrim_sub_vec + | VecPrim_mul_vec + | VecPrim_sdiv_vec + | VecPrim_lsr_vec + | VecPrim_asr_vec + | VecPrim_lsl_vec + | VecPrim_ite_vec + | VecPrim_sle_vec + | VecPrim_slt_vec + | VecPrim_eq_vec + | VecPrim_zcast_vec + | VecPrim_scast_vec + | VecPrim_trunc_vec + | VecPrim_select_vec + | VecPrim_shuffle_vec + | VecPrim_reduce_add + diff --git a/libASL/bnfc/BNFC_Util.ml b/libASL/bnfc/BNFC_Util.ml new file mode 100644 index 00000000..20689a8b --- /dev/null +++ b/libASL/bnfc/BNFC_Util.ml @@ -0,0 +1,6 @@ +(* File generated by the BNF Converter (bnfc 2.9.5). *) + +open Lexing + +(* this should really be in the parser, but ocamlyacc won't put it in the .mli *) +exception Parse_error of Lexing.position * Lexing.position diff --git a/libASL/bnfc/LexSemantics.mll b/libASL/bnfc/LexSemantics.mll new file mode 100644 index 00000000..5eaea8e2 --- /dev/null +++ b/libASL/bnfc/LexSemantics.mll @@ -0,0 +1,77 @@ +(* File generated by the BNF Converter (bnfc 2.9.5). *) + +(* Lexer definition for ocamllex. *) + +(* preamble *) +{ +open ParSemantics +open Lexing + +let symbol_table = Hashtbl.create 115 +let _ = List.iter (fun (kwd, tok) -> Hashtbl.add symbol_table kwd tok) + [(";", SYMB1);("(", SYMB2);(",", SYMB3);(")", SYMB4);("[", SYMB5);("]", SYMB6);("\"boolean\"", SYMB7);("\"TRUE\"", SYMB8);("\"FALSE\"", SYMB9);("\"_PC\"", SYMB10);("\"SP_EL0\"", SYMB11);("\"FPCR\"", SYMB12);("\"FPSR\"", SYMB13);("\"BTypeCompatible\"", SYMB14);("\"__BranchTaken\"", SYMB15);("\"BTypeNext\"", SYMB16);("\"__ExclusiveLocal\"", SYMB17);("\"PSTATE\"", SYMB18);("\"N\"", SYMB19);("\"Z\"", SYMB20);("\"C\"", SYMB21);("\"V\"", SYMB22);("\"A\"", SYMB23);("\"D\"", SYMB24);("\"DIT\"", SYMB25);("\"F\"", SYMB26);("\"I\"", SYMB27);("\"PAN\"", SYMB28);("\"SP\"", SYMB29);("\"SSBS\"", SYMB30);("\"TCO\"", SYMB31);("\"UAO\"", SYMB32);("\"BTYPE\"", SYMB33);("\"_R\"", SYMB34);("\"_Z\"", SYMB35);("\"Mem.set.0\"", SYMB36);("\"AtomicStart.0\"", SYMB37);("\"AtomicEnd.0\"", SYMB38);("\"AArch64.MemTag.read.0\"", SYMB39);("\"AArch64.MemTag.set.0\"", SYMB40);("\"Mem.read.0\"", SYMB41);("\"and_bool.0\"", SYMB42);("\"or_bool.0\"", SYMB43);("\"not_bool.0\"", SYMB44);("\"cvt_bits_uint.0\"", SYMB45);("\"eq_bits.0\"", SYMB46);("\"ne_bits.0\"", SYMB47);("\"not_bits.0\"", SYMB48);("\"cvt_bool_bv.0\"", SYMB49);("\"or_bits.0\"", SYMB50);("\"eor_bits.0\"", SYMB51);("\"and_bits.0\"", SYMB52);("\"add_bits.0\"", SYMB53);("\"sub_bits.0\"", SYMB54);("\"sdiv_bits.0\"", SYMB55);("\"sle_bits.0\"", SYMB56);("\"slt_bits.0\"", SYMB57);("\"mul_bits.0\"", SYMB58);("\"append_bits.0\"", SYMB59);("\"lsr_bits.0\"", SYMB60);("\"lsl_bits.0\"", SYMB61);("\"asr_bits.0\"", SYMB62);("\"replicate_bits.0\"", SYMB63);("\"ZeroExtend.0\"", SYMB64);("\"SignExtend.0\"", SYMB65);("\"FPCompare.0\"", SYMB66);("\"FPCompareEQ.0\"", SYMB67);("\"FPCompareGE.0\"", SYMB68);("\"FPCompareGT.0\"", SYMB69);("\"FPAdd.0\"", SYMB70);("\"FPSub.0\"", SYMB71);("\"FPMulAdd.0\"", SYMB72);("\"FPMulAddH.0\"", SYMB73);("\"FPMulX.0\"", SYMB74);("\"FPMul.0\"", SYMB75);("\"FPDiv.0\"", SYMB76);("\"FPMin.0\"", SYMB77);("\"FPMinNum.0\"", SYMB78);("\"FPMax.0\"", SYMB79);("\"FPMaxNum.0\"", SYMB80);("\"FPRecpX.0\"", SYMB81);("\"FPSqrt.0\"", SYMB82);("\"FPRecipEstimate.0\"", SYMB83);("\"UnsignedRSqrtEstimate.0\"", SYMB84);("\"FPRSqrtEstimate.0\"", SYMB85);("\"BFAdd.0\"", SYMB86);("\"BFMul.0\"", SYMB87);("\"FPConvertBF.0\"", SYMB88);("\"FPRecipStepFused.0\"", SYMB89);("\"FPRSqrtStepFused.0\"", SYMB90);("\"FPToFixed.0\"", SYMB91);("\"FixedToFP.0\"", SYMB92);("\"FPConvert.0\"", SYMB93);("\"FPRoundInt.0\"", SYMB94);("\"FPRoundIntN.0\"", SYMB95);("\"FPToFixedJS_impl.0\"", SYMB96);("\"Elem.set.0\"", SYMB97);("\"Elem.read.0\"", SYMB98);("\"add_vec.0\"", SYMB99);("\"sub_vec.0\"", SYMB100);("\"mul_vec.0\"", SYMB101);("\"sdiv_vec.0\"", SYMB102);("\"lsr_vec.0\"", SYMB103);("\"asr_vec.0\"", SYMB104);("\"lsl_vec.0\"", SYMB105);("\"ite_vec.0\"", SYMB106);("\"sle_vec.0\"", SYMB107);("\"slt_vec.0\"", SYMB108);("\"eq_vec.0\"", SYMB109);("\"zcast_vec.0\"", SYMB110);("\"scast_vec.0\"", SYMB111);("\"trunc_vec.0\"", SYMB112);("\"select_vec.0\"", SYMB113);("\"shuffle_vec.0\"", SYMB114);("\"reduce_add.0\"", SYMB115)] + +let resword_table = Hashtbl.create 20 +let _ = List.iter (fun (kwd, tok) -> Hashtbl.add resword_table kwd tok) + [("Stmt_Assign", KW_Stmt_Assign);("Stmt_ConstDecl", KW_Stmt_ConstDecl);("Stmt_VarDecl", KW_Stmt_VarDecl);("Stmt_VarDeclsNoInit", KW_Stmt_VarDeclsNoInit);("Stmt_Assert", KW_Stmt_Assert);("Stmt_Throw", KW_Stmt_Throw);("Stmt_TCall", KW_Stmt_TCall);("Stmt_If", KW_Stmt_If);("Slice_HiLo", KW_Slice_HiLo);("Type_Bits", KW_Type_Bits);("Type_Constructor", KW_Type_Constructor);("LExpr_Var", KW_LExpr_Var);("LExpr_Field", KW_LExpr_Field);("LExpr_Array", KW_LExpr_Array);("Expr_Var", KW_Expr_Var);("Expr_TApply", KW_Expr_TApply);("Expr_Slices", KW_Expr_Slices);("Expr_Field", KW_Expr_Field);("Expr_Array", KW_Expr_Array);("Slice_LoWd", KW_Slice_LoWd)] + +let unescapeInitTail (s:string) : string = + let rec unesc s = match s with + '\\'::c::cs when List.mem c ['\"'; '\\'; '\''] -> c :: unesc cs + | '\\'::'n'::cs -> '\n' :: unesc cs + | '\\'::'t'::cs -> '\t' :: unesc cs + | '\\'::'r'::cs -> '\r' :: unesc cs + | '\"'::[] -> [] + | '\''::[] -> [] + | c::cs -> c :: unesc cs + | _ -> [] + (* explode/implode from caml FAQ *) + in let explode (s : string) : char list = + let rec exp i l = + if i < 0 then l else exp (i - 1) (s.[i] :: l) in + exp (String.length s - 1) [] + in let implode (l : char list) : string = + let res = Buffer.create (List.length l) in + List.iter (Buffer.add_char res) l; + Buffer.contents res + in implode (unesc (List.tl (explode s))) + +let incr_lineno (lexbuf:Lexing.lexbuf) : unit = + let pos = lexbuf.lex_curr_p in + lexbuf.lex_curr_p <- { pos with + pos_lnum = pos.pos_lnum + 1; + pos_bol = pos.pos_cnum; + } +} + +(* BNFC character classes *) +let _letter = ['a'-'z' 'A'-'Z' '\192' - '\255'] # ['\215' '\247'] (* isolatin1 letter FIXME *) +let _upper = ['A'-'Z' '\192'-'\221'] # '\215' (* capital isolatin1 letter FIXME *) +let _lower = ['a'-'z' '\222'-'\255'] # '\247' (* small isolatin1 letter FIXME *) +let _digit = ['0'-'9'] (* _digit *) +let _idchar = _letter | _digit | ['_' '\''] (* identifier character *) +let _universal = _ (* universal: any character *) + +(* reserved words consisting of special symbols *) +let rsyms = ";" | "(" | "," | ")" | "[" | "]" | "\"boolean\"" | "\"TRUE\"" | "\"FALSE\"" | "\"_PC\"" | "\"SP_EL0\"" | "\"FPCR\"" | "\"FPSR\"" | "\"BTypeCompatible\"" | "\"__BranchTaken\"" | "\"BTypeNext\"" | "\"__ExclusiveLocal\"" | "\"PSTATE\"" | "\"N\"" | "\"Z\"" | "\"C\"" | "\"V\"" | "\"A\"" | "\"D\"" | "\"DIT\"" | "\"F\"" | "\"I\"" | "\"PAN\"" | "\"SP\"" | "\"SSBS\"" | "\"TCO\"" | "\"UAO\"" | "\"BTYPE\"" | "\"_R\"" | "\"_Z\"" | "\"Mem.set.0\"" | "\"AtomicStart.0\"" | "\"AtomicEnd.0\"" | "\"AArch64.MemTag.read.0\"" | "\"AArch64.MemTag.set.0\"" | "\"Mem.read.0\"" | "\"and_bool.0\"" | "\"or_bool.0\"" | "\"not_bool.0\"" | "\"cvt_bits_uint.0\"" | "\"eq_bits.0\"" | "\"ne_bits.0\"" | "\"not_bits.0\"" | "\"cvt_bool_bv.0\"" | "\"or_bits.0\"" | "\"eor_bits.0\"" | "\"and_bits.0\"" | "\"add_bits.0\"" | "\"sub_bits.0\"" | "\"sdiv_bits.0\"" | "\"sle_bits.0\"" | "\"slt_bits.0\"" | "\"mul_bits.0\"" | "\"append_bits.0\"" | "\"lsr_bits.0\"" | "\"lsl_bits.0\"" | "\"asr_bits.0\"" | "\"replicate_bits.0\"" | "\"ZeroExtend.0\"" | "\"SignExtend.0\"" | "\"FPCompare.0\"" | "\"FPCompareEQ.0\"" | "\"FPCompareGE.0\"" | "\"FPCompareGT.0\"" | "\"FPAdd.0\"" | "\"FPSub.0\"" | "\"FPMulAdd.0\"" | "\"FPMulAddH.0\"" | "\"FPMulX.0\"" | "\"FPMul.0\"" | "\"FPDiv.0\"" | "\"FPMin.0\"" | "\"FPMinNum.0\"" | "\"FPMax.0\"" | "\"FPMaxNum.0\"" | "\"FPRecpX.0\"" | "\"FPSqrt.0\"" | "\"FPRecipEstimate.0\"" | "\"UnsignedRSqrtEstimate.0\"" | "\"FPRSqrtEstimate.0\"" | "\"BFAdd.0\"" | "\"BFMul.0\"" | "\"FPConvertBF.0\"" | "\"FPRecipStepFused.0\"" | "\"FPRSqrtStepFused.0\"" | "\"FPToFixed.0\"" | "\"FixedToFP.0\"" | "\"FPConvert.0\"" | "\"FPRoundInt.0\"" | "\"FPRoundIntN.0\"" | "\"FPToFixedJS_impl.0\"" | "\"Elem.set.0\"" | "\"Elem.read.0\"" | "\"add_vec.0\"" | "\"sub_vec.0\"" | "\"mul_vec.0\"" | "\"sdiv_vec.0\"" | "\"lsr_vec.0\"" | "\"asr_vec.0\"" | "\"lsl_vec.0\"" | "\"ite_vec.0\"" | "\"sle_vec.0\"" | "\"slt_vec.0\"" | "\"eq_vec.0\"" | "\"zcast_vec.0\"" | "\"scast_vec.0\"" | "\"trunc_vec.0\"" | "\"select_vec.0\"" | "\"shuffle_vec.0\"" | "\"reduce_add.0\"" + +(* user-defined token types *) +let binary = '\'' ('0' | '1')+ '\'' + +(* lexing rules *) +rule token = + parse rsyms { let x = lexeme lexbuf in try Hashtbl.find symbol_table x with Not_found -> failwith ("internal lexer error: reserved symbol " ^ x ^ " not found in hashtable") } + | binary { let l = lexeme lexbuf in try Hashtbl.find resword_table l with Not_found -> TOK_Binary l } + | _letter _idchar* + { let l = lexeme lexbuf in try Hashtbl.find resword_table l with Not_found -> TOK_Ident l } + | _digit+ { TOK_Integer (int_of_string (lexeme lexbuf)) } + | _digit+ '.' _digit+ ('e' ('-')? _digit+)? + { TOK_Double (float_of_string (lexeme lexbuf)) } + | '\"' (([^ '\"' '\\' '\n']) | ('\\' ('\"' | '\\' | '\'' | 'n' | 't' | 'r')))* '\"' + { TOK_String (unescapeInitTail (lexeme lexbuf)) } + | '\'' (([^ '\'' '\\']) | ('\\' ('\\' | '\'' | 'n' | 't' | 'r'))) '\'' + { TOK_Char (unescapeInitTail (lexeme lexbuf)).[0] } + | [' ' '\t' '\r'] + { token lexbuf } + | '\n' { incr_lineno lexbuf; token lexbuf } + | eof { TOK_EOF } diff --git a/libASL/bnfc/ParSemantics.mly b/libASL/bnfc/ParSemantics.mly new file mode 100644 index 00000000..3695636b --- /dev/null +++ b/libASL/bnfc/ParSemantics.mly @@ -0,0 +1,363 @@ +/* File generated by the BNF Converter (bnfc 2.9.5). */ + +/* Parser definition for use with menhir */ + +%{ +open AbsSemantics +open Lexing +%} + +%token KW_Stmt_Assign KW_Stmt_ConstDecl KW_Stmt_VarDecl KW_Stmt_VarDeclsNoInit KW_Stmt_Assert KW_Stmt_Throw KW_Stmt_TCall KW_Stmt_If KW_Slice_HiLo KW_Type_Bits KW_Type_Constructor KW_LExpr_Var KW_LExpr_Field KW_LExpr_Array KW_Expr_Var KW_Expr_TApply KW_Expr_Slices KW_Expr_Field KW_Expr_Array KW_Slice_LoWd + +%token SYMB1 /* ; */ +%token SYMB2 /* ( */ +%token SYMB3 /* , */ +%token SYMB4 /* ) */ +%token SYMB5 /* [ */ +%token SYMB6 /* ] */ +%token SYMB7 /* "boolean" */ +%token SYMB8 /* "TRUE" */ +%token SYMB9 /* "FALSE" */ +%token SYMB10 /* "_PC" */ +%token SYMB11 /* "SP_EL0" */ +%token SYMB12 /* "FPCR" */ +%token SYMB13 /* "FPSR" */ +%token SYMB14 /* "BTypeCompatible" */ +%token SYMB15 /* "__BranchTaken" */ +%token SYMB16 /* "BTypeNext" */ +%token SYMB17 /* "__ExclusiveLocal" */ +%token SYMB18 /* "PSTATE" */ +%token SYMB19 /* "N" */ +%token SYMB20 /* "Z" */ +%token SYMB21 /* "C" */ +%token SYMB22 /* "V" */ +%token SYMB23 /* "A" */ +%token SYMB24 /* "D" */ +%token SYMB25 /* "DIT" */ +%token SYMB26 /* "F" */ +%token SYMB27 /* "I" */ +%token SYMB28 /* "PAN" */ +%token SYMB29 /* "SP" */ +%token SYMB30 /* "SSBS" */ +%token SYMB31 /* "TCO" */ +%token SYMB32 /* "UAO" */ +%token SYMB33 /* "BTYPE" */ +%token SYMB34 /* "_R" */ +%token SYMB35 /* "_Z" */ +%token SYMB36 /* "Mem.set.0" */ +%token SYMB37 /* "AtomicStart.0" */ +%token SYMB38 /* "AtomicEnd.0" */ +%token SYMB39 /* "AArch64.MemTag.read.0" */ +%token SYMB40 /* "AArch64.MemTag.set.0" */ +%token SYMB41 /* "Mem.read.0" */ +%token SYMB42 /* "and_bool.0" */ +%token SYMB43 /* "or_bool.0" */ +%token SYMB44 /* "not_bool.0" */ +%token SYMB45 /* "cvt_bits_uint.0" */ +%token SYMB46 /* "eq_bits.0" */ +%token SYMB47 /* "ne_bits.0" */ +%token SYMB48 /* "not_bits.0" */ +%token SYMB49 /* "cvt_bool_bv.0" */ +%token SYMB50 /* "or_bits.0" */ +%token SYMB51 /* "eor_bits.0" */ +%token SYMB52 /* "and_bits.0" */ +%token SYMB53 /* "add_bits.0" */ +%token SYMB54 /* "sub_bits.0" */ +%token SYMB55 /* "sdiv_bits.0" */ +%token SYMB56 /* "sle_bits.0" */ +%token SYMB57 /* "slt_bits.0" */ +%token SYMB58 /* "mul_bits.0" */ +%token SYMB59 /* "append_bits.0" */ +%token SYMB60 /* "lsr_bits.0" */ +%token SYMB61 /* "lsl_bits.0" */ +%token SYMB62 /* "asr_bits.0" */ +%token SYMB63 /* "replicate_bits.0" */ +%token SYMB64 /* "ZeroExtend.0" */ +%token SYMB65 /* "SignExtend.0" */ +%token SYMB66 /* "FPCompare.0" */ +%token SYMB67 /* "FPCompareEQ.0" */ +%token SYMB68 /* "FPCompareGE.0" */ +%token SYMB69 /* "FPCompareGT.0" */ +%token SYMB70 /* "FPAdd.0" */ +%token SYMB71 /* "FPSub.0" */ +%token SYMB72 /* "FPMulAdd.0" */ +%token SYMB73 /* "FPMulAddH.0" */ +%token SYMB74 /* "FPMulX.0" */ +%token SYMB75 /* "FPMul.0" */ +%token SYMB76 /* "FPDiv.0" */ +%token SYMB77 /* "FPMin.0" */ +%token SYMB78 /* "FPMinNum.0" */ +%token SYMB79 /* "FPMax.0" */ +%token SYMB80 /* "FPMaxNum.0" */ +%token SYMB81 /* "FPRecpX.0" */ +%token SYMB82 /* "FPSqrt.0" */ +%token SYMB83 /* "FPRecipEstimate.0" */ +%token SYMB84 /* "UnsignedRSqrtEstimate.0" */ +%token SYMB85 /* "FPRSqrtEstimate.0" */ +%token SYMB86 /* "BFAdd.0" */ +%token SYMB87 /* "BFMul.0" */ +%token SYMB88 /* "FPConvertBF.0" */ +%token SYMB89 /* "FPRecipStepFused.0" */ +%token SYMB90 /* "FPRSqrtStepFused.0" */ +%token SYMB91 /* "FPToFixed.0" */ +%token SYMB92 /* "FixedToFP.0" */ +%token SYMB93 /* "FPConvert.0" */ +%token SYMB94 /* "FPRoundInt.0" */ +%token SYMB95 /* "FPRoundIntN.0" */ +%token SYMB96 /* "FPToFixedJS_impl.0" */ +%token SYMB97 /* "Elem.set.0" */ +%token SYMB98 /* "Elem.read.0" */ +%token SYMB99 /* "add_vec.0" */ +%token SYMB100 /* "sub_vec.0" */ +%token SYMB101 /* "mul_vec.0" */ +%token SYMB102 /* "sdiv_vec.0" */ +%token SYMB103 /* "lsr_vec.0" */ +%token SYMB104 /* "asr_vec.0" */ +%token SYMB105 /* "lsl_vec.0" */ +%token SYMB106 /* "ite_vec.0" */ +%token SYMB107 /* "sle_vec.0" */ +%token SYMB108 /* "slt_vec.0" */ +%token SYMB109 /* "eq_vec.0" */ +%token SYMB110 /* "zcast_vec.0" */ +%token SYMB111 /* "scast_vec.0" */ +%token SYMB112 /* "trunc_vec.0" */ +%token SYMB113 /* "select_vec.0" */ +%token SYMB114 /* "shuffle_vec.0" */ +%token SYMB115 /* "reduce_add.0" */ + +%token TOK_EOF +%token TOK_Ident +%token TOK_Char +%token TOK_Double +%token TOK_Integer +%token TOK_String +%token TOK_Binary + +%start pStmtLines_list +%type pStmtLines_list + +%type stmt_list +%type string_list +%type stmtLines_list +%type stmtLines +%type stmt +%type regTypeSlices_list +%type regTypeSlices +%type typeT +%type lexpr +%type int_list +%type expr_list +%type expr +%type slice +%type varName +%type structName +%type structField +%type arrayName +%type callName +%type primName +%type vecPrimName + +%type int +%type string +%type binary + +%% + +pStmtLines_list : stmtLines_list TOK_EOF { $1 }; + +stmt_list : /* empty */ { [] } + | stmt { (fun x -> [x]) $1 } + | stmt SYMB1 stmt_list { (fun (x,xs) -> x::xs) ($1, $3) } + ; + +string_list : /* empty */ { [] } + | string { (fun x -> [x]) $1 } + | string SYMB1 string_list { (fun (x,xs) -> x::xs) ($1, $3) } + ; + +stmtLines_list : /* empty */ { [] } + | stmtLines stmtLines_list { (fun (x,xs) -> x::xs) ($1, $2) } + ; + +stmtLines : stmt { StmtLinesStmt $1 } + ; + +stmt : KW_Stmt_Assign SYMB2 lexpr SYMB3 expr SYMB4 { Stmt_Assign ($3, $5) } + | KW_Stmt_ConstDecl SYMB2 typeT SYMB3 string SYMB3 expr SYMB4 { Stmt_ConstDecl ($3, $5, $7) } + | KW_Stmt_VarDecl SYMB2 typeT SYMB3 string SYMB3 expr SYMB4 { Stmt_VarDecl ($3, $5, $7) } + | KW_Stmt_VarDeclsNoInit SYMB2 typeT SYMB3 SYMB5 string_list SYMB6 SYMB4 { Stmt_VarDeclsNoInit ($3, $6) } + | KW_Stmt_Assert SYMB2 expr SYMB4 { Stmt_Assert $3 } + | KW_Stmt_Throw SYMB2 string SYMB4 { Stmt_Throw $3 } + | KW_Stmt_TCall SYMB2 callName SYMB3 SYMB5 int_list SYMB6 SYMB3 SYMB5 expr_list SYMB6 SYMB4 { Stmt_TCall ($3, $6, $10) } + | KW_Stmt_If SYMB2 expr SYMB3 SYMB5 stmt_list SYMB6 SYMB3 SYMB5 SYMB6 SYMB3 SYMB5 stmt_list SYMB6 SYMB4 { Stmt_If ($3, $6, $13) } + ; + +regTypeSlices_list : regTypeSlices { (fun x -> [x]) $1 } + | regTypeSlices SYMB3 regTypeSlices_list { (fun (x,xs) -> x::xs) ($1, $3) } + ; + +regTypeSlices : SYMB2 SYMB5 KW_Slice_HiLo SYMB2 expr SYMB3 { Slice_HiLo $5 } + ; + +typeT : KW_Type_Bits SYMB2 int SYMB4 { Type_Bits $3 } + | KW_Type_Constructor SYMB2 SYMB7 SYMB4 { Type_Boolean } + | KW_Type_Constructor SYMB2 string SYMB4 { Type_Constructor $3 } + ; + +lexpr : KW_LExpr_Var SYMB2 varName SYMB4 { Lexpr_KnownVar $3 } + | KW_LExpr_Var SYMB2 string SYMB4 { Lexpr_LocalVar $3 } + | KW_LExpr_Field SYMB2 KW_LExpr_Var SYMB2 structName SYMB4 SYMB3 structField SYMB4 { Lexpr_Field ($5, $8) } + | KW_LExpr_Array SYMB2 KW_LExpr_Var SYMB2 arrayName SYMB4 SYMB3 int SYMB4 { Lexpr_Array ($5, $8) } + ; + +int_list : /* empty */ { [] } + | int { (fun x -> [x]) $1 } + | int SYMB1 int_list { (fun (x,xs) -> x::xs) ($1, $3) } + ; + +expr_list : /* empty */ { [] } + | expr { (fun x -> [x]) $1 } + | expr SYMB1 expr_list { (fun (x,xs) -> x::xs) ($1, $3) } + ; + +expr : KW_Expr_Var SYMB2 SYMB8 SYMB4 { Expr_True } + | KW_Expr_Var SYMB2 SYMB9 SYMB4 { Expr_False } + | KW_Expr_Var SYMB2 varName SYMB4 { Expr_KnownVar $3 } + | KW_Expr_Var SYMB2 string SYMB4 { Expr_LocalVar $3 } + | KW_Expr_TApply SYMB2 primName SYMB3 SYMB5 int_list SYMB6 SYMB3 SYMB5 expr_list SYMB6 SYMB4 { Expr_Prim ($3, $6, $10) } + | KW_Expr_TApply SYMB2 vecPrimName SYMB3 SYMB5 int_list SYMB6 SYMB3 SYMB5 expr_list SYMB6 SYMB4 { Expr_VecPrim ($3, $6, $10) } + | KW_Expr_Slices SYMB2 expr SYMB3 SYMB5 slice SYMB6 SYMB4 { Expr_Slices ($3, $6) } + | KW_Expr_Field SYMB2 KW_Expr_Var SYMB2 structName SYMB4 SYMB3 structField SYMB4 { Expr_Field ($5, $8) } + | KW_Expr_Array SYMB2 KW_Expr_Var SYMB2 arrayName SYMB4 SYMB3 int SYMB4 { Expr_Array ($5, $8) } + | int { Expr_LitInt $1 } + | binary { Expr_LitBits $1 } + | SYMB2 expr SYMB4 { $2 } + ; + +slice : KW_Slice_LoWd SYMB2 int SYMB3 int SYMB4 { Slice_LoWd ($3, $5) } + ; + +varName : SYMB10 { Var_PC } + | SYMB11 { Var_SP_EL0 } + | SYMB12 { Var_FPCR } + | SYMB13 { Var_FPSR } + | SYMB14 { Var_BTypeCompatible } + | SYMB15 { Var_BranchTaken } + | SYMB16 { Var_BTypeNext } + | SYMB17 { Var_ExclusiveLocal } + ; + +structName : SYMB18 { Struct_Pstate } + ; + +structField : SYMB19 { Field_N } + | SYMB20 { Field_Z } + | SYMB21 { Field_C } + | SYMB22 { Field_V } + | SYMB23 { Field_A } + | SYMB24 { Field_D } + | SYMB25 { Field_DIT } + | SYMB26 { Field_F } + | SYMB27 { Field_I } + | SYMB28 { Field_PAN } + | SYMB29 { Field_SP } + | SYMB30 { Field_SSBS } + | SYMB31 { Field_TCO } + | SYMB32 { Field_UAO } + | SYMB33 { Field_BTYPE } + ; + +arrayName : SYMB34 { Array_R } + | SYMB35 { Array_Z } + ; + +callName : SYMB36 { Call_Mem_set } + | SYMB37 { Call_AtomicStart } + | SYMB38 { Call_AtomicEnd } + | SYMB39 { Call_Memtag_read } + | SYMB40 { Call_Memtag_set } + ; + +primName : SYMB41 { Prim_Mem_read } + | SYMB42 { Prim_and_bool } + | SYMB43 { Prim_or_bool } + | SYMB44 { Prim_not_bool } + | SYMB45 { Prim_cvt_bits_uint } + | SYMB46 { Prim_eq_bits } + | SYMB47 { Prim_ne_bits } + | SYMB48 { Prim_not_bits } + | SYMB49 { Prim_cvt_bool_bv } + | SYMB50 { Prim_or_bits } + | SYMB51 { Prim_eor_bits } + | SYMB52 { Prim_and_bits } + | SYMB53 { Prim_add_bits } + | SYMB54 { Prim_sub_bits } + | SYMB55 { Prim_sdiv_bits } + | SYMB56 { Prim_sle_bits } + | SYMB57 { Prim_slt_bits } + | SYMB58 { Prim_mul_bits } + | SYMB59 { Prim_append_bits } + | SYMB60 { Prim_lsr_bits } + | SYMB61 { Prim_lsl_bits } + | SYMB62 { Prim_asr_bits } + | SYMB63 { Prim_replicate_bits } + | SYMB64 { Prim_ZeroExtend } + | SYMB65 { Prim_SignExtend } + | SYMB66 { Prim_FPCompare } + | SYMB67 { Prim_FPCompareEQ } + | SYMB68 { Prim_FPCompareGE } + | SYMB69 { Prim_FPCompareGT } + | SYMB70 { Prim_FPAdd } + | SYMB71 { Prim_FPSub } + | SYMB72 { Prim_FPMulAdd } + | SYMB73 { Prim_FPMulAddH } + | SYMB74 { Prim_FPMulX } + | SYMB75 { Prim_FPMul } + | SYMB76 { Prim_FPDiv } + | SYMB77 { Prim_FPMin } + | SYMB78 { Prim_FPMinNum } + | SYMB79 { Prim_FPMax } + | SYMB80 { Prim_FPMaxNum } + | SYMB81 { Prim_FPRecpX } + | SYMB82 { Prim_FPSqrt } + | SYMB83 { Prim_FPRecipEstimate } + | SYMB84 { Prim_UnsignedRSqrtEstimate } + | SYMB85 { Prim_FPRSqrtEstimate } + | SYMB86 { Prim_BFAdd } + | SYMB87 { Prim_BFMul } + | SYMB88 { Prim_FPConvertBF } + | SYMB89 { Prim_FPRecipStepFused } + | SYMB90 { Prim_FPRSqrtStepFused } + | SYMB91 { Prim_FPToFixed } + | SYMB92 { Prim_FixedToFP } + | SYMB93 { Prim_FPConvert } + | SYMB94 { Prim_FPRoundInt } + | SYMB95 { Prim_FPRoundIntN } + | SYMB96 { Prim_FPToFixedJS_impl } + ; + +vecPrimName : SYMB97 { VecPrim_Elem_set } + | SYMB98 { VecPrim_Elem_read } + | SYMB99 { VecPrim_add_vec } + | SYMB100 { VecPrim_sub_vec } + | SYMB101 { VecPrim_mul_vec } + | SYMB102 { VecPrim_sdiv_vec } + | SYMB103 { VecPrim_lsr_vec } + | SYMB104 { VecPrim_asr_vec } + | SYMB105 { VecPrim_lsl_vec } + | SYMB106 { VecPrim_ite_vec } + | SYMB107 { VecPrim_sle_vec } + | SYMB108 { VecPrim_slt_vec } + | SYMB109 { VecPrim_eq_vec } + | SYMB110 { VecPrim_zcast_vec } + | SYMB111 { VecPrim_scast_vec } + | SYMB112 { VecPrim_trunc_vec } + | SYMB113 { VecPrim_select_vec } + | SYMB114 { VecPrim_shuffle_vec } + | SYMB115 { VecPrim_reduce_add } + ; + +int : TOK_Integer { $1 }; +string : TOK_String { $1 }; +binary : TOK_Binary { Binary ($1)}; + diff --git a/libASL/bnfc/PrintSemantics.ml b/libASL/bnfc/PrintSemantics.ml new file mode 100644 index 00000000..840bea97 --- /dev/null +++ b/libASL/bnfc/PrintSemantics.ml @@ -0,0 +1,282 @@ +(* File generated by the BNF Converter (bnfc 2.9.5). *) + +(* pretty-printer *) + +open Printf + +(* We use string buffers for efficient string concatenation. + A document takes a buffer and an indentation, has side effects on the buffer + and returns a new indentation. The indentation argument indicates the level + of indentation to be used if a new line has to be started (because of what is + already in the buffer) *) +type doc = Buffer.t -> int -> int + +let rec printTree (printer : int -> 'a -> doc) (tree : 'a) : string = + let buffer_init_size = 64 (* you may want to change this *) + in let buffer = Buffer.create buffer_init_size + in + let _ = printer 0 tree buffer 0 in (* discard return value *) + Buffer.contents buffer + +let indent_width = 2 + +let spaces (i: int) : string = if i > 0 then String.make i ' ' else "" +let indent (i: int) : string = "\n" ^ spaces i + +(* To avoid dependency on package extlib, which has + Extlib.ExtChar.Char.is_whitespace, we employ the following awkward + way to check a character for whitespace. + Note: String.trim exists in the core libraries since Ocaml 4.00. *) +let isWhiteSpace (c: char) : bool = String.trim (String.make 1 c) = "" + +(* this render function is written for C-style languages, you may want to change it *) +let render (s : string) : doc = fun buf i -> + (* invariant: last char of the buffer is never whitespace *) + let n = Buffer.length buf in + let last = if n = 0 then None else Some (Buffer.nth buf (n-1)) in + let newindent = match s with + "{" -> i + indent_width + | "}" -> i - indent_width + | _ -> i in + let whitespace = match last with + None -> "" + | Some '}' -> (match s with + ";" -> "" + | _ -> indent newindent) + | (Some '{') | (Some ';') -> if s = "}" then indent newindent else indent i + | (Some '[') | (Some '(') -> "" + | Some c -> if isWhiteSpace c then "" else (match s with + ";" | "," | ")" | "]" -> "" + | "{" -> indent i + | "}" -> indent newindent + | _ -> if String.trim s = "" then "" else " ") in + Buffer.add_string buf whitespace; + Buffer.add_string buf s; + newindent + +let emptyDoc : doc = fun buf i -> i + +let concatD (ds : doc list) : doc = fun buf i -> + List.fold_left (fun accIndent elemDoc -> elemDoc buf accIndent) (emptyDoc buf i) ds + +let parenth (d:doc) : doc = concatD [render "("; d; render ")"] + +let prPrec (i:int) (j:int) (d:doc) : doc = if j (concatD []) + | (_,[x]) -> (concatD [prtInt 0 x]) + | (_,x::xs) -> (concatD [prtInt 0 x ; render ";" ; prtIntListBNFC 0 xs]) + + +let prtFloat (_:int) (f:float) : doc = render (sprintf "%.15g" f) + + + +let prtString (_:int) (s:string) : doc = render ("\"" ^ String.escaped s ^ "\"") +let rec prtStringListBNFC i es : doc = match (i, es) with + (_,[]) -> (concatD []) + | (_,[x]) -> (concatD [prtString 0 x]) + | (_,x::xs) -> (concatD [prtString 0 x ; render ";" ; prtStringListBNFC 0 xs]) + + + +let prtBinary _ (AbsSemantics.Binary i) : doc = render i + + + +let rec prtStmtLines (i:int) (e : AbsSemantics.stmtLines) : doc = match e with + AbsSemantics.StmtLinesStmt stmt -> prPrec i 0 (concatD [prtStmt 0 stmt]) + +and prtStmtLinesListBNFC i es : doc = match (i, es) with + (_,[]) -> (concatD []) + | (_,x::xs) -> (concatD [prtStmtLines 0 x ; prtStmtLinesListBNFC 0 xs]) +and prtStmt (i:int) (e : AbsSemantics.stmt) : doc = match e with + AbsSemantics.Stmt_Assign (lexpr, expr) -> prPrec i 0 (concatD [render "Stmt_Assign" ; render "(" ; prtLexpr 0 lexpr ; render "," ; prtExpr 0 expr ; render ")"]) + | AbsSemantics.Stmt_ConstDecl (type_, string, expr) -> prPrec i 0 (concatD [render "Stmt_ConstDecl" ; render "(" ; prtTypeT 0 type_ ; render "," ; prtString 0 string ; render "," ; prtExpr 0 expr ; render ")"]) + | AbsSemantics.Stmt_VarDecl (type_, string, expr) -> prPrec i 0 (concatD [render "Stmt_VarDecl" ; render "(" ; prtTypeT 0 type_ ; render "," ; prtString 0 string ; render "," ; prtExpr 0 expr ; render ")"]) + | AbsSemantics.Stmt_VarDeclsNoInit (type_, strings) -> prPrec i 0 (concatD [render "Stmt_VarDeclsNoInit" ; render "(" ; prtTypeT 0 type_ ; render "," ; render "[" ; prtStringListBNFC 0 strings ; render "]" ; render ")"]) + | AbsSemantics.Stmt_Assert expr -> prPrec i 0 (concatD [render "Stmt_Assert" ; render "(" ; prtExpr 0 expr ; render ")"]) + | AbsSemantics.Stmt_Throw string -> prPrec i 0 (concatD [render "Stmt_Throw" ; render "(" ; prtString 0 string ; render ")"]) + | AbsSemantics.Stmt_TCall (callname, integers, exprs) -> prPrec i 0 (concatD [render "Stmt_TCall" ; render "(" ; prtCallName 0 callname ; render "," ; render "[" ; prtIntListBNFC 0 integers ; render "]" ; render "," ; render "[" ; prtExprListBNFC 0 exprs ; render "]" ; render ")"]) + | AbsSemantics.Stmt_If (expr, stmts1, stmts2) -> prPrec i 0 (concatD [render "Stmt_If" ; render "(" ; prtExpr 0 expr ; render "," ; render "[" ; prtStmtListBNFC 0 stmts1 ; render "]" ; render "," ; render "[" ; render "]" ; render "," ; render "[" ; prtStmtListBNFC 0 stmts2 ; render "]" ; render ")"]) + +and prtStmtListBNFC i es : doc = match (i, es) with + (_,[]) -> (concatD []) + | (_,[x]) -> (concatD [prtStmt 0 x]) + | (_,x::xs) -> (concatD [prtStmt 0 x ; render ";" ; prtStmtListBNFC 0 xs]) +and prtRegTypeSlices (i:int) (e : AbsSemantics.regTypeSlices) : doc = match e with + AbsSemantics.Slice_HiLo expr -> prPrec i 0 (concatD [render "(" ; render "[" ; render "Slice_HiLo" ; render "(" ; prtExpr 0 expr ; render ","]) + +and prtRegTypeSlicesListBNFC i es : doc = match (i, es) with + (_,[]) -> (concatD []) + | (_,[x]) -> (concatD [prtRegTypeSlices 0 x]) + | (_,x::xs) -> (concatD [prtRegTypeSlices 0 x ; render "," ; prtRegTypeSlicesListBNFC 0 xs]) +and prtTypeT (i:int) (e : AbsSemantics.typeT) : doc = match e with + AbsSemantics.Type_Bits integer -> prPrec i 0 (concatD [render "Type_Bits" ; render "(" ; prtInt 0 integer ; render ")"]) + | AbsSemantics.Type_Boolean -> prPrec i 0 (concatD [render "Type_Constructor" ; render "(" ; render "\"boolean\"" ; render ")"]) + | AbsSemantics.Type_Constructor string -> prPrec i 0 (concatD [render "Type_Constructor" ; render "(" ; prtString 0 string ; render ")"]) + + +and prtLexpr (i:int) (e : AbsSemantics.lexpr) : doc = match e with + AbsSemantics.Lexpr_KnownVar varname -> prPrec i 0 (concatD [render "LExpr_Var" ; render "(" ; prtVarName 0 varname ; render ")"]) + | AbsSemantics.Lexpr_LocalVar string -> prPrec i 0 (concatD [render "LExpr_Var" ; render "(" ; prtString 0 string ; render ")"]) + | AbsSemantics.Lexpr_Field (structname, structfield) -> prPrec i 0 (concatD [render "LExpr_Field" ; render "(" ; render "LExpr_Var" ; render "(" ; prtStructName 0 structname ; render ")" ; render "," ; prtStructField 0 structfield ; render ")"]) + | AbsSemantics.Lexpr_Array (arrayname, integer) -> prPrec i 0 (concatD [render "LExpr_Array" ; render "(" ; render "LExpr_Var" ; render "(" ; prtArrayName 0 arrayname ; render ")" ; render "," ; prtInt 0 integer ; render ")"]) + + +and prtExpr (i:int) (e : AbsSemantics.expr) : doc = match e with + AbsSemantics.Expr_True -> prPrec i 0 (concatD [render "Expr_Var" ; render "(" ; render "\"TRUE\"" ; render ")"]) + | AbsSemantics.Expr_False -> prPrec i 0 (concatD [render "Expr_Var" ; render "(" ; render "\"FALSE\"" ; render ")"]) + | AbsSemantics.Expr_KnownVar varname -> prPrec i 0 (concatD [render "Expr_Var" ; render "(" ; prtVarName 0 varname ; render ")"]) + | AbsSemantics.Expr_LocalVar string -> prPrec i 0 (concatD [render "Expr_Var" ; render "(" ; prtString 0 string ; render ")"]) + | AbsSemantics.Expr_Prim (primname, integers, exprs) -> prPrec i 0 (concatD [render "Expr_TApply" ; render "(" ; prtPrimName 0 primname ; render "," ; render "[" ; prtIntListBNFC 0 integers ; render "]" ; render "," ; render "[" ; prtExprListBNFC 0 exprs ; render "]" ; render ")"]) + | AbsSemantics.Expr_VecPrim (vecprimname, integers, exprs) -> prPrec i 0 (concatD [render "Expr_TApply" ; render "(" ; prtVecPrimName 0 vecprimname ; render "," ; render "[" ; prtIntListBNFC 0 integers ; render "]" ; render "," ; render "[" ; prtExprListBNFC 0 exprs ; render "]" ; render ")"]) + | AbsSemantics.Expr_Slices (expr, slice) -> prPrec i 0 (concatD [render "Expr_Slices" ; render "(" ; prtExpr 0 expr ; render "," ; render "[" ; prtSlice 0 slice ; render "]" ; render ")"]) + | AbsSemantics.Expr_Field (structname, structfield) -> prPrec i 0 (concatD [render "Expr_Field" ; render "(" ; render "Expr_Var" ; render "(" ; prtStructName 0 structname ; render ")" ; render "," ; prtStructField 0 structfield ; render ")"]) + | AbsSemantics.Expr_Array (arrayname, integer) -> prPrec i 0 (concatD [render "Expr_Array" ; render "(" ; render "Expr_Var" ; render "(" ; prtArrayName 0 arrayname ; render ")" ; render "," ; prtInt 0 integer ; render ")"]) + | AbsSemantics.Expr_LitInt integer -> prPrec i 0 (concatD [prtInt 0 integer]) + | AbsSemantics.Expr_LitBits binary -> prPrec i 0 (concatD [prtBinary 0 binary]) + +and prtExprListBNFC i es : doc = match (i, es) with + (_,[]) -> (concatD []) + | (_,[x]) -> (concatD [prtExpr 0 x]) + | (_,x::xs) -> (concatD [prtExpr 0 x ; render ";" ; prtExprListBNFC 0 xs]) +and prtSlice (i:int) (e : AbsSemantics.slice) : doc = match e with + AbsSemantics.Slice_LoWd (integer1, integer2) -> prPrec i 0 (concatD [render "Slice_LoWd" ; render "(" ; prtInt 0 integer1 ; render "," ; prtInt 0 integer2 ; render ")"]) + + +and prtVarName (i:int) (e : AbsSemantics.varName) : doc = match e with + AbsSemantics.Var_PC -> prPrec i 0 (concatD [render "\"_PC\""]) + | AbsSemantics.Var_SP_EL0 -> prPrec i 0 (concatD [render "\"SP_EL0\""]) + | AbsSemantics.Var_FPCR -> prPrec i 0 (concatD [render "\"FPCR\""]) + | AbsSemantics.Var_FPSR -> prPrec i 0 (concatD [render "\"FPSR\""]) + | AbsSemantics.Var_BTypeCompatible -> prPrec i 0 (concatD [render "\"BTypeCompatible\""]) + | AbsSemantics.Var_BranchTaken -> prPrec i 0 (concatD [render "\"__BranchTaken\""]) + | AbsSemantics.Var_BTypeNext -> prPrec i 0 (concatD [render "\"BTypeNext\""]) + | AbsSemantics.Var_ExclusiveLocal -> prPrec i 0 (concatD [render "\"__ExclusiveLocal\""]) + + +and prtStructName (i:int) (e : AbsSemantics.structName) : doc = match e with + AbsSemantics.Struct_Pstate -> prPrec i 0 (concatD [render "\"PSTATE\""]) + + +and prtStructField (i:int) (e : AbsSemantics.structField) : doc = match e with + AbsSemantics.Field_N -> prPrec i 0 (concatD [render "\"N\""]) + | AbsSemantics.Field_Z -> prPrec i 0 (concatD [render "\"Z\""]) + | AbsSemantics.Field_C -> prPrec i 0 (concatD [render "\"C\""]) + | AbsSemantics.Field_V -> prPrec i 0 (concatD [render "\"V\""]) + | AbsSemantics.Field_A -> prPrec i 0 (concatD [render "\"A\""]) + | AbsSemantics.Field_D -> prPrec i 0 (concatD [render "\"D\""]) + | AbsSemantics.Field_DIT -> prPrec i 0 (concatD [render "\"DIT\""]) + | AbsSemantics.Field_F -> prPrec i 0 (concatD [render "\"F\""]) + | AbsSemantics.Field_I -> prPrec i 0 (concatD [render "\"I\""]) + | AbsSemantics.Field_PAN -> prPrec i 0 (concatD [render "\"PAN\""]) + | AbsSemantics.Field_SP -> prPrec i 0 (concatD [render "\"SP\""]) + | AbsSemantics.Field_SSBS -> prPrec i 0 (concatD [render "\"SSBS\""]) + | AbsSemantics.Field_TCO -> prPrec i 0 (concatD [render "\"TCO\""]) + | AbsSemantics.Field_UAO -> prPrec i 0 (concatD [render "\"UAO\""]) + | AbsSemantics.Field_BTYPE -> prPrec i 0 (concatD [render "\"BTYPE\""]) + + +and prtArrayName (i:int) (e : AbsSemantics.arrayName) : doc = match e with + AbsSemantics.Array_R -> prPrec i 0 (concatD [render "\"_R\""]) + | AbsSemantics.Array_Z -> prPrec i 0 (concatD [render "\"_Z\""]) + + +and prtCallName (i:int) (e : AbsSemantics.callName) : doc = match e with + AbsSemantics.Call_Mem_set -> prPrec i 0 (concatD [render "\"Mem.set.0\""]) + | AbsSemantics.Call_AtomicStart -> prPrec i 0 (concatD [render "\"AtomicStart.0\""]) + | AbsSemantics.Call_AtomicEnd -> prPrec i 0 (concatD [render "\"AtomicEnd.0\""]) + | AbsSemantics.Call_Memtag_read -> prPrec i 0 (concatD [render "\"AArch64.MemTag.read.0\""]) + | AbsSemantics.Call_Memtag_set -> prPrec i 0 (concatD [render "\"AArch64.MemTag.set.0\""]) + + +and prtPrimName (i:int) (e : AbsSemantics.primName) : doc = match e with + AbsSemantics.Prim_Mem_read -> prPrec i 0 (concatD [render "\"Mem.read.0\""]) + | AbsSemantics.Prim_and_bool -> prPrec i 0 (concatD [render "\"and_bool.0\""]) + | AbsSemantics.Prim_or_bool -> prPrec i 0 (concatD [render "\"or_bool.0\""]) + | AbsSemantics.Prim_not_bool -> prPrec i 0 (concatD [render "\"not_bool.0\""]) + | AbsSemantics.Prim_cvt_bits_uint -> prPrec i 0 (concatD [render "\"cvt_bits_uint.0\""]) + | AbsSemantics.Prim_eq_bits -> prPrec i 0 (concatD [render "\"eq_bits.0\""]) + | AbsSemantics.Prim_ne_bits -> prPrec i 0 (concatD [render "\"ne_bits.0\""]) + | AbsSemantics.Prim_not_bits -> prPrec i 0 (concatD [render "\"not_bits.0\""]) + | AbsSemantics.Prim_cvt_bool_bv -> prPrec i 0 (concatD [render "\"cvt_bool_bv.0\""]) + | AbsSemantics.Prim_or_bits -> prPrec i 0 (concatD [render "\"or_bits.0\""]) + | AbsSemantics.Prim_eor_bits -> prPrec i 0 (concatD [render "\"eor_bits.0\""]) + | AbsSemantics.Prim_and_bits -> prPrec i 0 (concatD [render "\"and_bits.0\""]) + | AbsSemantics.Prim_add_bits -> prPrec i 0 (concatD [render "\"add_bits.0\""]) + | AbsSemantics.Prim_sub_bits -> prPrec i 0 (concatD [render "\"sub_bits.0\""]) + | AbsSemantics.Prim_sdiv_bits -> prPrec i 0 (concatD [render "\"sdiv_bits.0\""]) + | AbsSemantics.Prim_sle_bits -> prPrec i 0 (concatD [render "\"sle_bits.0\""]) + | AbsSemantics.Prim_slt_bits -> prPrec i 0 (concatD [render "\"slt_bits.0\""]) + | AbsSemantics.Prim_mul_bits -> prPrec i 0 (concatD [render "\"mul_bits.0\""]) + | AbsSemantics.Prim_append_bits -> prPrec i 0 (concatD [render "\"append_bits.0\""]) + | AbsSemantics.Prim_lsr_bits -> prPrec i 0 (concatD [render "\"lsr_bits.0\""]) + | AbsSemantics.Prim_lsl_bits -> prPrec i 0 (concatD [render "\"lsl_bits.0\""]) + | AbsSemantics.Prim_asr_bits -> prPrec i 0 (concatD [render "\"asr_bits.0\""]) + | AbsSemantics.Prim_replicate_bits -> prPrec i 0 (concatD [render "\"replicate_bits.0\""]) + | AbsSemantics.Prim_ZeroExtend -> prPrec i 0 (concatD [render "\"ZeroExtend.0\""]) + | AbsSemantics.Prim_SignExtend -> prPrec i 0 (concatD [render "\"SignExtend.0\""]) + | AbsSemantics.Prim_FPCompare -> prPrec i 0 (concatD [render "\"FPCompare.0\""]) + | AbsSemantics.Prim_FPCompareEQ -> prPrec i 0 (concatD [render "\"FPCompareEQ.0\""]) + | AbsSemantics.Prim_FPCompareGE -> prPrec i 0 (concatD [render "\"FPCompareGE.0\""]) + | AbsSemantics.Prim_FPCompareGT -> prPrec i 0 (concatD [render "\"FPCompareGT.0\""]) + | AbsSemantics.Prim_FPAdd -> prPrec i 0 (concatD [render "\"FPAdd.0\""]) + | AbsSemantics.Prim_FPSub -> prPrec i 0 (concatD [render "\"FPSub.0\""]) + | AbsSemantics.Prim_FPMulAdd -> prPrec i 0 (concatD [render "\"FPMulAdd.0\""]) + | AbsSemantics.Prim_FPMulAddH -> prPrec i 0 (concatD [render "\"FPMulAddH.0\""]) + | AbsSemantics.Prim_FPMulX -> prPrec i 0 (concatD [render "\"FPMulX.0\""]) + | AbsSemantics.Prim_FPMul -> prPrec i 0 (concatD [render "\"FPMul.0\""]) + | AbsSemantics.Prim_FPDiv -> prPrec i 0 (concatD [render "\"FPDiv.0\""]) + | AbsSemantics.Prim_FPMin -> prPrec i 0 (concatD [render "\"FPMin.0\""]) + | AbsSemantics.Prim_FPMinNum -> prPrec i 0 (concatD [render "\"FPMinNum.0\""]) + | AbsSemantics.Prim_FPMax -> prPrec i 0 (concatD [render "\"FPMax.0\""]) + | AbsSemantics.Prim_FPMaxNum -> prPrec i 0 (concatD [render "\"FPMaxNum.0\""]) + | AbsSemantics.Prim_FPRecpX -> prPrec i 0 (concatD [render "\"FPRecpX.0\""]) + | AbsSemantics.Prim_FPSqrt -> prPrec i 0 (concatD [render "\"FPSqrt.0\""]) + | AbsSemantics.Prim_FPRecipEstimate -> prPrec i 0 (concatD [render "\"FPRecipEstimate.0\""]) + | AbsSemantics.Prim_UnsignedRSqrtEstimate -> prPrec i 0 (concatD [render "\"UnsignedRSqrtEstimate.0\""]) + | AbsSemantics.Prim_FPRSqrtEstimate -> prPrec i 0 (concatD [render "\"FPRSqrtEstimate.0\""]) + | AbsSemantics.Prim_BFAdd -> prPrec i 0 (concatD [render "\"BFAdd.0\""]) + | AbsSemantics.Prim_BFMul -> prPrec i 0 (concatD [render "\"BFMul.0\""]) + | AbsSemantics.Prim_FPConvertBF -> prPrec i 0 (concatD [render "\"FPConvertBF.0\""]) + | AbsSemantics.Prim_FPRecipStepFused -> prPrec i 0 (concatD [render "\"FPRecipStepFused.0\""]) + | AbsSemantics.Prim_FPRSqrtStepFused -> prPrec i 0 (concatD [render "\"FPRSqrtStepFused.0\""]) + | AbsSemantics.Prim_FPToFixed -> prPrec i 0 (concatD [render "\"FPToFixed.0\""]) + | AbsSemantics.Prim_FixedToFP -> prPrec i 0 (concatD [render "\"FixedToFP.0\""]) + | AbsSemantics.Prim_FPConvert -> prPrec i 0 (concatD [render "\"FPConvert.0\""]) + | AbsSemantics.Prim_FPRoundInt -> prPrec i 0 (concatD [render "\"FPRoundInt.0\""]) + | AbsSemantics.Prim_FPRoundIntN -> prPrec i 0 (concatD [render "\"FPRoundIntN.0\""]) + | AbsSemantics.Prim_FPToFixedJS_impl -> prPrec i 0 (concatD [render "\"FPToFixedJS_impl.0\""]) + + +and prtVecPrimName (i:int) (e : AbsSemantics.vecPrimName) : doc = match e with + AbsSemantics.VecPrim_Elem_set -> prPrec i 0 (concatD [render "\"Elem.set.0\""]) + | AbsSemantics.VecPrim_Elem_read -> prPrec i 0 (concatD [render "\"Elem.read.0\""]) + | AbsSemantics.VecPrim_add_vec -> prPrec i 0 (concatD [render "\"add_vec.0\""]) + | AbsSemantics.VecPrim_sub_vec -> prPrec i 0 (concatD [render "\"sub_vec.0\""]) + | AbsSemantics.VecPrim_mul_vec -> prPrec i 0 (concatD [render "\"mul_vec.0\""]) + | AbsSemantics.VecPrim_sdiv_vec -> prPrec i 0 (concatD [render "\"sdiv_vec.0\""]) + | AbsSemantics.VecPrim_lsr_vec -> prPrec i 0 (concatD [render "\"lsr_vec.0\""]) + | AbsSemantics.VecPrim_asr_vec -> prPrec i 0 (concatD [render "\"asr_vec.0\""]) + | AbsSemantics.VecPrim_lsl_vec -> prPrec i 0 (concatD [render "\"lsl_vec.0\""]) + | AbsSemantics.VecPrim_ite_vec -> prPrec i 0 (concatD [render "\"ite_vec.0\""]) + | AbsSemantics.VecPrim_sle_vec -> prPrec i 0 (concatD [render "\"sle_vec.0\""]) + | AbsSemantics.VecPrim_slt_vec -> prPrec i 0 (concatD [render "\"slt_vec.0\""]) + | AbsSemantics.VecPrim_eq_vec -> prPrec i 0 (concatD [render "\"eq_vec.0\""]) + | AbsSemantics.VecPrim_zcast_vec -> prPrec i 0 (concatD [render "\"zcast_vec.0\""]) + | AbsSemantics.VecPrim_scast_vec -> prPrec i 0 (concatD [render "\"scast_vec.0\""]) + | AbsSemantics.VecPrim_trunc_vec -> prPrec i 0 (concatD [render "\"trunc_vec.0\""]) + | AbsSemantics.VecPrim_select_vec -> prPrec i 0 (concatD [render "\"select_vec.0\""]) + | AbsSemantics.VecPrim_shuffle_vec -> prPrec i 0 (concatD [render "\"shuffle_vec.0\""]) + | AbsSemantics.VecPrim_reduce_add -> prPrec i 0 (concatD [render "\"reduce_add.0\""]) + + + diff --git a/libASL/bnfc/Semantics.cf b/libASL/bnfc/Semantics.cf new file mode 100644 index 00000000..6d27c511 --- /dev/null +++ b/libASL/bnfc/Semantics.cf @@ -0,0 +1,173 @@ +entrypoints [StmtLines]; + +token Binary ('\'' ["01"]+ '\''); + +separator Stmt ";"; +separator String ";"; + +separator StmtLines ""; +rules StmtLines ::= Stmt; + +Stmt_Assign.Stmt ::= "Stmt_Assign" "(" Lexpr "," Expr ")"; +Stmt_ConstDecl.Stmt ::= "Stmt_ConstDecl" "(" Type "," String "," Expr ")"; +Stmt_VarDecl.Stmt ::= "Stmt_VarDecl" "(" Type "," String "," Expr ")"; +Stmt_VarDeclsNoInit.Stmt ::= "Stmt_VarDeclsNoInit" "(" Type "," "[" [String] "]" ")"; +Stmt_Assert.Stmt ::= "Stmt_Assert" "(" Expr ")"; +Stmt_Throw.Stmt ::= "Stmt_Throw" "(" String ")"; +Stmt_TCall.Stmt ::= "Stmt_TCall" "(" CallName "," "[" [Integer] "]" "," "[" [Expr] "]" ")"; +Stmt_If.Stmt ::= "Stmt_If" "(" Expr "," "[" [Stmt] "]" "," "[" "]" "," "[" [Stmt] "]" ")"; + +separator nonempty RegTypeSlices ","; + +-- is this needed? +-- Slice_HiLo.RegTypeSlices ::= "(" "[" "Slice_HiLo" "(" Expr ","; + +Type_Bits.Type ::= "Type_Bits" "(" Integer ")"; +Type_Boolean.Type ::= "Type_Constructor" "(" "\"boolean\"" ")"; +--Type_Constructor.Type ::= "Type_Constructor" "(" String ")"; +--Type_Register.Type ::= "Type_Register" "(" String RegSlice ")"; + +Lexpr_KnownVar.Lexpr ::= "LExpr_Var" "(" VarName ")"; +Lexpr_LocalVar.Lexpr ::= "LExpr_Var" "(" String ")"; +Lexpr_Field.Lexpr ::= "LExpr_Field" "(" "LExpr_Var" "(" StructName ")" "," StructField ")"; +Lexpr_Array.Lexpr ::= "LExpr_Array" "(" "LExpr_Var" "(" ArrayName ")" "," Integer ")"; + +separator Integer ";"; +separator Expr ";"; + +Expr_True.Expr ::= "Expr_Var" "(" "\"TRUE\"" ")"; +Expr_False.Expr ::= "Expr_Var" "(" "\"FALSE\"" ")"; +Expr_KnownVar.Expr ::= "Expr_Var" "(" VarName ")"; +Expr_LocalVar.Expr ::= "Expr_Var" "(" String ")"; +Expr_Prim.Expr ::= "Expr_TApply" "(" PrimName "," "[" [Integer] "]" "," "[" [Expr] "]" ")"; +Expr_VecPrim.Expr ::= "Expr_TApply" "(" VecPrimName "," "[" [Integer] "]" "," "[" [Expr] "]" ")"; +Expr_Slices.Expr ::= "Expr_Slices" "(" Expr "," "[" Slice "]" ")"; +Expr_Field.Expr ::= "Expr_Field" "(" "Expr_Var" "(" StructName ")" "," StructField ")"; +Expr_Array.Expr ::= "Expr_Array" "(" "Expr_Var" "(" ArrayName ")" "," Integer ")"; +Expr_LitInt.Expr ::= Integer; +Expr_LitBits.Expr ::= Binary; +_.Expr ::= "(" Expr ")"; + +Slice_LoWd.Slice ::= "Slice_LoWd" "(" Integer "," Integer ")"; + +{- +RegSlice_HiLo.RegSlice ::= "," "(" "Slice_HiLo" "(" Integer "," Integer ")"; +separator RegSlice ""; +-} + +-- largely taken from template_offline_utils.ml + +Var_PC.VarName ::= "\"_PC\""; +Var_SP_EL0.VarName ::= "\"SP_EL0\""; +Var_FPCR.VarName ::= "\"FPCR\""; +Var_FPSR.VarName ::= "\"FPSR\""; +Var_BTypeCompatible.VarName ::= "\"BTypeCompatible\""; +Var_BranchTaken.VarName ::= "\"__BranchTaken\""; +Var_BTypeNext.VarName ::= "\"BTypeNext\""; +Var_ExclusiveLocal.VarName ::= "\"__ExclusiveLocal\""; + +Struct_Pstate.StructName ::= "\"PSTATE\""; + +Field_N.StructField ::= "\"N\""; +Field_Z.StructField ::= "\"Z\""; +Field_C.StructField ::= "\"C\""; +Field_V.StructField ::= "\"V\""; + +Field_A.StructField ::= "\"A\""; +Field_D.StructField ::= "\"D\""; +Field_DIT.StructField ::= "\"DIT\""; +Field_F.StructField ::= "\"F\""; +Field_I.StructField ::= "\"I\""; +Field_PAN.StructField ::= "\"PAN\""; +Field_SP.StructField ::= "\"SP\""; +Field_SSBS.StructField ::= "\"SSBS\""; +Field_TCO.StructField ::= "\"TCO\""; +Field_UAO.StructField ::= "\"UAO\""; +Field_BTYPE.StructField ::= "\"BTYPE\""; + +Array_R.ArrayName ::= "\"_R\""; +Array_Z.ArrayName ::= "\"_Z\""; + +Call_Mem_set.CallName ::= "\"Mem.set.0\""; +Call_AtomicStart.CallName ::= "\"AtomicStart.0\""; +Call_AtomicEnd.CallName ::= "\"AtomicEnd.0\""; +Call_Memtag_read.CallName ::= "\"AArch64.MemTag.read.0\""; +Call_Memtag_set.CallName ::= "\"AArch64.MemTag.set.0\""; + +Prim_Mem_read.PrimName ::= "\"Mem.read.0\""; +Prim_and_bool.PrimName ::= "\"and_bool.0\""; +Prim_or_bool.PrimName ::= "\"or_bool.0\""; +Prim_not_bool.PrimName ::= "\"not_bool.0\""; +Prim_cvt_bits_uint.PrimName ::= "\"cvt_bits_uint.0\""; +Prim_eq_bits.PrimName ::= "\"eq_bits.0\""; +Prim_ne_bits.PrimName ::= "\"ne_bits.0\""; +Prim_not_bits.PrimName ::= "\"not_bits.0\""; +Prim_cvt_bool_bv.PrimName ::= "\"cvt_bool_bv.0\""; +Prim_or_bits.PrimName ::= "\"or_bits.0\""; +Prim_eor_bits.PrimName ::= "\"eor_bits.0\""; +Prim_and_bits.PrimName ::= "\"and_bits.0\""; +Prim_add_bits.PrimName ::= "\"add_bits.0\""; +Prim_sub_bits.PrimName ::= "\"sub_bits.0\""; +Prim_sdiv_bits.PrimName ::= "\"sdiv_bits.0\""; +Prim_sle_bits.PrimName ::= "\"sle_bits.0\""; +Prim_slt_bits.PrimName ::= "\"slt_bits.0\""; +Prim_mul_bits.PrimName ::= "\"mul_bits.0\""; +Prim_append_bits.PrimName ::= "\"append_bits.0\""; +Prim_lsr_bits.PrimName ::= "\"lsr_bits.0\""; +Prim_lsl_bits.PrimName ::= "\"lsl_bits.0\""; +Prim_asr_bits.PrimName ::= "\"asr_bits.0\""; +Prim_replicate_bits.PrimName ::= "\"replicate_bits.0\""; +Prim_ZeroExtend.PrimName ::= "\"ZeroExtend.0\""; +Prim_SignExtend.PrimName ::= "\"SignExtend.0\""; +Prim_FPCompare.PrimName ::= "\"FPCompare.0\""; +Prim_FPCompareEQ.PrimName ::= "\"FPCompareEQ.0\""; +Prim_FPCompareGE.PrimName ::= "\"FPCompareGE.0\""; +Prim_FPCompareGT.PrimName ::= "\"FPCompareGT.0\""; +Prim_FPAdd.PrimName ::= "\"FPAdd.0\""; +Prim_FPSub.PrimName ::= "\"FPSub.0\""; +Prim_FPMulAdd.PrimName ::= "\"FPMulAdd.0\""; +Prim_FPMulAddH.PrimName ::= "\"FPMulAddH.0\""; +Prim_FPMulX.PrimName ::= "\"FPMulX.0\""; +Prim_FPMul.PrimName ::= "\"FPMul.0\""; +Prim_FPDiv.PrimName ::= "\"FPDiv.0\""; +Prim_FPMin.PrimName ::= "\"FPMin.0\""; +Prim_FPMinNum.PrimName ::= "\"FPMinNum.0\""; +Prim_FPMax.PrimName ::= "\"FPMax.0\""; +Prim_FPMaxNum.PrimName ::= "\"FPMaxNum.0\""; +Prim_FPRecpX.PrimName ::= "\"FPRecpX.0\""; +Prim_FPSqrt.PrimName ::= "\"FPSqrt.0\""; +Prim_FPRecipEstimate.PrimName ::= "\"FPRecipEstimate.0\""; +Prim_UnsignedRSqrtEstimate.PrimName ::= "\"UnsignedRSqrtEstimate.0\""; +Prim_FPRSqrtEstimate.PrimName ::= "\"FPRSqrtEstimate.0\""; +Prim_BFAdd.PrimName ::= "\"BFAdd.0\""; +Prim_BFMul.PrimName ::= "\"BFMul.0\""; +Prim_FPConvertBF.PrimName ::= "\"FPConvertBF.0\""; +Prim_FPRecipStepFused.PrimName ::= "\"FPRecipStepFused.0\""; +Prim_FPRSqrtStepFused.PrimName ::= "\"FPRSqrtStepFused.0\""; +Prim_FPToFixed.PrimName ::= "\"FPToFixed.0\""; +Prim_FixedToFP.PrimName ::= "\"FixedToFP.0\""; +Prim_FPConvert.PrimName ::= "\"FPConvert.0\""; +Prim_FPRoundInt.PrimName ::= "\"FPRoundInt.0\""; +Prim_FPRoundIntN.PrimName ::= "\"FPRoundIntN.0\""; +Prim_FPToFixedJS_impl.PrimName ::= "\"FPToFixedJS_impl.0\""; + +VecPrim_Elem_set.VecPrimName ::= "\"Elem.set.0\""; +VecPrim_Elem_read.VecPrimName ::= "\"Elem.read.0\""; +VecPrim_add_vec.VecPrimName ::= "\"add_vec.0\""; +VecPrim_sub_vec.VecPrimName ::= "\"sub_vec.0\""; +VecPrim_mul_vec.VecPrimName ::= "\"mul_vec.0\""; +VecPrim_sdiv_vec.VecPrimName ::= "\"sdiv_vec.0\""; +VecPrim_lsr_vec.VecPrimName ::= "\"lsr_vec.0\""; +VecPrim_asr_vec.VecPrimName ::= "\"asr_vec.0\""; +VecPrim_lsl_vec.VecPrimName ::= "\"lsl_vec.0\""; +VecPrim_ite_vec.VecPrimName ::= "\"ite_vec.0\""; +VecPrim_sle_vec.VecPrimName ::= "\"sle_vec.0\""; +VecPrim_slt_vec.VecPrimName ::= "\"slt_vec.0\""; +VecPrim_eq_vec.VecPrimName ::= "\"eq_vec.0\""; +VecPrim_zcast_vec.VecPrimName ::= "\"zcast_vec.0\""; +VecPrim_scast_vec.VecPrimName ::= "\"scast_vec.0\""; +VecPrim_trunc_vec.VecPrimName ::= "\"trunc_vec.0\""; +VecPrim_select_vec.VecPrimName ::= "\"select_vec.0\""; +VecPrim_shuffle_vec.VecPrimName ::= "\"shuffle_vec.0\""; +VecPrim_reduce_add.VecPrimName ::= "\"reduce_add.0\""; + diff --git a/libASL/bnfc/ShowSemantics.ml b/libASL/bnfc/ShowSemantics.ml new file mode 100644 index 00000000..b1de6b7d --- /dev/null +++ b/libASL/bnfc/ShowSemantics.ml @@ -0,0 +1,220 @@ +(* File generated by the BNF Converter (bnfc 2.9.5). *) + +(* show functions *) + +(* use string buffers for efficient string concatenations *) +type showable = Buffer.t -> unit + +let show (s : showable) : string = + let init_size = 16 in (* you may want to adjust this *) + let b = Buffer.create init_size in + s b; + Buffer.contents b + +let emptyS : showable = fun buf -> () + +let c2s (c:char) : showable = fun buf -> Buffer.add_char buf c +let s2s (s:string) : showable = fun buf -> Buffer.add_string buf s + +let ( >> ) (s1 : showable) (s2 : showable) : showable = fun buf -> s1 buf; s2 buf + +let showChar (c:char) : showable = fun buf -> + Buffer.add_string buf ("'" ^ Char.escaped c ^ "'") + +let showString (s:string) : showable = fun buf -> + Buffer.add_string buf ("\"" ^ String.escaped s ^ "\"") + +let showList (showFun : 'a -> showable) (xs : 'a list) : showable = fun buf -> + let rec f ys = match ys with + [] -> () + | [y] -> showFun y buf + | y::ys -> showFun y buf; Buffer.add_string buf "; "; f ys + in + Buffer.add_char buf '['; + f xs; + Buffer.add_char buf ']' + + +let showInt (i:int) : showable = s2s (string_of_int i) +let showFloat (f:float) : showable = s2s (string_of_float f) + +let rec showBinary (AbsSemantics.Binary i) : showable = s2s "Binary " >> showString i + +let rec showStmtLines (e : AbsSemantics.stmtLines) : showable = match e with + AbsSemantics.StmtLinesStmt stmt -> s2s "StmtLinesStmt" >> c2s ' ' >> c2s '(' >> showStmt stmt >> c2s ')' + + +and showStmt (e : AbsSemantics.stmt) : showable = match e with + AbsSemantics.Stmt_Assign (lexpr, expr) -> s2s "Stmt_Assign" >> c2s ' ' >> c2s '(' >> showLexpr lexpr >> s2s ", " >> showExpr expr >> c2s ')' + | AbsSemantics.Stmt_ConstDecl (type', string, expr) -> s2s "Stmt_ConstDecl" >> c2s ' ' >> c2s '(' >> showTypeT type' >> s2s ", " >> showString string >> s2s ", " >> showExpr expr >> c2s ')' + | AbsSemantics.Stmt_VarDecl (type', string, expr) -> s2s "Stmt_VarDecl" >> c2s ' ' >> c2s '(' >> showTypeT type' >> s2s ", " >> showString string >> s2s ", " >> showExpr expr >> c2s ')' + | AbsSemantics.Stmt_VarDeclsNoInit (type', strings) -> s2s "Stmt_VarDeclsNoInit" >> c2s ' ' >> c2s '(' >> showTypeT type' >> s2s ", " >> showList showString strings >> c2s ')' + | AbsSemantics.Stmt_Assert expr -> s2s "Stmt_Assert" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')' + | AbsSemantics.Stmt_Throw string -> s2s "Stmt_Throw" >> c2s ' ' >> c2s '(' >> showString string >> c2s ')' + | AbsSemantics.Stmt_TCall (callname, integers, exprs) -> s2s "Stmt_TCall" >> c2s ' ' >> c2s '(' >> showCallName callname >> s2s ", " >> showList showInt integers >> s2s ", " >> showList showExpr exprs >> c2s ')' + | AbsSemantics.Stmt_If (expr, stmts0, stmts) -> s2s "Stmt_If" >> c2s ' ' >> c2s '(' >> showExpr expr >> s2s ", " >> showList showStmt stmts0 >> s2s ", " >> showList showStmt stmts >> c2s ')' + + +and showRegTypeSlices (e : AbsSemantics.regTypeSlices) : showable = match e with + AbsSemantics.Slice_HiLo expr -> s2s "Slice_HiLo" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')' + + +and showTypeT (e : AbsSemantics.typeT) : showable = match e with + AbsSemantics.Type_Bits integer -> s2s "Type_Bits" >> c2s ' ' >> c2s '(' >> showInt integer >> c2s ')' + | AbsSemantics.Type_Boolean -> s2s "Type_Boolean" + | AbsSemantics.Type_Constructor string -> s2s "Type_Constructor" >> c2s ' ' >> c2s '(' >> showString string >> c2s ')' + + +and showLexpr (e : AbsSemantics.lexpr) : showable = match e with + AbsSemantics.Lexpr_KnownVar varname -> s2s "Lexpr_KnownVar" >> c2s ' ' >> c2s '(' >> showVarName varname >> c2s ')' + | AbsSemantics.Lexpr_LocalVar string -> s2s "Lexpr_LocalVar" >> c2s ' ' >> c2s '(' >> showString string >> c2s ')' + | AbsSemantics.Lexpr_Field (structname, structfield) -> s2s "Lexpr_Field" >> c2s ' ' >> c2s '(' >> showStructName structname >> s2s ", " >> showStructField structfield >> c2s ')' + | AbsSemantics.Lexpr_Array (arrayname, integer) -> s2s "Lexpr_Array" >> c2s ' ' >> c2s '(' >> showArrayName arrayname >> s2s ", " >> showInt integer >> c2s ')' + + +and showExpr (e : AbsSemantics.expr) : showable = match e with + AbsSemantics.Expr_True -> s2s "Expr_True" + | AbsSemantics.Expr_False -> s2s "Expr_False" + | AbsSemantics.Expr_KnownVar varname -> s2s "Expr_KnownVar" >> c2s ' ' >> c2s '(' >> showVarName varname >> c2s ')' + | AbsSemantics.Expr_LocalVar string -> s2s "Expr_LocalVar" >> c2s ' ' >> c2s '(' >> showString string >> c2s ')' + | AbsSemantics.Expr_Prim (primname, integers, exprs) -> s2s "Expr_Prim" >> c2s ' ' >> c2s '(' >> showPrimName primname >> s2s ", " >> showList showInt integers >> s2s ", " >> showList showExpr exprs >> c2s ')' + | AbsSemantics.Expr_VecPrim (vecprimname, integers, exprs) -> s2s "Expr_VecPrim" >> c2s ' ' >> c2s '(' >> showVecPrimName vecprimname >> s2s ", " >> showList showInt integers >> s2s ", " >> showList showExpr exprs >> c2s ')' + | AbsSemantics.Expr_Slices (expr, slice) -> s2s "Expr_Slices" >> c2s ' ' >> c2s '(' >> showExpr expr >> s2s ", " >> showSlice slice >> c2s ')' + | AbsSemantics.Expr_Field (structname, structfield) -> s2s "Expr_Field" >> c2s ' ' >> c2s '(' >> showStructName structname >> s2s ", " >> showStructField structfield >> c2s ')' + | AbsSemantics.Expr_Array (arrayname, integer) -> s2s "Expr_Array" >> c2s ' ' >> c2s '(' >> showArrayName arrayname >> s2s ", " >> showInt integer >> c2s ')' + | AbsSemantics.Expr_LitInt integer -> s2s "Expr_LitInt" >> c2s ' ' >> c2s '(' >> showInt integer >> c2s ')' + | AbsSemantics.Expr_LitBits binary -> s2s "Expr_LitBits" >> c2s ' ' >> c2s '(' >> showBinary binary >> c2s ')' + + +and showSlice (e : AbsSemantics.slice) : showable = match e with + AbsSemantics.Slice_LoWd (integer0, integer) -> s2s "Slice_LoWd" >> c2s ' ' >> c2s '(' >> showInt integer0 >> s2s ", " >> showInt integer >> c2s ')' + + +and showVarName (e : AbsSemantics.varName) : showable = match e with + AbsSemantics.Var_PC -> s2s "Var_PC" + | AbsSemantics.Var_SP_EL0 -> s2s "Var_SP_EL0" + | AbsSemantics.Var_FPCR -> s2s "Var_FPCR" + | AbsSemantics.Var_FPSR -> s2s "Var_FPSR" + | AbsSemantics.Var_BTypeCompatible -> s2s "Var_BTypeCompatible" + | AbsSemantics.Var_BranchTaken -> s2s "Var_BranchTaken" + | AbsSemantics.Var_BTypeNext -> s2s "Var_BTypeNext" + | AbsSemantics.Var_ExclusiveLocal -> s2s "Var_ExclusiveLocal" + + +and showStructName (e : AbsSemantics.structName) : showable = match e with + AbsSemantics.Struct_Pstate -> s2s "Struct_Pstate" + + +and showStructField (e : AbsSemantics.structField) : showable = match e with + AbsSemantics.Field_N -> s2s "Field_N" + | AbsSemantics.Field_Z -> s2s "Field_Z" + | AbsSemantics.Field_C -> s2s "Field_C" + | AbsSemantics.Field_V -> s2s "Field_V" + | AbsSemantics.Field_A -> s2s "Field_A" + | AbsSemantics.Field_D -> s2s "Field_D" + | AbsSemantics.Field_DIT -> s2s "Field_DIT" + | AbsSemantics.Field_F -> s2s "Field_F" + | AbsSemantics.Field_I -> s2s "Field_I" + | AbsSemantics.Field_PAN -> s2s "Field_PAN" + | AbsSemantics.Field_SP -> s2s "Field_SP" + | AbsSemantics.Field_SSBS -> s2s "Field_SSBS" + | AbsSemantics.Field_TCO -> s2s "Field_TCO" + | AbsSemantics.Field_UAO -> s2s "Field_UAO" + | AbsSemantics.Field_BTYPE -> s2s "Field_BTYPE" + + +and showArrayName (e : AbsSemantics.arrayName) : showable = match e with + AbsSemantics.Array_R -> s2s "Array_R" + | AbsSemantics.Array_Z -> s2s "Array_Z" + + +and showCallName (e : AbsSemantics.callName) : showable = match e with + AbsSemantics.Call_Mem_set -> s2s "Call_Mem_set" + | AbsSemantics.Call_AtomicStart -> s2s "Call_AtomicStart" + | AbsSemantics.Call_AtomicEnd -> s2s "Call_AtomicEnd" + | AbsSemantics.Call_Memtag_read -> s2s "Call_Memtag_read" + | AbsSemantics.Call_Memtag_set -> s2s "Call_Memtag_set" + + +and showPrimName (e : AbsSemantics.primName) : showable = match e with + AbsSemantics.Prim_Mem_read -> s2s "Prim_Mem_read" + | AbsSemantics.Prim_and_bool -> s2s "Prim_and_bool" + | AbsSemantics.Prim_or_bool -> s2s "Prim_or_bool" + | AbsSemantics.Prim_not_bool -> s2s "Prim_not_bool" + | AbsSemantics.Prim_cvt_bits_uint -> s2s "Prim_cvt_bits_uint" + | AbsSemantics.Prim_eq_bits -> s2s "Prim_eq_bits" + | AbsSemantics.Prim_ne_bits -> s2s "Prim_ne_bits" + | AbsSemantics.Prim_not_bits -> s2s "Prim_not_bits" + | AbsSemantics.Prim_cvt_bool_bv -> s2s "Prim_cvt_bool_bv" + | AbsSemantics.Prim_or_bits -> s2s "Prim_or_bits" + | AbsSemantics.Prim_eor_bits -> s2s "Prim_eor_bits" + | AbsSemantics.Prim_and_bits -> s2s "Prim_and_bits" + | AbsSemantics.Prim_add_bits -> s2s "Prim_add_bits" + | AbsSemantics.Prim_sub_bits -> s2s "Prim_sub_bits" + | AbsSemantics.Prim_sdiv_bits -> s2s "Prim_sdiv_bits" + | AbsSemantics.Prim_sle_bits -> s2s "Prim_sle_bits" + | AbsSemantics.Prim_slt_bits -> s2s "Prim_slt_bits" + | AbsSemantics.Prim_mul_bits -> s2s "Prim_mul_bits" + | AbsSemantics.Prim_append_bits -> s2s "Prim_append_bits" + | AbsSemantics.Prim_lsr_bits -> s2s "Prim_lsr_bits" + | AbsSemantics.Prim_lsl_bits -> s2s "Prim_lsl_bits" + | AbsSemantics.Prim_asr_bits -> s2s "Prim_asr_bits" + | AbsSemantics.Prim_replicate_bits -> s2s "Prim_replicate_bits" + | AbsSemantics.Prim_ZeroExtend -> s2s "Prim_ZeroExtend" + | AbsSemantics.Prim_SignExtend -> s2s "Prim_SignExtend" + | AbsSemantics.Prim_FPCompare -> s2s "Prim_FPCompare" + | AbsSemantics.Prim_FPCompareEQ -> s2s "Prim_FPCompareEQ" + | AbsSemantics.Prim_FPCompareGE -> s2s "Prim_FPCompareGE" + | AbsSemantics.Prim_FPCompareGT -> s2s "Prim_FPCompareGT" + | AbsSemantics.Prim_FPAdd -> s2s "Prim_FPAdd" + | AbsSemantics.Prim_FPSub -> s2s "Prim_FPSub" + | AbsSemantics.Prim_FPMulAdd -> s2s "Prim_FPMulAdd" + | AbsSemantics.Prim_FPMulAddH -> s2s "Prim_FPMulAddH" + | AbsSemantics.Prim_FPMulX -> s2s "Prim_FPMulX" + | AbsSemantics.Prim_FPMul -> s2s "Prim_FPMul" + | AbsSemantics.Prim_FPDiv -> s2s "Prim_FPDiv" + | AbsSemantics.Prim_FPMin -> s2s "Prim_FPMin" + | AbsSemantics.Prim_FPMinNum -> s2s "Prim_FPMinNum" + | AbsSemantics.Prim_FPMax -> s2s "Prim_FPMax" + | AbsSemantics.Prim_FPMaxNum -> s2s "Prim_FPMaxNum" + | AbsSemantics.Prim_FPRecpX -> s2s "Prim_FPRecpX" + | AbsSemantics.Prim_FPSqrt -> s2s "Prim_FPSqrt" + | AbsSemantics.Prim_FPRecipEstimate -> s2s "Prim_FPRecipEstimate" + | AbsSemantics.Prim_UnsignedRSqrtEstimate -> s2s "Prim_UnsignedRSqrtEstimate" + | AbsSemantics.Prim_FPRSqrtEstimate -> s2s "Prim_FPRSqrtEstimate" + | AbsSemantics.Prim_BFAdd -> s2s "Prim_BFAdd" + | AbsSemantics.Prim_BFMul -> s2s "Prim_BFMul" + | AbsSemantics.Prim_FPConvertBF -> s2s "Prim_FPConvertBF" + | AbsSemantics.Prim_FPRecipStepFused -> s2s "Prim_FPRecipStepFused" + | AbsSemantics.Prim_FPRSqrtStepFused -> s2s "Prim_FPRSqrtStepFused" + | AbsSemantics.Prim_FPToFixed -> s2s "Prim_FPToFixed" + | AbsSemantics.Prim_FixedToFP -> s2s "Prim_FixedToFP" + | AbsSemantics.Prim_FPConvert -> s2s "Prim_FPConvert" + | AbsSemantics.Prim_FPRoundInt -> s2s "Prim_FPRoundInt" + | AbsSemantics.Prim_FPRoundIntN -> s2s "Prim_FPRoundIntN" + | AbsSemantics.Prim_FPToFixedJS_impl -> s2s "Prim_FPToFixedJS_impl" + + +and showVecPrimName (e : AbsSemantics.vecPrimName) : showable = match e with + AbsSemantics.VecPrim_Elem_set -> s2s "VecPrim_Elem_set" + | AbsSemantics.VecPrim_Elem_read -> s2s "VecPrim_Elem_read" + | AbsSemantics.VecPrim_add_vec -> s2s "VecPrim_add_vec" + | AbsSemantics.VecPrim_sub_vec -> s2s "VecPrim_sub_vec" + | AbsSemantics.VecPrim_mul_vec -> s2s "VecPrim_mul_vec" + | AbsSemantics.VecPrim_sdiv_vec -> s2s "VecPrim_sdiv_vec" + | AbsSemantics.VecPrim_lsr_vec -> s2s "VecPrim_lsr_vec" + | AbsSemantics.VecPrim_asr_vec -> s2s "VecPrim_asr_vec" + | AbsSemantics.VecPrim_lsl_vec -> s2s "VecPrim_lsl_vec" + | AbsSemantics.VecPrim_ite_vec -> s2s "VecPrim_ite_vec" + | AbsSemantics.VecPrim_sle_vec -> s2s "VecPrim_sle_vec" + | AbsSemantics.VecPrim_slt_vec -> s2s "VecPrim_slt_vec" + | AbsSemantics.VecPrim_eq_vec -> s2s "VecPrim_eq_vec" + | AbsSemantics.VecPrim_zcast_vec -> s2s "VecPrim_zcast_vec" + | AbsSemantics.VecPrim_scast_vec -> s2s "VecPrim_scast_vec" + | AbsSemantics.VecPrim_trunc_vec -> s2s "VecPrim_trunc_vec" + | AbsSemantics.VecPrim_select_vec -> s2s "VecPrim_select_vec" + | AbsSemantics.VecPrim_shuffle_vec -> s2s "VecPrim_shuffle_vec" + | AbsSemantics.VecPrim_reduce_add -> s2s "VecPrim_reduce_add" + + + diff --git a/libASL/bnfc/SkelSemantics.ml b/libASL/bnfc/SkelSemantics.ml new file mode 100644 index 00000000..d20e2fd1 --- /dev/null +++ b/libASL/bnfc/SkelSemantics.ml @@ -0,0 +1,193 @@ +(* File generated by the BNF Converter (bnfc 2.9.5). *) + +module SkelSemantics = struct + +open AbsSemantics + +type result = string + +let failure x = failwith "Undefined case." (* x discarded *) + +let rec transBinary (x : binary) : result = match x with + Binary string -> failure x + + +and transStmtLines (x : stmtLines) : result = match x with + StmtLinesStmt stmt -> failure x + + +and transStmt (x : stmt) : result = match x with + Stmt_Assign (lexpr, expr) -> failure x + | Stmt_ConstDecl (type', string, expr) -> failure x + | Stmt_VarDecl (type', string, expr) -> failure x + | Stmt_VarDeclsNoInit (type', strings) -> failure x + | Stmt_Assert expr -> failure x + | Stmt_Throw string -> failure x + | Stmt_TCall (callname, integers, exprs) -> failure x + | Stmt_If (expr, stmts0, stmts) -> failure x + + +and transRegTypeSlices (x : regTypeSlices) : result = match x with + Slice_HiLo expr -> failure x + + +and transType (x : typeT) : result = match x with + Type_Bits integer -> failure x + | Type_Boolean -> failure x + | Type_Constructor string -> failure x + + +and transLexpr (x : lexpr) : result = match x with + Lexpr_KnownVar varname -> failure x + | Lexpr_LocalVar string -> failure x + | Lexpr_Field (structname, structfield) -> failure x + | Lexpr_Array (arrayname, integer) -> failure x + + +and transExpr (x : expr) : result = match x with + Expr_True -> failure x + | Expr_False -> failure x + | Expr_KnownVar varname -> failure x + | Expr_LocalVar string -> failure x + | Expr_Prim (primname, integers, exprs) -> failure x + | Expr_VecPrim (vecprimname, integers, exprs) -> failure x + | Expr_Slices (expr, slice) -> failure x + | Expr_Field (structname, structfield) -> failure x + | Expr_Array (arrayname, integer) -> failure x + | Expr_LitInt integer -> failure x + | Expr_LitBits binary -> failure x + + +and transSlice (x : slice) : result = match x with + Slice_LoWd (integer0, integer) -> failure x + + +and transVarName (x : varName) : result = match x with + Var_PC -> failure x + | Var_SP_EL0 -> failure x + | Var_FPCR -> failure x + | Var_FPSR -> failure x + | Var_BTypeCompatible -> failure x + | Var_BranchTaken -> failure x + | Var_BTypeNext -> failure x + | Var_ExclusiveLocal -> failure x + + +and transStructName (x : structName) : result = match x with + Struct_Pstate -> failure x + + +and transStructField (x : structField) : result = match x with + Field_N -> failure x + | Field_Z -> failure x + | Field_C -> failure x + | Field_V -> failure x + | Field_A -> failure x + | Field_D -> failure x + | Field_DIT -> failure x + | Field_F -> failure x + | Field_I -> failure x + | Field_PAN -> failure x + | Field_SP -> failure x + | Field_SSBS -> failure x + | Field_TCO -> failure x + | Field_UAO -> failure x + | Field_BTYPE -> failure x + + +and transArrayName (x : arrayName) : result = match x with + Array_R -> failure x + | Array_Z -> failure x + + +and transCallName (x : callName) : result = match x with + Call_Mem_set -> failure x + | Call_AtomicStart -> failure x + | Call_AtomicEnd -> failure x + | Call_Memtag_read -> failure x + | Call_Memtag_set -> failure x + + +and transPrimName (x : primName) : result = match x with + Prim_Mem_read -> failure x + | Prim_and_bool -> failure x + | Prim_or_bool -> failure x + | Prim_not_bool -> failure x + | Prim_cvt_bits_uint -> failure x + | Prim_eq_bits -> failure x + | Prim_ne_bits -> failure x + | Prim_not_bits -> failure x + | Prim_cvt_bool_bv -> failure x + | Prim_or_bits -> failure x + | Prim_eor_bits -> failure x + | Prim_and_bits -> failure x + | Prim_add_bits -> failure x + | Prim_sub_bits -> failure x + | Prim_sdiv_bits -> failure x + | Prim_sle_bits -> failure x + | Prim_slt_bits -> failure x + | Prim_mul_bits -> failure x + | Prim_append_bits -> failure x + | Prim_lsr_bits -> failure x + | Prim_lsl_bits -> failure x + | Prim_asr_bits -> failure x + | Prim_replicate_bits -> failure x + | Prim_ZeroExtend -> failure x + | Prim_SignExtend -> failure x + | Prim_FPCompare -> failure x + | Prim_FPCompareEQ -> failure x + | Prim_FPCompareGE -> failure x + | Prim_FPCompareGT -> failure x + | Prim_FPAdd -> failure x + | Prim_FPSub -> failure x + | Prim_FPMulAdd -> failure x + | Prim_FPMulAddH -> failure x + | Prim_FPMulX -> failure x + | Prim_FPMul -> failure x + | Prim_FPDiv -> failure x + | Prim_FPMin -> failure x + | Prim_FPMinNum -> failure x + | Prim_FPMax -> failure x + | Prim_FPMaxNum -> failure x + | Prim_FPRecpX -> failure x + | Prim_FPSqrt -> failure x + | Prim_FPRecipEstimate -> failure x + | Prim_UnsignedRSqrtEstimate -> failure x + | Prim_FPRSqrtEstimate -> failure x + | Prim_BFAdd -> failure x + | Prim_BFMul -> failure x + | Prim_FPConvertBF -> failure x + | Prim_FPRecipStepFused -> failure x + | Prim_FPRSqrtStepFused -> failure x + | Prim_FPToFixed -> failure x + | Prim_FixedToFP -> failure x + | Prim_FPConvert -> failure x + | Prim_FPRoundInt -> failure x + | Prim_FPRoundIntN -> failure x + | Prim_FPToFixedJS_impl -> failure x + + +and transVecPrimName (x : vecPrimName) : result = match x with + VecPrim_Elem_set -> failure x + | VecPrim_Elem_read -> failure x + | VecPrim_add_vec -> failure x + | VecPrim_sub_vec -> failure x + | VecPrim_mul_vec -> failure x + | VecPrim_sdiv_vec -> failure x + | VecPrim_lsr_vec -> failure x + | VecPrim_asr_vec -> failure x + | VecPrim_lsl_vec -> failure x + | VecPrim_ite_vec -> failure x + | VecPrim_sle_vec -> failure x + | VecPrim_slt_vec -> failure x + | VecPrim_eq_vec -> failure x + | VecPrim_zcast_vec -> failure x + | VecPrim_scast_vec -> failure x + | VecPrim_trunc_vec -> failure x + | VecPrim_select_vec -> failure x + | VecPrim_shuffle_vec -> failure x + | VecPrim_reduce_add -> failure x + + + +end diff --git a/libASL/bnfc/TestSemantics.ml b/libASL/bnfc/TestSemantics.ml new file mode 100644 index 00000000..a4833ccc --- /dev/null +++ b/libASL/bnfc/TestSemantics.ml @@ -0,0 +1,40 @@ +(* File generated by the BNF Converter (bnfc 2.9.5). *) + +open Lexing + +let parse (c : in_channel) : AbsSemantics.stmtLines list = + let lexbuf = Lexing.from_channel c + in + try + ParSemantics.pStmtLines_list LexSemantics.token lexbuf + with + ParSemantics.Error -> + let start_pos = Lexing.lexeme_start_p lexbuf + and end_pos = Lexing.lexeme_end_p lexbuf + in raise (BNFC_Util.Parse_error (start_pos, end_pos)) +;; + +let showTree (t : AbsSemantics.stmtLines list) : string = + "[Abstract syntax]\n\n"^ + ShowSemantics.show (ShowSemantics.showList ShowSemantics.showStmtLines t)^ + "\n\n"^ "[Linearized tree]\n\n"^ + PrintSemantics.printTree PrintSemantics.prtStmtLinesListBNFC t^ + "\n" +;; + +let main () = + let channel = + if Array.length Sys.argv > 1 then open_in Sys.argv.(1) + else stdin + in + try print_string (showTree (parse channel)); + flush stdout; + exit 0 + with BNFC_Util.Parse_error (start_pos, end_pos) -> + Printf.printf "Parse error at %d.%d-%d.%d\n" + start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol + 1) + end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol + 1); + exit 1 +;; + +main ();; diff --git a/libASL/bnfc/dune b/libASL/bnfc/dune new file mode 100644 index 00000000..cc24b2a0 --- /dev/null +++ b/libASL/bnfc/dune @@ -0,0 +1,29 @@ +(rule + (deps Semantics.cf) + (action (run bnfc --ocaml-menhir Semantics.cf)) + (targets AbsSemantics.ml LexSemantics.mll ParSemantics.mly SkelSemantics.ml PrintSemantics.ml ShowSemantics.ml TestSemantics.ml BNFC_Util.ml) + (mode promote) + (enabled_if %{env:ASLP_BNFC_PROMOTE=false})) +; NOTE: bnfc is not run unless ASLP_BNFC_PROMOTE is manually set to `true`. + +(ocamllex LexSemantics) + +(menhir + (modules ParSemantics) + (flags (--explain))) + +(library + (name libASL_bnfc) + (public_name asli.libASL-bnfc) + (flags (:standard -w -27-33-39)) + (modules LexSemantics ParSemantics AbsSemantics BNFC_Util PrintSemantics ShowSemantics SkelSemantics)) + +(executable + (name TestSemantics) + (public_name TestSemantics) + (package asli) + (modes exe byte) + (modules TestSemantics) + (flags (:standard -open LibASL_bnfc)) + (libraries asli.libASL asli.libASL-bnfc)) + diff --git a/libASL/dune b/libASL/dune index d4851b93..8a7a5384 100644 --- a/libASL/dune +++ b/libASL/dune @@ -35,22 +35,22 @@ (public_name asli.libASL-stage1) (flags (:standard -w -27 -cclib -lstdc++ -open LibASL_stage0)) - (modules + (modules gen_backend cpu dis elf eval lexer lexersupport loadASL monad rws tcheck testing transforms rASL_check symbolic_lifter decoder_program call_graph req_analysis offline_transform dis_tc offline_opt - ocaml_backend + ocaml_backend cpp_backend - scala_backend + scala_backend arm_env pretransforms flags ) (preprocessor_deps (alias ../asl_files) (alias cpp_backend_files) ../offlineASL/template_offline_utils.ml) (preprocess (pps ppx_blob)) - (libraries libASL_stage0 libASL_support str mlbdd)) + (libraries libASL_stage0 libASL_support str mlbdd asli.libASL-bnfc)) -(alias +(alias (name cpp_backend_files) (deps ../offlineASL-cpp/subprojects/aslp-lifter/meson.build.in diff --git a/libASL/testing.ml b/libASL/testing.ml index 13d991e2..d1c15649 100644 --- a/libASL/testing.ml +++ b/libASL/testing.ml @@ -454,6 +454,7 @@ type operror = | Op_DisFail of exn | Op_DisEvalFail of exn | Op_DisEvalNotEqual + | Op_BnfcFailure let pp_operror: operror -> string = function @@ -462,6 +463,7 @@ let pp_operror: operror -> string = | Op_DisFail e -> "[2] Disassembly failure: " ^ Printexc.to_string e | Op_DisEvalFail e -> "[3] Dissassembled evaluation failure: " ^ Printexc.to_string e | Op_DisEvalNotEqual -> "[4] Evaluation results not equal" + | Op_BnfcFailure -> "[5] BNFC parsing of RASL failed" type 'a opresult = ('a, operror) Result.t @@ -487,6 +489,17 @@ let op_dis (env: Env.t) (iset: string) (op: Primops.bigint): stmt list opresult with | e -> Result.Error (Op_DisFail e) +let op_try_bnfc (stmts: stmt list): unit opresult = + let open LibASL_bnfc in + try + List.iter + (fun s -> + let lexbuf = Lexing.from_string @@ Utils.to_string @@ PP.pp_raw_stmt s in + ignore @@ ParSemantics.pStmtLines_list LexSemantics.token lexbuf) + stmts; + Result.Ok () + with ParSemantics.Error -> Result.Error Op_BnfcFailure + let op_diseval (env: Env.t) (stmts: stmt list): Env.t opresult = let env = Env.copy env in try @@ -514,6 +527,7 @@ let op_test_opcode (env: Env.t) (iset: string) (op: int): Env.t opresult = let (let*) = Result.bind in let* evalenv = op_eval initenv iset op in let* disstmts = op_dis env iset op in + let* _ = op_try_bnfc disstmts in let* disevalenv = op_diseval initenv disstmts in op_compare (evalenv, disevalenv)