Handle repeat

.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

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

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
 

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

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) }

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 [])

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

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

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)