Completely remove unsafe append by extending int simps

libASL/dis.ml

@@ -813,8 +813,8 @@ and dis_expr' (loc: l) (x: AST.expr): sym rws =
     | Expr_Slices(e, ss) ->
             let@ e' = dis_expr loc e in
             let+ ss' = DisEnv.traverse (dis_slice loc) ss in
-            let vs = List.map (fun (i,w) -> sym_extract_bits loc e' i w) ss' in
-            sym_concat_unsafe loc vs
+            let vs = List.map (fun (i,w) -> (int_of_sym w, sym_extract_bits loc e' i w)) ss' in
+            sym_concat loc vs
     | Expr_In(e, p) ->
             let@ e' = dis_expr loc e in
             let@ p' = dis_pattern loc e' p in

libASL/symbolic.ml

@@ -165,6 +165,12 @@ let pp_sym (rs: sym): string =
     | Val v -> Printf.sprintf "Val(%s)" (pp_value v)
     | Exp e -> Printf.sprintf "Exp(%s)" (pp_expr e)
 
+let int_of_sym (e: sym): int =
+  match e with
+  | Val (VInt n) -> Z.to_int n
+  | Exp e        -> int_of_expr e
+  | _ -> failwith @@ "int_of_sym: cannot coerce to int " ^ pp_sym e
+
 let sym_of_tuple (loc: AST.l) (v: sym): sym list  =
   match v with
   | Val (VTuple vs) -> (List.map (fun v -> Val v) vs)
@@ -236,8 +242,6 @@ 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 sym_add_int  = prim_binop "add_int"
-let sym_sub_int  = prim_binop "sub_int"
 let sym_le_int   = prim_binop "le_int"
 
 let sym_eq_bits  = prim_binop "eq_bits"
@@ -257,6 +261,86 @@ let sym_eq (loc: AST.l) (x: sym) (y: sym): sym =
       | _ -> failwith @@ "sym_eq: unknown value type " ^ (pp_sym x) ^ " " ^ (pp_sym y))
   | (_,_) -> failwith "sym_eq: insufficient info to resolve type")
 
+let rec is_pure_exp (e: expr) =
+  match e with
+  | Expr_TApply (FIdent (f, 0), targs, args) ->
+      (List.mem f prims_pure) && List.for_all (is_pure_exp) targs && List.for_all (is_pure_exp) args
+  | Expr_Slices(e, ss) ->
+      is_pure_exp e && List.for_all is_pure_slice ss
+  | Expr_Var _ -> true
+  | Expr_LitInt _ -> true
+  | _ -> false
+
+and is_pure_slice (s: slice) =
+  match s with
+  | Slice_Single i -> is_pure_exp i
+  | Slice_HiLo(hi, lo) -> is_pure_exp hi && is_pure_exp lo
+  | Slice_LoWd(lo, wd) -> is_pure_exp lo && is_pure_exp wd
+
+let vint_eq cmp = function
+  | VInt x when Z.equal cmp x -> true
+  | _ -> 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
+
+(* Hook into add_int calls to enforce (expr + val) form and apply simple identities. *)
+let sym_add_int loc (x: sym) (y: sym) =
+  let x = eval_lit x in
+  let y = eval_lit y in
+  match (x, y) with
+  | (Val (VInt x), Val (VInt y)) -> Val (VInt (Z.add x y))
+  (* Zero Identity *)
+  | (Val z, Exp x)
+  | (Exp x, Val z) when is_zero z -> Exp x
+  (* Chained constant add *)
+  | (Exp (Expr_TApply (FIdent ("add_int", 0), _, [x1; Expr_LitInt v])), Val (VInt y)) ->
+      let n = Z.of_string v in
+      let e = Expr_LitInt (Z.to_string (Z.add n y)) in
+      Exp (Expr_TApply (FIdent ("add_int", 0), [], [x1; e]))
+  (* Normalise *)
+  | (Val _, Exp _) ->
+      Exp (Expr_TApply (FIdent ("add_int", 0), [], [sym_expr y; sym_expr x]))
+  | _ -> Exp (Expr_TApply (FIdent ("add_int", 0), [], [sym_expr x; sym_expr y]))
+
+let rec find_elim_term loc (e: expr) (f: expr -> sym option) =
+  match f e with
+  | Some e' -> Some e'
+  | None ->
+      (match e with
+      | Expr_TApply (FIdent ("add_int", 0), _, [x1; x2]) ->
+          (match find_elim_term loc x2 f with
+           | Some e' -> Some (sym_add_int loc (Exp x1) e')
+           | _ -> (match find_elim_term loc x1 f with
+                  | Some e' -> Some (sym_add_int loc e' (Exp x2))
+                  | _ -> None))
+      | _ -> None)
+
+let sym_sub_int loc (x: sym) (y: sym) =
+  let x = eval_lit x in
+  let y = eval_lit y in
+  let t = Exp (Expr_TApply (FIdent ("sub_int", 0), [], [sym_expr x; sym_expr y])) in
+  match (x,y) with
+  | (Val (VInt x), Val (VInt y)) -> Val (VInt (Z.sub x y))
+  (* Zero Identity *)
+  | (Exp x, Val z) when is_zero z -> Exp x
+  (* Chained constant add *)
+  | (Exp (Expr_TApply (FIdent ("add_int", 0), _, [x1; Expr_LitInt v])), Val (VInt y)) ->
+      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 *) 
+  | (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
+
 (*** Symbolic Boolean Operations ***)
 
 let sym_not_bool loc (x: sym) =
@@ -360,10 +444,6 @@ let rec sym_append_bits (loc: l) (xw: int) (yw: int) (x: sym) (y: sym): sym =
     Exp (expr_prim' "append_bits" [expr_of_int xw; expr_of_int yw] [sym_expr x;sym_expr y])
   )
 
-(* WARNING: incorrect type arguments passed to append_bits but sufficient for evaluation
-   of primitive with eval_prim. *)
-and sym_append_bits_unsafe loc x y = sym_append_bits loc (-1) (-1) x y
-
 and sym_replicate (xw: int) (x: sym) (n: int): sym =
   match n with
   | _ when n < 0 -> failwith @@ "sym_replicate: negative replicate count"
@@ -525,14 +605,6 @@ let sym_concat (loc: AST.l) (xs: (int * sym) list): sym =
   | [] -> Val (VBits empty_bits)
   | x::xs -> let (_,r) = List.fold_left body x xs in r
 
-(** Append a list of bitvectors together
-    TODO: Will inject invalid widths due to unsafe sym_append_bits call.
- *)
-let sym_concat_unsafe (loc: AST.l) (xs: sym list): sym =
-  match xs with
-  | [] -> Val (VBits empty_bits)
-  | x::xs -> List.fold_left (sym_append_bits_unsafe loc) x xs
-
 (* Identify the bits in an expression that might be 1.
    Represent these as a bitvector with 1s in their position, of width w. *)
 let rec maybe_set (w: Z.t) (e: expr): bitvector =
@@ -578,22 +650,19 @@ let is_insert_mask (b: bitvector): (int * int) option =
 let sym_prim_simplify (name: string) (tes: sym list) (es: sym list): sym option =
   let loc = Unknown in
 
-  let vint_eq cmp = function
-    | VInt x when Z.equal cmp x -> true
-    | _ -> false in
-
-  let [@warning "-26"] is_zero = vint_eq Z.zero
-  and [@warning "-26"] is_one = vint_eq Z.one in
-
   (* Utility to overwrite outer[wd:lo] with inner[wd:lo] *)
   let insert w outer lo wd inner =
     let mid = sym_slice loc inner lo wd in
     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",     _,                [Val x1; x2])       when is_zero x1 -> Some x2
-  | ("add_int",     _,                [x1; Val x2])       when is_zero x2 -> Some x1
-  | ("sub_int",     _,                [x1; Val x2])       when is_zero x2 -> Some x1
+  | ("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