diff --git a/dune b/dune index 47b46643..10c8b130 100644 --- a/dune +++ b/dune @@ -24,4 +24,4 @@ (alias (name default) - (deps (package asli))) + (deps (package asli) (alias install))) diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index d85f9bad..17585fbe 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -23,6 +23,9 @@ let is_lit f = let is_slice f = f = FIdent ("gen_slice", 0) +let is_merge_target f2 = + f2 = Offline_transform.rt_merge_branch + let is_gen_call f = let prefix = "gen_" in match f with @@ -228,15 +231,15 @@ module CopyProp = struct merge_st tst fst (* RunTime branch *) - | Stmt_Assign(LExpr_Tuple([LExpr_Var tv; LExpr_Var fv; LExpr_Var mv]), Expr_TApply(f, [], [c]), loc) when is_branch f -> + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], [c]), loc) when is_branch f -> (* Collect reads and process them all *) let deps = get_deps c in let st = read_vars deps st in (* Push the merge point *) - push_context mv st + push_context v st (* Context switch *) - | Stmt_TCall(f, [], [Expr_Var i], loc) when is_context_switch f -> + | Stmt_TCall(f, [], [Expr_TApply(f2, [], [Expr_Var i])], loc) when is_context_switch f && is_merge_target f2 -> let top = peek_context st in if i = top then pop_context st else st @@ -286,3 +289,23 @@ module CopyProp = struct Asl_visitor.visit_stmts v body end + +module DeadContextSwitch = struct + (* Backwards walk to reduce consecutive context switches. + Could be extended to any context switches with no rt gen operations between, + but this pattern doesn't seem to show up. *) + + let rec walk_stmts s dead = + List.fold_right (fun s (acc,dead) -> + match s with + | Stmt_TCall (f, _, _, _) when is_context_switch f && dead -> (acc,dead) + | Stmt_TCall (f, _, _, _) when is_context_switch f -> (s::acc,true) + | Stmt_If(c, t, [], f, loc) -> + let (t,dead) = walk_stmts t dead in + let (f,dead') = walk_stmts f dead in + (Stmt_If(c, t, [], f, loc)::acc, dead && dead') + | _ -> (s::acc,false) + ) s ([],dead) + + let run fn body = let (s,_) = walk_stmts body false in s +end diff --git a/libASL/offline_transform.ml b/libASL/offline_transform.ml index 9276243a..0bdaaaf6 100644 --- a/libASL/offline_transform.ml +++ b/libASL/offline_transform.ml @@ -715,23 +715,20 @@ let gen_fresh_var loc ty = let+ _ = gen_var_decl loc ty i in i +let rt_true_branch = FIdent("true_branch", 0) +let rt_false_branch = FIdent("false_branch", 0) +let rt_merge_branch = FIdent("merge_branch", 0) + (* Generate a branch in the runtime program, with some way to refer to its targets and merge point *) let gen_branch loc c = - let@ tl = get_fresh_name in - let@ tf = get_fresh_name in - let@ tm = get_fresh_name in - let lexpr = LExpr_Tuple ( List.map (fun v -> LExpr_Var v) [tl;tf;tm] ) in - let+ _ = write [ - Stmt_VarDeclsNoInit( rt_label_ty, [tl], loc); - Stmt_VarDeclsNoInit( rt_label_ty, [tf], loc); - Stmt_VarDeclsNoInit( rt_label_ty, [tm], loc); - Stmt_Assign(lexpr, Expr_TApply(rt_gen_branch, [], [c]), loc) - ] in - (tl,tf,tm) + let@ res = get_fresh_name in + let v = Expr_Var res in + let+ _ = write [Stmt_ConstDecl( rt_label_ty, res, Expr_TApply(rt_gen_branch, [], [c]), loc) ] in + (Expr_TApply(rt_true_branch, [], [v]),Expr_TApply(rt_false_branch,[],[v]),Expr_TApply(rt_merge_branch,[],[v])) (* Switch the implicit context to one produced by gen_branch *) let switch_context loc t = - write [Stmt_TCall(rt_switch_context, [], [Expr_Var t], loc)] + write [Stmt_TCall(rt_switch_context, [], [t], loc)] (* Generate a variable store/load *) let gen_var_store loc v e = diff --git a/libASL/req_analysis.ml b/libASL/req_analysis.ml index e76c81b0..10ede486 100644 --- a/libASL/req_analysis.ml +++ b/libASL/req_analysis.ml @@ -68,6 +68,10 @@ let wrap f = fun s -> match f s with | Either.Left r -> Either.Left (s,[],r) | Either.Right e -> Either.Right e +let wrapl f = fun s -> + match f s with + | Either.Left (s,w,r) -> Either.Left (s,[],(w,r)) + | Either.Right e -> Either.Right e let write l = fun s -> Either.Left (s,[l],()) let writel l = fun s -> @@ -391,7 +395,17 @@ let contains_req_assign s : bool wrm = | _ -> pure false) s in List.mem true search -let fix_stmt fid s = +let rec process_alts fid v loc alts d = + match alts with + | (Alt_Alt(p,oc,b))::alts -> + let e = Expr_In (v, Pat_Set p) in + let e = match oc with Some c -> Expr_TApply (FIdent ("and_bool", 0), [], [e;c]) | _ -> e in + let@ (b,_) = wrapl (fix_stmts fid b) in + let+ acc = process_alts fid v loc alts d in + [Stmt_If(e, b, [], acc, loc)] + | _ -> pure d + +and fix_stmt fid s = match s with | Stmt_VarDecl(ty, v, e, loc) | Stmt_ConstDecl(ty, v, e, loc) -> @@ -403,6 +417,16 @@ let fix_stmt fid s = | _, Some vals -> Printf.printf " %s: Splitting %s into %d values\n" (name_of_FIdent fid)(pp_stmt s) (List.length vals); let@ _ = write (Stmt_VarDeclsNoInit(ty, [v], loc)) in + write (List.fold_right (fun (test,expr) acc -> + Stmt_If(test, [Stmt_Assign(LExpr_Var v, expr, loc)], [], [acc], loc)) vals (Stmt_Throw (Ident ("UNREACHABLE"), loc)))) + | Stmt_Assign(LExpr_Var v, e, loc) -> + let@ r = get_req v in + let vals = enumerate e in + (match r, vals with + | NoReq, _ + | _, None -> write s + | _, Some vals -> + Printf.printf " %s: Splitting assign %s into %d values\n" (name_of_FIdent fid)(pp_stmt s) (List.length vals); write (List.fold_right (fun (test,expr) acc -> Stmt_If(test, [Stmt_Assign(LExpr_Var v, expr, loc)], [], [acc], loc)) vals (Stmt_Throw (Ident ("UNREACHABLE"), loc)))) | Stmt_Case(v, alts, None, loc) -> @@ -410,22 +434,18 @@ let fix_stmt fid s = if not b then write s else (Printf.printf " %s: Splitting %s into %d values\n" (name_of_FIdent fid) (pp_stmt s) (List.length alts); - write (List.fold_left (fun acc (Alt_Alt(p,oc,b)) -> - let e = Expr_In (v, Pat_Set p) in - let e = match oc with Some c -> Expr_TApply (FIdent ("and_bool", 0), [], [e;c]) | _ -> e in - Stmt_If(e, b, [], [acc], loc)) (Stmt_Throw (Ident ("UNREACHABLE"), loc)) alts)) + let@ r = process_alts fid v loc alts [Stmt_Throw (Ident ("UNREACHABLE"), loc)] in + writel r) | Stmt_Case(v, alts, Some d, loc) -> let@ b = contains_req_assign (List.flatten (List.map (function Alt_Alt(p,oc,b) -> b) alts)) in if not b then write s else (Printf.printf " %s: Splitting %s into %d values\n" (name_of_FIdent fid) (pp_stmt s) (List.length alts + 1); - writel (List.fold_left (fun acc (Alt_Alt(p,oc,b)) -> - let e = Expr_In (v, Pat_Set p) in - let e = match oc with Some c -> Expr_TApply (FIdent ("and_bool", 0), [], [e;c]) | _ -> e in - [Stmt_If(e, b, [], acc, loc)]) (d) alts)) + let@ r = process_alts fid v loc alts d in + writel r) | _ -> write s -let fix_stmts fid s = +and fix_stmts fid s = let+ _ = traverse (fix_stmt fid) s in () diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index b73d25c3..dcd94da1 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -34,10 +34,6 @@ let unsupported_set = IdentSet.of_list [ (* Problematic instruction encoding names, due to various disassembly issues *) let problematic_enc = [ - (* >10k lines due to unrolling/splitting *) - "aarch64_memory_vector_multiple_no_wb"; - "aarch64_memory_vector_multiple_post_inc"; - (* Need to extend RemoveUnsupported to remove all undesirable global variables & fields *) "aarch64_system_register_system"; "aarch64_system_register_cpsr"; @@ -372,6 +368,7 @@ let run iset pat env = Printf.printf "Stages 7-8: Offline Transform\n"; let offline_fns = Offline_transform.run fns env in let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.CopyProp.run k)) offline_fns in + let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.DeadContextSwitch.run k)) offline_fns in let dsig = fnsig_upd_body (DecoderCleanup.run (unsupported_inst tests offline_fns)) dsig in let dsig = fnsig_upd_body (Transforms.RemoveUnused.remove_unused IdentSet.empty) dsig in Printf.printf "\n"; diff --git a/libASL/transforms.ml b/libASL/transforms.ml index db910855..922687a2 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -121,13 +121,14 @@ let infer_type (e: expr): ty option = (** Remove variables which are unused at the end of the statement list. *) module RemoveUnused = struct - let rec remove_unused (globals: IdentSet.t) xs = (remove_unused' globals xs) + let rec remove_unused (globals: IdentSet.t) xs = fst (remove_unused' globals IdentSet.empty xs) - and remove_unused' (used: IdentSet.t) (xs: stmt list): (stmt list) = - fst @@ List.fold_right (fun stmt (acc, used) -> + and remove_unused' globals (used: IdentSet.t) (xs: stmt list): (stmt list * IdentSet.t) = + List.fold_right (fun stmt (acc, used) -> let pass = (acc, used) and emit (s: stmt) = (s::acc, IdentSet.union used (fv_stmt s)) + and halt (s: stmt) = ([stmt], IdentSet.empty) in match stmt with @@ -146,19 +147,34 @@ module RemoveUnused = struct else pass | Stmt_Assign(le, r, loc) -> let lvs = assigned_vars_of_stmts [stmt] in - if not (IdentSet.disjoint lvs used) + if not (IdentSet.disjoint lvs used) || not (IdentSet.disjoint lvs globals) then emit stmt else pass + + (* Skip if structure if possible - often seen in decode tests *) + | Stmt_If(Expr_Var (Ident "TRUE"), tstmts, elsif, fstmts, loc) -> + let (tstmts',tused) = remove_unused' globals used tstmts in + (tstmts'@acc,tused) + | Stmt_If(c, tstmts, elsif, fstmts, loc) -> - let tstmts' = remove_unused' used tstmts in - let fstmts' = remove_unused' used fstmts in + let (tstmts',tused) = remove_unused' globals used tstmts in + let (fstmts',fused) = remove_unused' globals used fstmts in let elsif' = List.map (fun (S_Elsif_Cond (c,ss)) -> - S_Elsif_Cond (c, remove_unused' used ss)) + let (b, bused) = remove_unused' globals used ss in + let bused = IdentSet.union bused (fv_expr c) in + (S_Elsif_Cond (c,b), bused)) elsif in + let used = List.fold_right (fun (_,u) -> IdentSet.union u) elsif' (IdentSet.union tused fused) in + let used = IdentSet.union used (fv_expr c) in (match (tstmts',fstmts',elsif') with | [], [], [] -> pass - | _, _, _ -> emit (Stmt_If(c, tstmts', elsif', fstmts', loc))) + | _, _, _ -> (Stmt_If(c, tstmts', List.map fst elsif', fstmts', loc)::acc,used)) + + (* Unreachable points *) + | Stmt_Assert (Expr_Var (Ident "FALSE"), _) + | Stmt_Throw _ -> halt stmt + | x -> emit x ) xs ([], used) diff --git a/offline-build.sh b/offline-build.sh deleted file mode 100755 index 461f8bef..00000000 --- a/offline-build.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash - -echo ':gen A64 aarch64_.+' | dune exec asli -dune build diff --git a/offline-coverage.sh b/offline-coverage.sh deleted file mode 100755 index 99fac0e6..00000000 --- a/offline-coverage.sh +++ /dev/null @@ -1,64 +0,0 @@ -#!/bin/bash - -# performs regression testing based on :coverage of particular groups of instructions -INSTRUCTION_GROUPS='' -INSTRUCTION_GROUPS+='aarch64_integer.+' -INSTRUCTION_GROUPS+=' aarch64_branch.+' -INSTRUCTION_GROUPS+=' aarch64_float_.+' -INSTRUCTION_GROUPS+=' aarch64_vector_.+' -INSTRUCTION_GROUPS+=' aarch64_memory_.+' - -COVERAGE_DIR="./tests/coverage" -COVERAGE_TEMP=$(mktemp -d) - -MODE="" -if [[ "$1" == "test" ]]; then - MODE=test -elif [[ "$1" == "update" ]]; then - MODE=update -else - echo "requires 'test' or 'update' as first argument." - exit 1 -fi - -mkdir -p "$COVERAGE_DIR" -mkdir -p "$COVERAGE_TEMP" - -asl_dir="$(dune exec asli -- --aarch64-dir)" - -tar xf encodings.tar.gz || exit 1 - -RESULT=0 -for inst in $INSTRUCTION_GROUPS; do - fname="$(tr -c '[:alnum:]_' _ <<< "$inst")" - new="$COVERAGE_TEMP/$fname" - diff="$COVERAGE_TEMP/$fname.diff" - echo "::group::$inst" - echo "$new" - time dune exec asloff-coverage "$inst" > "$new" - old="$COVERAGE_DIR/$fname" - - sed -i "s#$asl_dir#.#g" "$new" - - if [[ $MODE == update ]]; then - echo "overwriting coverage results with updated results." - cp -v "$new" "$old" - else - echo "testing coverage with previous results." - diff -Nu "$old" "$new" > "$diff" - diff -Nu --color=auto "$old" "$new" - RESULT=$(($RESULT + $?)) - fi - echo "::endgroup::" - echo -done - -if [[ -z "$GITHUB_OUTPUT" ]]; then - GITHUB_OUTPUT=/dev/null -fi - -echo "OUTPUT=$COVERAGE_TEMP" >> $GITHUB_OUTPUT - - -exit $RESULT - diff --git a/offlineASL/utils.ml b/offlineASL/utils.ml index 3be4bb2d..6ead03b3 100644 --- a/offlineASL/utils.ml +++ b/offlineASL/utils.ml @@ -121,6 +121,10 @@ let f_gen_branch cond = Expr_LitInt (string_of_int merge)], loc)); (true_branch, false_branch, merge) +let f_true_branch (a,_,_) = a +let f_false_branch (_,b,_) = b +let f_merge_branch (_,_,c) = c + let undefined () = Expr_Tuple [] (* Runtime assert *) diff --git a/tests/coverage/dune b/tests/coverage/dune index c53c36aa..718b8ba1 100644 --- a/tests/coverage/dune +++ b/tests/coverage/dune @@ -12,6 +12,10 @@ (deps (package asli) ./encodings) (action (copy ./run.sh ./run))) +(rule + (deps (package asli) ./encodings) + (action (copy ./off_run.sh ./off_run))) + (rule (with-stdout-to cov_integer (run ./run "aarch64_integer.+"))) (rule (with-stdout-to cov_branch (run ./run "aarch64_branch.+"))) (rule (with-stdout-to cov_float (run ./run "aarch64_float_.+"))) @@ -25,4 +29,17 @@ (rule (alias coverage) (action (diff ./aarch64_vector1 cov_vector1))) (rule (alias coverage) (action (diff ./aarch64_vector2 cov_vector2))) (rule (alias coverage) (action (diff ./aarch64_memory cov_memory))) - + +(rule (with-stdout-to off_cov_integer (run ./off_run "aarch64_integer.+"))) +(rule (with-stdout-to off_cov_branch (run ./off_run "aarch64_branch.+"))) +(rule (with-stdout-to off_cov_float (run ./off_run "aarch64_float_.+"))) +(rule (with-stdout-to off_cov_vector1 (run ./off_run "aarch64_vector_arithmetic_binary.+"))) +(rule (with-stdout-to off_cov_vector2 (run ./off_run "aarch64_vector_(?!arithmetic_binary).+"))) +(rule (with-stdout-to off_cov_memory (run ./off_run "aarch64_memory_.+"))) + +(rule (alias offline-coverage) (action (diff ./aarch64_integer off_cov_integer))) +(rule (alias offline-coverage) (action (diff ./aarch64_branch off_cov_branch))) +(rule (alias offline-coverage) (action (diff ./aarch64_float off_cov_float))) +(rule (alias offline-coverage) (action (diff ./aarch64_vector1 off_cov_vector1))) +(rule (alias offline-coverage) (action (diff ./aarch64_vector2 off_cov_vector2))) +(rule (alias offline-coverage) (action (diff ./aarch64_memory off_cov_memory))) diff --git a/tests/coverage/off_run.sh b/tests/coverage/off_run.sh new file mode 100755 index 00000000..580ba203 --- /dev/null +++ b/tests/coverage/off_run.sh @@ -0,0 +1,8 @@ +#!/bin/bash -e + +pattern="${1:?requires regex pattern as first argument}" + +asl_dir="$(asli --aarch64-dir)" +output="$(asloff-coverage "$pattern")" + +echo "$output" | sed "s#$asl_dir#.#g"