dis: do not emit slices with dynamic indices

also fixup extraction due to missed case in nested slice

we should now have all static-low-index extractions

libASL/dis.ml

@@ -307,7 +307,6 @@ module LocalEnv = struct
           | Some (t,_) -> Some (t,v)
           | None -> internal_error loc @@ "failed to set resolved variable: " ^ pp_var x)) n env.locals in
         { env with locals }
-
 end
 
 type tree =
@@ -718,7 +717,14 @@ and type_of_load (loc: l) (x: expr): ty rws =
       (match Tcheck.derefType env t with
       | Type_Array(ixty, elty) -> dis_type loc elty
       | _ -> raise (EvalError (loc, "Can't type expression: " ^ pp_expr a)))
-  | _ -> raise (EvalError (loc, "Can't type expression: " ^ pp_expr x)))
+  | _ ->
+      let@ config = DisEnv.read in
+      let@ lenv = DisEnv.get in
+      let vars x = Some (fst @@ snd @@ LocalEnv.resolveGetVar loc (Ident x) lenv) in
+
+      match Dis_tc.infer_type' x vars config.eval_env  with
+      | Some t -> dis_type loc t
+      | None -> raise (EvalError (loc, "Can't type expression: " ^ pp_expr x)))
 
 and type_access_chain (loc: l) (var: var) (ref: access_chain list): ty rws =
     let Var (_,id) = var in
@@ -870,15 +876,18 @@ and dis_expr' (loc: l) (x: AST.expr): sym rws =
             let+ vs = DisEnv.traverse (fun f -> dis_load_with_type loc (Expr_Field(e,f))) fs in
             let vs' = List.map (fun (t,x) -> (width_of_type loc t, x)) vs in
             sym_concat loc vs'
-    | Expr_Slices(e, [s]) ->
-            let@ e' = dis_expr loc e in
-            let+ (i,w) = dis_slice loc s in
-            sym_extract_bits loc e' i w
     | Expr_Slices(e, ss) ->
+            let@ config = DisEnv.read in
+            let@ ty = type_of_load loc e in
             let@ e' = dis_expr loc e in
             let+ ss' = DisEnv.traverse (dis_slice loc) ss in
-            let vs = List.map (fun (i,w) -> (int_of_sym w, sym_extract_bits loc e' i w)) ss' in
-            sym_concat loc vs
+            (match ty with
+            | Type_Constructor (Ident "integer") ->
+                Exp (Expr_Slices(sym_expr e', List.map (fun (x,y) -> Slice_LoWd(sym_expr x,sym_expr y)) ss'))
+            | _ ->
+                let vwd = width_of_type loc ty in
+                let vs = List.map (fun (i,w) -> (int_of_sym w, sym_extract_bits loc e' vwd 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
@@ -1201,7 +1210,7 @@ and dis_lexpr' (loc: l) (x: lexpr) (r: sym): unit rws =
             | [] -> DisEnv.pure prev
             | (s :: ss) ->
                 let@ (i, w) = dis_slice loc s in
-                let v       = sym_extract_bits loc r o w in
+                let v       = sym_extract_bits loc r prev_width o w in
                 eval (sym_add_int loc o w) ss (sym_insert_bits loc prev_width prev i w v)
             )
         in

libASL/dis_tc.ml

@@ -116,11 +116,11 @@ let get_ret_type f targs env =
       Some (subst_type subst ty)
   | _ -> None
 
-let infer_type (e: expr) vars env =
+let rec infer_type' (e: expr) vars env =
   match e with
   | Expr_Var (Ident "TRUE")
   | Expr_Var (Ident "FALSE") -> (Some(Type_Constructor(Ident ("boolean"))))
-  | Expr_Var v -> Bindings.find_opt v vars
+  | Expr_Var (Ident v) -> vars v
   | Expr_LitInt _ -> (Some(Value.type_integer))
   | 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)))
@@ -131,4 +131,8 @@ let infer_type (e: expr) vars env =
       (match prim_type f targs with
       | Some t -> Some t 
       | None -> get_ret_type f targs env)
+  | Expr_Parens e -> infer_type' e vars env
   | _ -> None
+
+let infer_type e vars env =
+  infer_type' e (fun v -> Bindings.find_opt (Ident v) vars) env

libASL/symbolic.ml

@@ -550,7 +550,7 @@ and sym_slice (loc: l) (x: sym) (lo: int) (wd: int): sym =
     | _ -> Exp slice_expr)
 
 (** Wrapper around sym_slice to handle cases of symbolic slice bounds *)
-let sym_extract_bits loc v i w =
+let rec sym_extract_bits loc v vwd i w =
   match (v, i, w) with
   (* Constant slice *)
   | _, Val i', Val w' ->
@@ -560,8 +560,13 @@ let sym_extract_bits loc v i w =
   (* Nested slice *)
   | Exp (Expr_Slices (e, [Slice_LoWd (lo,wd)])), lo', wd' ->
       let lo = sym_add_int loc (Exp lo) lo' in
-      Exp (Expr_Slices (e, [Slice_LoWd (sym_expr lo, sym_expr wd')]))
-  | _ -> Exp (Expr_Slices (sym_expr v, [Slice_LoWd (sym_expr i, sym_expr w)]))
+      sym_extract_bits loc (sym_of_expr e) vwd lo wd'
+  (* Lower dynamically-indexed extractions to a shift. Requires static width. *)
+  | v, Exp lo, Val w ->
+      let shifted = Exp (Expr_TApply (FIdent ("LSR", 0), [Expr_LitInt (string_of_int vwd)], [sym_expr v; lo])) in
+      sym_slice loc shifted 0 (to_int loc w)
+  | _ -> failwith "asjdio"
+  (* | _ -> Exp (Expr_Slices (sym_expr v, [Slice_LoWd (sym_expr i, sym_expr w)])) *)
 
 let sym_zero_extend num_zeros old_width e =
   match sym_append_bits Unknown num_zeros old_width (Val (val_zeros num_zeros)) e with