Merge remote-tracking branch 'origin/partial_eval' into separate-serv…

…er-module

libASL/dis.ml

@@ -1580,6 +1580,7 @@ let dis_core (env: Eval.Env.t) (unroll_bound) ((lenv,globals): env) (decode: dec
     let stmts' = Transforms.CaseSimp.do_transform stmts' in
     let stmts' = Transforms.RemoveRegisters.run stmts' in
     let stmts' = Transforms.AppendZeros.run stmts' in
+    let stmts' = Transforms.BitITESimp.do_transform stmts' in
 
     if !debug_level >= 2 then begin
         let stmts' = Asl_visitor.visit_stmts (new Asl_utils.resugarClass (!TC.binop_table)) stmts' in

libASL/symbolic.ml

@@ -183,6 +183,11 @@ let sym_of_tuple (loc: AST.l) (v: sym): sym list  =
   | Exp (Expr_Tuple vs) -> (List.map (fun v -> Exp v) vs)
   | _ -> raise (EvalError (loc, "tuple expected. Got "^ pp_sym v))
 
+let eval_lit (x: sym) =
+  match x with
+  | Val _ -> x
+  | Exp e -> sym_of_expr e
+
 (* Types *)
 
 let type_bool = Type_Constructor(Ident "boolean")
@@ -247,7 +252,19 @@ let expr_true    = Expr_Var (Ident "TRUE")
 let expr_false   = Expr_Var (Ident "FALSE")
 let sym_zeros n  = Val (VBits (prim_zeros_bits (Z.of_int n)))
 
-let sym_eq_int   = prim_binop "eq_int"
+let rec sym_eq_int loc x y =
+  let x = eval_lit x in
+  let y = eval_lit y in
+  match x, y with
+  | Val x, Val y -> Val (VBool (prim_eq_int (to_integer loc x) (to_integer loc y)))
+  (* (x = x) = True *)
+  | Exp x, Exp y when x = y -> Val (VBool (true))
+  (* (x = x + v) = (v = 0) *)
+  | Exp x, Exp (Expr_TApply (FIdent ("add_int", 0), [], [x'; y])) when x = x' ->
+      sym_eq_int loc (Exp y) (Val (VInt Z.zero))
+  (* TODO: Could benefit from add_int/sub_int reductions by phrasing as x - y = 0 *)
+  | _ -> Exp (Expr_TApply (FIdent ("eq_int", 0), [], [sym_expr x; sym_expr y]) )
+
 let sym_le_int   = prim_binop "le_int"
 
 let sym_eq_bits  = prim_binop "eq_bits"
@@ -287,12 +304,7 @@ let vint_eq cmp = function
   | _ -> false
 
 let is_zero = vint_eq Z.zero
-let is_one = vint_eq Z.one 
-
-let eval_lit (x: sym) =
-  match x with
-  | Val _ -> x
-  | Exp e -> sym_of_expr e
+let is_one = vint_eq Z.one
 
 (* Hook into add_int calls to enforce (expr + val) form and apply simple identities. *)
 let sym_add_int loc (x: sym) (y: sym) =
@@ -344,13 +356,27 @@ let rec sym_sub_int loc (x: sym) (y: sym) =
       let n = Z.of_string v in
       let e = Expr_LitInt (Z.to_string (Z.sub n y)) in
       Exp (Expr_TApply (FIdent ("add_int", 0), [], [x1; e]))
-  (* Elim term *) 
+  (* Elim term *)
   | (Exp x, Exp y) when is_pure_exp y ->
       (match find_elim_term loc x (fun v -> if y = v then Some (Val (VInt Z.zero)) else None) with
       | Some e -> e
       | _ -> t)
   | _ -> t
 
+let rec sym_mul_int (loc: l) (x: sym) (y: sym) =
+  match x, y with
+  | Val x, Val y -> Val (VInt (prim_mul_int (to_integer loc x) (to_integer loc y)))
+  (* x * 1 = x *)
+  | Val x, y
+  | y, Val x when is_one x -> y
+  (* (x + c) * c' = x * c' + c * c' *)
+  | Exp (Expr_TApply (FIdent ("add_int", 0), [], [x; Expr_LitInt lit])), Val (VInt c') ->
+      let c = Z.of_string lit in
+      let offset = Val (VInt (Z.mul c c')) in
+      let base = sym_mul_int loc (Exp x) y in
+      sym_add_int loc base offset
+  | _ -> Exp (Expr_TApply (FIdent ("mul_int", 0), [], [sym_expr x; sym_expr y]))
+
 (*** Symbolic Boolean Operations ***)
 
 let sym_not_bool loc (x: sym) =
@@ -411,6 +437,13 @@ let sym_and_bits loc w (x: sym) (y: sym) =
   | x, Val y when is_one_bits y -> x
   | _ -> Exp (Expr_TApply (FIdent ("and_bits", 0), [w], [sym_expr x; sym_expr y]) )
 
+let sym_add_bits loc w (x: sym) (y: sym) =
+  match x, y with
+  | Val x, Val y -> Val (VBits (prim_add_bits (to_bits loc x) (to_bits loc y)))
+  | Val x, y when is_zero_bits x -> y
+  | x, Val y when is_zero_bits y -> x
+  | _ -> Exp (Expr_TApply (FIdent ("add_bits", 0), [w], [sym_expr x; sym_expr y]) )
+
 let sym_inmask loc v mask =
   match v with
   | Val x -> Val (VBool (prim_in_mask (to_bits loc x) mask))
@@ -421,13 +454,16 @@ let sym_inmask loc v mask =
       let v = Val (VBits {v = mask.v; n}) in
       sym_eq_bits loc (sym_and_bits loc ne (Exp e) m) v
 
-let sym_or_bits loc w (x: sym) (y: sym) =
+let rec sym_or_bits loc w (x: sym) (y: sym) =
   match x, y with
   | Val x, Val y -> Val (VBits (prim_or_bits (to_bits loc x) (to_bits loc y)))
   | Val x, y when is_one_bits x -> Val x
   | x, Val y when is_one_bits y -> Val y
   | Val x, y when is_zero_bits x -> y
   | x, Val y when is_zero_bits y -> x
+  (* (a /\ b) \/ !a ~> b \/ !a *)
+  | Exp (Expr_TApply (FIdent ("and_bits", 0), _, [a; x])), Exp (Expr_TApply (FIdent ("not_bits", 0), _, [a'])) when a = a' ->
+      sym_or_bits loc w (sym_of_expr x) y
   | _ -> Exp (Expr_TApply (FIdent ("or_bits", 0), [w], [sym_expr x; sym_expr y]) )
 
 (** Construct a ITE expression from bitvector operations. Expects arguments to be 1 bit wide. *)
@@ -458,7 +494,7 @@ let rec sym_append_bits (loc: l) (xw: int) (yw: int) (x: sym) (y: sym): sym =
 
   (* Match append of top-bit replicate expressions, turn into sign extend *)
   | (Exp (Expr_TApply (FIdent ("replicate_bits", 0), [Expr_LitInt "1"; w], [e;_])), Exp r) when sym_slice loc (Exp r) (yw - 1) 1 = Exp e ->
-      Exp (Expr_TApply (FIdent ("SignExtend", 0), [int_expr yw;int_expr (xw+yw)], [r; int_expr (xw + yw)])) 
+      Exp (Expr_TApply (FIdent ("SignExtend", 0), [int_expr yw;int_expr (xw+yw)], [r; int_expr (xw + yw)]))
 
   | (x,y) ->
     Exp (expr_prim' "append_bits" [expr_of_int xw; expr_of_int yw] [sym_expr x;sym_expr y])
@@ -484,6 +520,7 @@ and sym_replicate (xw: int) (x: sym) (n: int): sym =
     distributes slices across bitvector append operations.
   *)
 and sym_slice (loc: l) (x: sym) (lo: int) (wd: int): sym =
+  let x = eval_lit x in
   match x with
   | Val v -> Val (extract_bits'' loc v (VInt (Z.of_int lo)) (VInt (Z.of_int wd)))
   | Exp e ->
@@ -529,6 +566,16 @@ and sym_slice (loc: l) (x: sym) (lo: int) (wd: int): sym =
           (sym_slice loc (Exp x1) lo wd)
           (sym_slice loc (Exp x2) lo wd)
 
+    (* (x + y)[wd +: 0] = (x[wd +: 0] + y[wd +: 0]) *)
+    | (Expr_TApply (FIdent ("add_int", 0), [], [x1; x2])) when lo = 0 ->
+        sym_add_bits loc (int_expr wd)
+          (sym_slice loc (Exp x1) lo wd)
+          (sym_slice loc (Exp x2) lo wd)
+
+    (* UInt{wd}(x)[wd +: 0] = x[wd +: 0] *)
+    | (Expr_TApply (FIdent ("cvt_bits_uint", 0), [Expr_LitInt w'], [x1])) when lo = 0 && int_of_string w' = wd ->
+        Exp x1
+
     | (Expr_TApply (FIdent ("append_bits", 0), [Expr_LitInt t1; Expr_LitInt t2], [x1; x2])) ->
       let t2 = int_of_string t2 in
       if t2 < 0 then
@@ -571,7 +618,7 @@ let sym_zero_extend num_zeros old_width e =
       Exp (expr_prim' "ZeroExtend" [expr_of_int old_width; n'] [sym_expr e; n'])
 
 let sym_sign_extend num_zeros old_width (e: sym): sym =
-  match e with 
+  match e with
   | Exp (Expr_TApply (FIdent ("ZeroExtend",0), [Expr_LitInt oldsize; Expr_LitInt newsize], [x; _])) ->
     let size' = string_of_int (num_zeros + int_of_string newsize) in
     Exp (Expr_TApply (FIdent ("ZeroExtend",0), [Expr_LitInt oldsize; Expr_LitInt size'], [x; Expr_LitInt size']))
@@ -687,25 +734,6 @@ let is_insert_mask (b: bitvector): (int * int) option =
       end
   | _ -> None
 
-(*
-let rec elem_read_collapse vw ew v j =
-  match v with
-  | Expr_TApply (FIdent ("Elem.set", 0), [Expr_LitInt vw'; Expr_LitInt ew'], [v; Expr_LitInt i; _; e])
-      when vw = Z.of_string vw' && ew = Z.of_string ew' && Z.of_string i = j ->
-        e
-  | Expr_TApply (FIdent ("Elem.set", 0), [Expr_LitInt vw'; Expr_LitInt ew'], [v; Expr_LitInt i; _; e])
-      when vw = Z.of_string vw' && ew = Z.of_string ew' && Z.of_string i <> j ->
-        elem_read_collapse vw ew v j
-  | Expr_Slices (v, [Slice_LoWd(Expr_LitInt lo, Expr_LitInt wd)]) 
-      when Z.equal (Z.rem (Z.of_string lo) ew) Z.zero ->
-        elem_read_collapse (Z.add vw vw) ew v (Z.add j (Z.div (Z.of_string lo) ew))
-  | _ -> 
-    (Expr_TApply (FIdent ("Elem.read", 0), [Expr_LitInt (Z.to_string vw); Expr_LitInt (Z.to_string ew)], [v; Expr_LitInt (Z.to_string j); Expr_LitInt (Z.to_string ew)]))
-*)
-  (*| ("Elem.read", [Val (VInt vw); Val (VInt ew)], [Exp v; Val (VInt j); _]) ->
-      let e = elem_read_collapse vw ew v j in
-      Some (Exp e)*)
-
 let sym_prim_simplify (name: string) (tes: sym list) (es: sym list): sym option =
   let loc = Unknown in
 
@@ -715,19 +743,11 @@ let sym_prim_simplify (name: string) (tes: sym list) (es: sym list): sym option
     sym_insert_bits loc (Z.to_int w) outer (sym_of_int lo) (sym_of_int wd) mid in
 
   (match (name, tes, es) with
-  | ("add_int",     _,                [x1; x2]) ->
-      Some (sym_add_int loc x1 x2)
-
-  | ("sub_int",     _,                [x1; x2]) -> 
-      Some (sym_sub_int loc x1 x2)
-
-  | ("mul_int",     _,                [Val x1; x2])       when is_one x1 -> Some x2
-  | ("mul_int",     _,                [x1; Val x2])       when is_one x2 -> Some x1
-  | ("mul_int",     _,                [Exp (Expr_TApply (FIdent ("add_int", 0), [], [x1; Expr_LitInt v])); Val (VInt v2)]) ->
-      let v = Z.of_string v in
-      let c = Val (VInt (Z.mul v v2)) in
-      let e = Exp (Expr_TApply (FIdent ("mul_int", 0), [], [x1; Expr_LitInt (Z.to_string v2)])) in
-      Some (sym_add_int loc e c)
+  | ("add_int",  [ ], [x1; x2]) -> Some (sym_add_int loc x1 x2)
+  | ("sub_int",  [ ], [x1; x2]) -> Some (sym_sub_int loc x1 x2)
+  | ("mul_int",  [ ], [x1; x2]) -> Some (sym_mul_int loc x1 x2)
+  | ("eq_int",   [ ], [x1; x2]) -> Some (sym_eq_int loc x1 x2)
+  | ("add_bits", [w], [x1; x2]) -> Some (sym_add_bits loc (sym_expr w) x1 x2)
 
   | ("append_bits", [Val t1; _],      [_; x2])            when is_zero t1 -> Some x2
   | ("append_bits", [_; Val t2],      [x1; _])            when is_zero t2 -> Some x1
@@ -752,9 +772,8 @@ let sym_prim_simplify (name: string) (tes: sym list) (es: sym list): sym option
 
   | ("eq_enum",     _,                [x; Val (VBool true)])
   | ("eq_enum",     _,                [Val (VBool true); x]) -> Some x
-
-  | ("add_bits",    _,                [Val x1; x2])       when is_zero_bits x1 -> Some x2
-  | ("add_bits",    _,                [x1; Val x2])       when is_zero_bits x2 -> Some x1
+  | ("eq_enum",     _,                [x; Val (VBool false)])
+  | ("eq_enum",     _,                [Val (VBool false); x]) -> Some (sym_not_bool loc x)
 
   | ("or_bits",     _,                [Val x1; x2])       when is_zero_bits x1 -> Some x2
   | ("or_bits",     _,                [x1; Val x2])       when is_zero_bits x2 -> Some x1

libASL/transforms.ml

@@ -21,6 +21,7 @@ let pure_prims =
 
 let infer_type (e: expr): ty option =
   match e with
+  | Expr_LitBits bv -> (Some(Type_Bits(Expr_LitInt (string_of_int (String.length bv)))))
   | Expr_Slices(x, [Slice_LoWd(l,w)]) -> Some(Type_Bits(w))
   | Expr_TApply((FIdent(name, _) | Ident(name)), [], _) -> begin
     match name with
@@ -1183,11 +1184,12 @@ module IntToBits = struct
         in
         let narrow_args () = Expr_TApply (f, [expr_of_int wd'], List.map narrow es) in
 
-        (* for add and sub expressions, we only need the lowest n bits in order
+        (* for some arithmetic expressions, we only need the lowest n bits in order
            to have n bits of precision in the output. *)
         (match name_of_FIdent f with
         | "add_bits" -> ChangeDoChildrenPost (narrow_args (), fun x -> Expr_Slices (x, [sl]))
         | "sub_bits" -> ChangeDoChildrenPost (narrow_args (), fun x -> Expr_Slices (x, [sl]))
+        | "mul_bits" -> ChangeDoChildrenPost (narrow_args (), fun x -> Expr_Slices (x, [sl]))
         | _ -> ChangeDoChildrenPost (narrow inner, fun x -> Expr_Slices (x, [sl]))
         )
       | _ -> DoChildren
@@ -1287,7 +1289,7 @@ module CopyProp = struct
     | Expr_Var v -> true
     | Expr_Field (e,_) -> candidateExpr e
     | Expr_Array (e,_) -> candidateExpr e
-    | Expr_TApply (f,_,_) -> (name_of_FIdent f = "Mem.read")
+    (*| Expr_TApply (f,_,_) -> (name_of_FIdent f = "Mem.read")*)
     | _ -> false
 
   let candidateIdent (i: ident) =
@@ -1679,6 +1681,108 @@ module CaseSimp = struct
     xs
 end
 
+(* Transform the following to remove control flow:
+
+  if cond then         ITESimp_0 := cond
+    X1 := E1           X1 := (ITESimp_0 & E1) | (!ITESimp_0 & F1)
+    ...                ...
+    XN := EN           XN := (ITESimp_0 & EN) | (!ITESimp_0 & F1)
+  else            ~>
+    X1 := F1
+    ...
+    XN := F2
+
+  Where:
+    - XNs are written on both edges in the same order.
+    - XNs are single bit variables.
+    - ENs and FNs are pure.
+
+  TODO:
+    - Could generalise to mismatched XNs, as long as self-assign is safe.
+      Not clear if this is okay semantically.
+    - Could generalise to arbitrary bitvectors, if worthwhile.
+      Resulting mask might be worse than branch however.
+    - Generalised order is difficult given dependencies.
+  *)
+module BitITESimp = struct
+  let one = Expr_LitInt "1"
+  let type_bit = Type_Bits one
+
+  (* Test if we can freely perform the operation, even if it wouldn't
+     have been performed in the original branching version *)
+  let rec is_pure e =
+    match e with
+    | Expr_Var _ -> true
+    | Expr_LitBits _ -> true
+    | Expr_LitInt _ -> true
+    | Expr_Slices(e, [Slice_LoWd(lo, wd)]) ->
+        is_pure e && is_pure lo && is_pure wd
+    | Expr_TApply(f, tes, es) ->
+        List.mem f pure_prims &&
+        List.for_all is_pure tes &&
+        List.for_all is_pure es
+    | Expr_Field(e,_) -> is_pure e
+    | Expr_Array(e,i) -> is_pure e && is_pure i
+    | _ -> false
+
+  (* Walk both branches in sync, collect necessary information *)
+  let rec match_body t f =
+    match t, f with
+    | Stmt_Assign(ti,te,loc)::ts, Stmt_Assign(fi,fe,_)::fs
+        when ti = fi && is_pure te && is_pure fe &&
+          infer_type te = Some type_bit ->
+            Option.map (fun rest -> ((ti,te,fe,loc)::rest)) (match_body ts fs)
+    | [], [] -> Some []
+    | _ -> None
+
+  (* Utility to convert a bool test into a bit value, with some cleanup *)
+  let rec bool_to_bit c =
+    match c with
+    | Expr_TApply (FIdent("and_bool", 0), [], ls) ->
+        Expr_TApply (FIdent("and_bits", 0), [one], List.map bool_to_bit ls)
+    | Expr_TApply (FIdent("eq_bits", 0), _, [e; Expr_LitBits "1"])
+    | Expr_TApply (FIdent("eq_bits", 0), _, [Expr_LitBits "1"; e]) -> e
+    | Expr_TApply (FIdent("eq_bits", 0), _, [e; Expr_LitBits "0"])
+    | Expr_TApply (FIdent("eq_bits", 0), _, [Expr_LitBits "0"; e]) ->
+        Expr_TApply (FIdent ("not_bits", 0), [one], [e])
+    | _ -> Expr_TApply (FIdent("cvt_bool_bv", 0), [], [c])
+
+  (* Generate the assignment for a paired expression *)
+  let build_stmt cond (i,e,e',loc) =
+    let e' = sym_or_bits loc one
+        (sym_and_bits loc one cond (sym_of_expr e))
+        (sym_and_bits loc one (sym_not_bits loc one cond) (sym_of_expr e')) in
+    Stmt_Assign (i, sym_expr e', loc)
+
+  (* Given the analysis has succeeded, build the equivalent series of assignments *)
+  let build_assigns cond assigns loc nv =
+    let cond_write = Stmt_ConstDecl(type_bit, nv, bool_to_bit cond, loc) in
+    let cond_load = Exp (Expr_Var nv) in
+    (cond_write::List.map (build_stmt cond_load) assigns)
+
+  class visit_if = object
+    inherit Asl_visitor.nopAslVisitor
+    val mutable next_var = 0
+    method! vstmt (s: stmt): stmt list visitAction =
+      match s with
+      | Stmt_If (cond, t, [], f, loc) ->
+          (match match_body t f with
+          | None -> DoChildren
+          | Some assigns ->
+              let nv = Ident ("ITESimp_" ^ string_of_int next_var) in
+              next_var <- next_var + 1;
+              ChangeTo (build_assigns cond assigns loc nv))
+      | _ -> DoChildren
+  end
+
+  let do_transform (xs: stmt list): stmt list =
+    let stmt_visitor = new visit_if in
+    let xs = visit_stmts stmt_visitor xs in
+    xs
+end
+
+
+
 (* Rewrite expressions with temporary dynamic width bitvectors into equivalent versions with only static bitvectors *)
 module RemoveTempBVs = struct
 

tests/aslt/test_antlr.t

@@ -17,8 +17,10 @@ tests building and running of the antlr grammar. requires java
   (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Field ( (lexpr LExpr_Var ( (ident " PSTATE ") )) , (ident " N ") )) , (expr Expr_Slices ( (expr Expr_Var ( (ident " Cse0__5 ") )) , [ (slice Slice_LoWd ( (expr (integer 63)) , (expr (integer 1)) )) ] )) )))
   (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _R ") )) , (expr (integer 1)) )) , (expr Expr_Var ( (ident " Cse0__5 ") )) )))
   (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SP_EL0 ") )) , (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 64))) ] , [ (expr Expr_Var ( (ident " SP_EL0 ") )) ; (expr (bits '1111111111111111111111111111111111111111111111111111111111100000')) ] )) )))
-  (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _R ") )) , (expr (integer 1)) )) , (expr Expr_TApply ( (ident " Mem.read.0 ") , [ (targs (expr (integer 8))) ] , [ (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 3)) )) ; (expr (integer 8)) ; (expr (integer 0)) ] )) )))
-  (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _R ") )) , (expr (integer 2)) )) , (expr Expr_TApply ( (ident " Mem.read.0 ") , [ (targs (expr (integer 8))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 64))) ] , [ (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 3)) )) ; (expr (bits '0000000000000000000000000000000000000000000000000000000000001000')) ] )) ; (expr (integer 8)) ; (expr (integer 0)) ] )) )))
+  (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 64)) )) , (ident " Exp16__5 ") , (expr Expr_TApply ( (ident " Mem.read.0 ") , [ (targs (expr (integer 8))) ] , [ (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 3)) )) ; (expr (integer 8)) ; (expr (integer 0)) ] )) )))
+  (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 64)) )) , (ident " Exp18__5 ") , (expr Expr_TApply ( (ident " Mem.read.0 ") , [ (targs (expr (integer 8))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 64))) ] , [ (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 3)) )) ; (expr (bits '0000000000000000000000000000000000000000000000000000000000001000')) ] )) ; (expr (integer 8)) ; (expr (integer 0)) ] )) )))
+  (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _R ") )) , (expr (integer 1)) )) , (expr Expr_Var ( (ident " Exp16__5 ") )) )))
+  (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _R ") )) , (expr (integer 2)) )) , (expr Expr_Var ( (ident " Exp18__5 ") )) )))
   (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _R ") )) , (expr (integer 3)) )) , (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 64))) ] , [ (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 3)) )) ; (expr (bits '0000000000000000000000000000000000000000000000000000000010000000')) ] )) )))
   (stmt (call_stmt Stmt_TCall ( (ident " Mem.set.0 ") , [ (targs (expr (integer 8))) ] , [ (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 3)) )) ; (expr (integer 8)) ; (expr (integer 0)) ; (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 1)) )) ] )))
   (stmt (call_stmt Stmt_TCall ( (ident " Mem.set.0 ") , [ (targs (expr (integer 8))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 64))) ] , [ (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 3)) )) ; (expr (bits '0000000000000000000000000000000000000000000000000000000000001000')) ] )) ; (expr (integer 8)) ; (expr (integer 0)) ; (expr Expr_Array ( (expr Expr_Var ( (ident " _R ") )) , (expr (integer 2)) )) ] )))