Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add partial support for sysreg accessors #47

Merged
merged 3 commits into from
Feb 22, 2024
Merged

Add partial support for sysreg accessors #47

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c4e77a7
Reduce usage of unsafe bitvector append
ncough Feb 20, 2024
baf1bd8
Add sysreg access mechanisms
ncough Feb 20, 2024
52fc84b
Completely remove unsafe append by extending int simps
ncough Feb 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
(mra_tools/arch/arch_decode.asl as mra_tools/arch/arch_decode.asl )
(mra_tools/arch/arch_instrs.asl as mra_tools/arch/arch_instrs.asl )
(mra_tools/arch/regs.asl as mra_tools/arch/regs.asl )
(mra_tools/arch/regs_access.asl as mra_tools/arch/regs_access.asl )
(mra_tools/support/aes.asl as mra_tools/support/aes.asl )
(mra_tools/support/barriers.asl as mra_tools/support/barriers.asl )
(mra_tools/support/debug.asl as mra_tools/support/debug.asl )
Expand Down
24 changes: 15 additions & 9 deletions libASL/dis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -734,12 +734,17 @@ and dis_slice (loc: l) (x: slice): (sym * sym) rws =
These structures are not supported by the target and must be removed for successful translation.
TODO: This does not appear to be a problem at the moment, but requires greater testing to be sure.
*)
and dis_load loc x =
let body = dis_load_chain loc x [] in
and dis_load (loc: l) (x: expr): sym rws =
let body = (let+ (_,s) = dis_load_chain loc x [] in s) in
if no_debug() then body
else DisEnv.scope loc "dis_load" (pp_expr x) pp_sym body

and dis_load_chain (loc: l) (x: expr) (ref: access_chain list): sym rws =
and dis_load_with_type (loc: l) (x: expr): (ty * sym) rws =
let body = dis_load_chain loc x [] in
if no_debug() then body
else DisEnv.scope loc "dis_load_with_type" (pp_expr x) (fun (t,s) -> pp_sym s) body

and dis_load_chain (loc: l) (x: expr) (ref: access_chain list): (ty * sym) rws =
(match x with
| Expr_Var(id) ->
let@ (var,local) = DisEnv.gets (LocalEnv.resolveGetVar loc id) in
Expand All @@ -759,12 +764,12 @@ and dis_load_chain (loc: l) (x: expr) (ref: access_chain list): sym rws =
(as a minor optimisation). *)
let@ () = DisEnv.if_ (ref = [])
(DisEnv.modify (LocalEnv.setVar loc var var')) in
DisEnv.pure var'
| v' -> DisEnv.pure (Val v')
DisEnv.pure (t', var')
| v' -> DisEnv.pure (t, Val v')
)
(* Variable is local with a symbolic value, should not expect a structure *)
| (t, Exp e) ->
if ref = [] then DisEnv.pure @@ Exp e
if ref = [] then DisEnv.pure @@ local
else unsupported loc "Local variable with dynamic structure"
)
| Expr_Field(e,f) -> dis_load_chain loc e (Field f::ref)
Expand Down Expand Up @@ -802,12 +807,13 @@ and dis_expr' (loc: l) (x: AST.expr): sym rws =
^ Utils.to_string (PP.pp_expr x)))
| Expr_Field(_, _) -> dis_load loc x
| Expr_Fields(e, fs) ->
let+ vs = DisEnv.traverse (fun f -> dis_load loc (Expr_Field(e,f))) fs in
sym_concat loc vs
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, 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
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
Expand Down
2 changes: 1 addition & 1 deletion libASL/eval.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1340,7 +1340,7 @@ let aarch64_asl_dir: string option =

let aarch64_asl_files: (string * string list) option =
let aarch64_file_load_order =
["mra_tools/arch/regs.asl"; "mra_tools/types.asl"; "mra_tools/arch/arch.asl"; "mra_tools/arch/arch_instrs.asl";
["mra_tools/arch/regs.asl"; "mra_tools/types.asl"; "mra_tools/arch/arch.asl"; "mra_tools/arch/arch_instrs.asl"; "mra_tools/arch/regs_access.asl";
"mra_tools/arch/arch_decode.asl"; "mra_tools/support/aes.asl"; "mra_tools/support/barriers.asl"; "mra_tools/support/debug.asl";
"mra_tools/support/feature.asl"; "mra_tools/support/hints.asl"; "mra_tools/support/interrupts.asl"; "mra_tools/support/memory.asl";
"mra_tools/support/stubs.asl"; "mra_tools/support/fetchdecode.asl"; "tests/override.asl"; "tests/override.prj"]
Expand Down
117 changes: 96 additions & 21 deletions libASL/symbolic.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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"
Expand All @@ -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) =
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -519,13 +599,11 @@ let sym_insert_bits loc (old_width: int) (old: sym) (lo: sym) (wd: sym) (v: sym)
| _ ->
failwith "sym_insert_bits: Width of inserted bitvector is unknown"

(** Append a list of bitvectors together
TODO: Will inject invalid widths due to unsafe sym_append_bits call.
*)
let sym_concat (loc: AST.l) (xs: sym list): sym =
let sym_concat (loc: AST.l) (xs: (int * sym) list): sym =
let body = fun (w,x) (yw,y) -> let b = sym_append_bits loc w yw x y in (w + yw,b) in
match xs with
| [] -> Val (VBits empty_bits)
| x::xs -> List.fold_left (sym_append_bits_unsafe loc) x xs
| x::xs -> let (_,r) = List.fold_left body x xs in r

(* Identify the bits in an expression that might be 1.
Represent these as a bitvector with 1s in their position, of width w. *)
Expand Down Expand Up @@ -572,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

Expand Down
Loading
Loading