diff --git a/.github/workflows/deploy-doc.yml b/.github/workflows/deploy-doc.yml index d12134f..e69d529 100644 --- a/.github/workflows/deploy-doc.yml +++ b/.github/workflows/deploy-doc.yml @@ -52,7 +52,7 @@ jobs: - name: Upload artifact uses: actions/upload-pages-artifact@v3 with: - path: _html + path: _html/html/bincaml - name: Deploy odoc to GitHub Pages id: deployment diff --git a/lib/fe/AbsBasilIR.ml b/lib/fe/AbsBasilIR.ml index d7f64bc..84303df 100644 --- a/lib/fe/AbsBasilIR.ml +++ b/lib/fe/AbsBasilIR.ml @@ -173,6 +173,7 @@ and expr = | Expr_SignExtend of intVal * expr | Expr_Extract of intVal * intVal * expr | Expr_Concat of expr list + | Expr_Repeat of intVal * expr and lambdaDef = LambdaDef1 of localVar list * lambdaSep * expr diff --git a/lib/fe/BasilIR.cf b/lib/fe/BasilIR.cf index 0c11f75..8d072cf 100644 --- a/lib/fe/BasilIR.cf +++ b/lib/fe/BasilIR.cf @@ -199,6 +199,7 @@ Expr_ZeroExtend . Expr ::= "zero_extend" "(" IntVal "," Expr ")" ; Expr_SignExtend . Expr ::= "sign_extend" "(" IntVal "," Expr ")" ; Expr_Extract . Expr ::= "extract" "(" IntVal "," IntVal "," Expr ")" ; Expr_Concat . Expr ::= "bvconcat" "(" [Expr] ")" ; +Expr_Repeat . Expr ::= "repeat" "(" IntVal "," Expr ")" ; -- operators diff --git a/lib/fe/LexBasilIR.mll b/lib/fe/LexBasilIR.mll index 6617909..61b7a62 100644 --- a/lib/fe/LexBasilIR.mll +++ b/lib/fe/LexBasilIR.mll @@ -11,9 +11,9 @@ let symbol_table = Hashtbl.create 10 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add symbol_table kwd tok) [(";", SYMB1);(",", SYMB2);(":", SYMB3);("declare-fun", SYMB4);("(", SYMB5);(")", SYMB6);("->", SYMB7);("define-fun", SYMB8);("=", SYMB9);(":=", SYMB10)] -let resword_table = Hashtbl.create 83 +let resword_table = Hashtbl.create 84 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add resword_table kwd tok) - [("axiom", KW_axiom);("memory", KW_memory);("shared", KW_shared);("var", KW_var);("prog", KW_prog);("entry", KW_entry);("proc", KW_proc);("le", KW_le);("be", KW_be);("nop", KW_nop);("load", KW_load);("store", KW_store);("call", KW_call);("indirect", KW_indirect);("assume", KW_assume);("guard", KW_guard);("assert", KW_assert);("goto", KW_goto);("unreachable", KW_unreachable);("return", KW_return);("phi", KW_phi);("block", KW_block);("true", KW_true);("false", KW_false);("forall", KW_forall);("exists", KW_exists);("old", KW_old);("boolnot", KW_boolnot);("intneg", KW_intneg);("booltobv1", KW_booltobv1);("zero_extend", KW_zero_extend);("sign_extend", KW_sign_extend);("extract", KW_extract);("bvconcat", KW_bvconcat);("eq", KW_eq);("neq", KW_neq);("bvnot", KW_bvnot);("bvneg", KW_bvneg);("bvand", KW_bvand);("bvor", KW_bvor);("bvadd", KW_bvadd);("bvmul", KW_bvmul);("bvudiv", KW_bvudiv);("bvurem", KW_bvurem);("bvshl", KW_bvshl);("bvlshr", KW_bvlshr);("bvnand", KW_bvnand);("bvnor", KW_bvnor);("bvxor", KW_bvxor);("bvxnor", KW_bvxnor);("bvcomp", KW_bvcomp);("bvsub", KW_bvsub);("bvsdiv", KW_bvsdiv);("bvsrem", KW_bvsrem);("bvsmod", KW_bvsmod);("bvashr", KW_bvashr);("bvule", KW_bvule);("bvugt", KW_bvugt);("bvuge", KW_bvuge);("bvult", KW_bvult);("bvslt", KW_bvslt);("bvsle", KW_bvsle);("bvsgt", KW_bvsgt);("bvsge", KW_bvsge);("intadd", KW_intadd);("intmul", KW_intmul);("intsub", KW_intsub);("intdiv", KW_intdiv);("intmod", KW_intmod);("intlt", KW_intlt);("intle", KW_intle);("intgt", KW_intgt);("intge", KW_intge);("booland", KW_booland);("boolor", KW_boolor);("boolimplies", KW_boolimplies);("require", KW_require);("requires", KW_requires);("ensure", KW_ensure);("ensures", KW_ensures);("invariant", KW_invariant);("rely", KW_rely);("guarantee", KW_guarantee)] + [("axiom", KW_axiom);("memory", KW_memory);("shared", KW_shared);("var", KW_var);("prog", KW_prog);("entry", KW_entry);("proc", KW_proc);("le", KW_le);("be", KW_be);("nop", KW_nop);("load", KW_load);("store", KW_store);("call", KW_call);("indirect", KW_indirect);("assume", KW_assume);("guard", KW_guard);("assert", KW_assert);("goto", KW_goto);("unreachable", KW_unreachable);("return", KW_return);("phi", KW_phi);("block", KW_block);("true", KW_true);("false", KW_false);("forall", KW_forall);("exists", KW_exists);("old", KW_old);("boolnot", KW_boolnot);("intneg", KW_intneg);("booltobv1", KW_booltobv1);("zero_extend", KW_zero_extend);("sign_extend", KW_sign_extend);("extract", KW_extract);("bvconcat", KW_bvconcat);("repeat", KW_repeat);("eq", KW_eq);("neq", KW_neq);("bvnot", KW_bvnot);("bvneg", KW_bvneg);("bvand", KW_bvand);("bvor", KW_bvor);("bvadd", KW_bvadd);("bvmul", KW_bvmul);("bvudiv", KW_bvudiv);("bvurem", KW_bvurem);("bvshl", KW_bvshl);("bvlshr", KW_bvlshr);("bvnand", KW_bvnand);("bvnor", KW_bvnor);("bvxor", KW_bvxor);("bvxnor", KW_bvxnor);("bvcomp", KW_bvcomp);("bvsub", KW_bvsub);("bvsdiv", KW_bvsdiv);("bvsrem", KW_bvsrem);("bvsmod", KW_bvsmod);("bvashr", KW_bvashr);("bvule", KW_bvule);("bvugt", KW_bvugt);("bvuge", KW_bvuge);("bvult", KW_bvult);("bvslt", KW_bvslt);("bvsle", KW_bvsle);("bvsgt", KW_bvsgt);("bvsge", KW_bvsge);("intadd", KW_intadd);("intmul", KW_intmul);("intsub", KW_intsub);("intdiv", KW_intdiv);("intmod", KW_intmod);("intlt", KW_intlt);("intle", KW_intle);("intgt", KW_intgt);("intge", KW_intge);("booland", KW_booland);("boolor", KW_boolor);("boolimplies", KW_boolimplies);("require", KW_require);("requires", KW_requires);("ensure", KW_ensure);("ensures", KW_ensures);("invariant", KW_invariant);("rely", KW_rely);("guarantee", KW_guarantee)] let unescapeInitTail (s:string) : string = let rec unesc s = match s with diff --git a/lib/fe/ParBasilIR.mly b/lib/fe/ParBasilIR.mly index 9319c0b..7bf408c 100644 --- a/lib/fe/ParBasilIR.mly +++ b/lib/fe/ParBasilIR.mly @@ -7,7 +7,7 @@ open AbsBasilIR open Lexing %} -%token KW_axiom KW_memory KW_shared KW_var KW_prog KW_entry KW_proc KW_le KW_be KW_nop KW_load KW_store KW_call KW_indirect KW_assume KW_guard KW_assert KW_goto KW_unreachable KW_return KW_phi KW_block KW_true KW_false KW_forall KW_exists KW_old KW_boolnot KW_intneg KW_booltobv1 KW_zero_extend KW_sign_extend KW_extract KW_bvconcat KW_eq KW_neq KW_bvnot KW_bvneg KW_bvand KW_bvor KW_bvadd KW_bvmul KW_bvudiv KW_bvurem KW_bvshl KW_bvlshr KW_bvnand KW_bvnor KW_bvxor KW_bvxnor KW_bvcomp KW_bvsub KW_bvsdiv KW_bvsrem KW_bvsmod KW_bvashr KW_bvule KW_bvugt KW_bvuge KW_bvult KW_bvslt KW_bvsle KW_bvsgt KW_bvsge KW_intadd KW_intmul KW_intsub KW_intdiv KW_intmod KW_intlt KW_intle KW_intgt KW_intge KW_booland KW_boolor KW_boolimplies KW_require KW_requires KW_ensure KW_ensures KW_invariant KW_rely KW_guarantee +%token KW_axiom KW_memory KW_shared KW_var KW_prog KW_entry KW_proc KW_le KW_be KW_nop KW_load KW_store KW_call KW_indirect KW_assume KW_guard KW_assert KW_goto KW_unreachable KW_return KW_phi KW_block KW_true KW_false KW_forall KW_exists KW_old KW_boolnot KW_intneg KW_booltobv1 KW_zero_extend KW_sign_extend KW_extract KW_bvconcat KW_repeat KW_eq KW_neq KW_bvnot KW_bvneg KW_bvand KW_bvor KW_bvadd KW_bvmul KW_bvudiv KW_bvurem KW_bvshl KW_bvlshr KW_bvnand KW_bvnor KW_bvxor KW_bvxnor KW_bvcomp KW_bvsub KW_bvsdiv KW_bvsrem KW_bvsmod KW_bvashr KW_bvule KW_bvugt KW_bvuge KW_bvult KW_bvslt KW_bvsle KW_bvsgt KW_bvsge KW_intadd KW_intmul KW_intsub KW_intdiv KW_intmod KW_intlt KW_intle KW_intgt KW_intge KW_booland KW_boolor KW_boolimplies KW_require KW_requires KW_ensure KW_ensures KW_invariant KW_rely KW_guarantee %token SYMB1 /* ; */ %token SYMB2 /* , */ @@ -560,6 +560,7 @@ expr : value { Expr_Literal $1 } | KW_sign_extend SYMB5 intVal SYMB2 expr SYMB6 { Expr_SignExtend ($3, $5) } | KW_extract SYMB5 intVal SYMB2 intVal SYMB2 expr SYMB6 { Expr_Extract ($3, $5, $7) } | KW_bvconcat SYMB5 expr_list SYMB6 { Expr_Concat $3 } + | KW_repeat SYMB5 intVal SYMB2 expr SYMB6 { Expr_Repeat ($3, $5) } ; lambdaDef : SYMB5 localVar_list SYMB6 lambdaSep expr { LambdaDef1 ($2, $4, $5) } diff --git a/lib/fe/PrintBasilIR.ml b/lib/fe/PrintBasilIR.ml index 09426d2..7bfcb59 100644 --- a/lib/fe/PrintBasilIR.ml +++ b/lib/fe/PrintBasilIR.ml @@ -363,6 +363,7 @@ and prtExpr (i:int) (e : AbsBasilIR.expr) : doc = match e with | AbsBasilIR.Expr_SignExtend (intval, expr) -> prPrec i 0 (concatD [render "sign_extend" ; render "(" ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr ; render ")"]) | AbsBasilIR.Expr_Extract (intval1, intval2, expr) -> prPrec i 0 (concatD [render "extract" ; render "(" ; prtIntVal 0 intval1 ; render "," ; prtIntVal 0 intval2 ; render "," ; prtExpr 0 expr ; render ")"]) | AbsBasilIR.Expr_Concat exprs -> prPrec i 0 (concatD [render "bvconcat" ; render "(" ; prtExprListBNFC 0 exprs ; render ")"]) + | AbsBasilIR.Expr_Repeat (intval, expr) -> prPrec i 0 (concatD [render "repeat" ; render "(" ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr ; render ")"]) and prtExprListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) diff --git a/lib/fe/ShowBasilIR.ml b/lib/fe/ShowBasilIR.ml index 50be23d..625b25d 100644 --- a/lib/fe/ShowBasilIR.ml +++ b/lib/fe/ShowBasilIR.ml @@ -245,6 +245,7 @@ and showExpr (e : AbsBasilIR.expr) : showable = match e with | AbsBasilIR.Expr_SignExtend (intval, expr) -> s2s "Expr_SignExtend" >> c2s ' ' >> c2s '(' >> showIntVal intval >> s2s ", " >> showExpr expr >> c2s ')' | AbsBasilIR.Expr_Extract (intval0, intval, expr) -> s2s "Expr_Extract" >> c2s ' ' >> c2s '(' >> showIntVal intval0 >> s2s ", " >> showIntVal intval >> s2s ", " >> showExpr expr >> c2s ')' | AbsBasilIR.Expr_Concat exprs -> s2s "Expr_Concat" >> c2s ' ' >> c2s '(' >> showList showExpr exprs >> c2s ')' + | AbsBasilIR.Expr_Repeat (intval, expr) -> s2s "Expr_Repeat" >> c2s ' ' >> c2s '(' >> showIntVal intval >> s2s ", " >> showExpr expr >> c2s ')' and showLambdaDef (e : AbsBasilIR.lambdaDef) : showable = match e with diff --git a/lib/fe/SkelBasilIR.ml b/lib/fe/SkelBasilIR.ml index 21c1897..c82f1e9 100644 --- a/lib/fe/SkelBasilIR.ml +++ b/lib/fe/SkelBasilIR.ml @@ -262,6 +262,7 @@ and transExpr (x : expr) : result = match x with | Expr_SignExtend (intval, expr) -> failure x | Expr_Extract (intval0, intval, expr) -> failure x | Expr_Concat exprs -> failure x + | Expr_Repeat (intval, expr) -> failure x and transLambdaDef (x : lambdaDef) : result = match x with diff --git a/lib/loadir.ml b/lib/loadir.ml index 0e84a5c..223dbfa 100644 --- a/lib/loadir.ml +++ b/lib/loadir.ml @@ -237,7 +237,7 @@ module BasilASTLoader = struct | TypeMapType maptype -> transMapType maptype | TypeBVType (BVType1 bvtype) -> transBVTYPE bvtype - and transIntVal (x : intVal) : PrimInt.t = + and trans_intval (x : intVal) : PrimInt.t = match x with | IntVal_Hex (IntegerHex (_, ihex)) -> Z.of_string ihex | IntVal_Dec (IntegerDec (_, i)) -> Z.of_string i @@ -262,7 +262,7 @@ module BasilASTLoader = struct | Stmt_Load_Var (lvar, endian, var, expr, intval) -> let endian = trans_endian endian in let mem = trans_var p_st var in - let cells = transIntVal intval |> Z.to_int in + let cells = trans_intval intval |> Z.to_int in `Stmt (Instr_Load { @@ -274,7 +274,7 @@ module BasilASTLoader = struct }) | Stmt_Store_Var (lhs, endian, var, addr, value, intval) -> let endian = trans_endian endian in - let cells = transIntVal intval |> Z.to_int in + let cells = trans_intval intval |> Z.to_int in let mem = trans_var p_st var in let lhs = trans_lvar p_st lhs in `Stmt @@ -302,7 +302,7 @@ module BasilASTLoader = struct Option.get_exn_or ("memory undefined: " ^ n) @@ Var.Decls.find_opt p_st.prog.globals n in - let cells = transIntVal intval |> Z.to_int in + let cells = trans_intval intval |> Z.to_int in `Stmt (Instr_Load { @@ -314,7 +314,7 @@ module BasilASTLoader = struct }) | Stmt_Store (endian, bident, addr, value, intval) -> let endian = trans_endian endian in - let cells = transIntVal intval |> Z.to_int in + let cells = trans_intval intval |> Z.to_int in let mem = let n = unsafe_unsigil (`Global bident) in Option.get_exn_or ("memory undefined: " ^ n) @@ -529,25 +529,33 @@ module BasilASTLoader = struct BasilExpr.unexp ~op:(transUnOp unop) (trans_expr expr) | Expr_ZeroExtend (intval, expr) -> BasilExpr.zero_extend - ~n_prefix_bits:(Z.to_int @@ transIntVal intval) + ~n_prefix_bits:(Z.to_int @@ trans_intval intval) (trans_expr expr) | Expr_SignExtend (intval, expr) -> BasilExpr.sign_extend - ~n_prefix_bits:(Z.to_int @@ transIntVal intval) + ~n_prefix_bits:(Z.to_int @@ trans_intval intval) (trans_expr expr) | Expr_Extract (ival0, intval, expr) -> BasilExpr.extract - ~hi_excl:(transIntVal ival0 |> Z.to_int) - ~lo_incl:(transIntVal intval |> Z.to_int) + ~hi_excl:(trans_intval ival0 |> Z.to_int) + ~lo_incl:(trans_intval intval |> Z.to_int) (trans_expr expr) + | Expr_Repeat (repeats, n) -> + let repeats = trans_intval repeats in + let e = trans_expr n in + if Z.equal Z.one repeats then e + else + BasilExpr.applyintrin ~op:`BVConcat + (List.init (Z.to_int repeats) (fun _ -> e)) | Expr_Concat exprs -> BasilExpr.applyintrin ~op:`BVConcat (List.map trans_expr exprs) | Expr_Literal (Value_BV (BVVal1 (intval, BVType1 bvtype))) -> BasilExpr.bvconst (match transBVTYPE bvtype with - | Bitvector size -> Bitvec.create ~size (transIntVal intval) + | Bitvector size -> Bitvec.create ~size (trans_intval intval) | _ -> failwith "unreachable") - | Expr_Literal (Value_Int intval) -> BasilExpr.intconst (transIntVal intval) + | Expr_Literal (Value_Int intval) -> + BasilExpr.intconst (trans_intval intval) | Expr_Literal Value_True -> BasilExpr.boolconst true | Expr_Literal Value_False -> BasilExpr.boolconst false | Expr_Old e -> BasilExpr.unexp ~op:`Old (trans_expr e)