From 349733842a9cc1eb3c239bdc26f692af87c21ab0 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 21 Oct 2025 19:05:56 -0700 Subject: [PATCH 1/7] XPRLIB: expand more multiplication expressions --- CodeHawk/CH/xprlib/xprUtil.ml | 186 +++++++++++++++++++++++----------- CodeHawk/CH/xprlib/xprt.ml | 7 ++ CodeHawk/CH/xprlib/xprt.mli | 2 + 3 files changed, 134 insertions(+), 61 deletions(-) diff --git a/CodeHawk/CH/xprlib/xprUtil.ml b/CodeHawk/CH/xprlib/xprUtil.ml index 124ceeeb..fe1ba310 100644 --- a/CodeHawk/CH/xprlib/xprUtil.ml +++ b/CodeHawk/CH/xprlib/xprUtil.ml @@ -3,7 +3,7 @@ Author: Henny Sipma ------------------------------------------------------------------------------ The MIT License (MIT) - + Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma Copyright (c) 2021-2022 Aarno Labs LLC @@ -14,10 +14,10 @@ to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: - + The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. - + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE @@ -39,22 +39,23 @@ open CHNestedCommands (* xprlib *) open Xprt -open XprTypes +open XprTypes open Xsimplify (* =============================================================================== Conversion of xpr_t to engine expressions + code - =============================================================================== + =============================================================================== *) - + let xconst_2_numexpr (reqN:tmp_provider_t) (_reqC:cst_provider_t) (c:xcst_t):code_num_t = match c with | IntConst num -> (make_nested_nop (), NUM num) | BoolConst b -> - let num = if b then numerical_one else numerical_zero in + let num = if b then numerical_one else numerical_zero in (make_nested_nop (), NUM num) | _ -> (make_nested_nop (), NUM_VAR (reqN ())) + let xconst_2_boolexpr (_reqN:tmp_provider_t) (_reqC:cst_provider_t) (c:xcst_t):code_bool_t = let bxpr = match c with | BoolConst b -> if b then TRUE else FALSE @@ -62,20 +63,22 @@ let xconst_2_boolexpr (_reqN:tmp_provider_t) (_reqC:cst_provider_t) (c:xcst_t):c | _ -> RANDOM in (make_nested_nop (), bxpr) + let rec xpr_2_numexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (xpr:xpr_t):code_num_t = match xpr with XVar v -> (make_nested_nop (), NUM_VAR v) | XConst c -> xconst_2_numexpr reqN reqC c | XOp (op, l) -> xop_2_numexpr reqN reqC op l | XAttr _ -> (make_nested_nop (), NUM_VAR (reqN ())) - + + and xop_2_numexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (op:xop_t) (l:xpr_t list):code_num_t = match (op,l) with - | (_, []) -> - raise (CHFailure (LBLOCK [ STR "Empty operand list in xop_2_numexpr" ])) + | (_, []) -> + raise (CHFailure (LBLOCK [STR "Empty operand list in xop_2_numexpr"])) | (XNeg, [e]) -> - xpr_2_numexpr reqN reqC (XOp (XMinus, [ zero_constant_expr ; e ])) + xpr_2_numexpr reqN reqC (XOp (XMinus, [zero_constant_expr; e])) | (XLNot, [_e]) | (XBNot, [_e]) @@ -83,30 +86,69 @@ and xop_2_numexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (op:xop_t) (l:xpr_ | (XXlsh, [_e]) -> (make_nested_nop (), NUM_VAR (reqN ())) - | (XMult, [ XConst (IntConst n) ; XVar v ]) - | (XMult, [ XVar v ; XConst (IntConst n) ]) when n#equal (mkNumerical 2) -> + | (XMult, [XConst (IntConst n); XVar v]) + | (XMult, [XVar v; XConst (IntConst n)]) when n#equal (mkNumerical 2) -> (make_nested_nop () , PLUS (v, v)) - | (XMult, [ XConst (IntConst n) ; XVar v ]) - | (XMult, [ XVar v ; XConst (IntConst n) ]) when n#equal (mkNumerical 4) -> + | (XMult, [XConst (IntConst n); XVar v]) + | (XMult, [XVar v; XConst (IntConst n)]) when n#equal (mkNumerical 4) -> let tmp = reqN () in let asgn1 = make_nested_cmd (ASSIGN_NUM (tmp, PLUS (v,v))) in let asgn2 = make_nested_cmd (ASSIGN_NUM (tmp, PLUS (tmp,tmp))) in - (make_nested_cmd_block [ asgn1 ; asgn2 ], NUM_VAR tmp) + (make_nested_cmd_block [asgn1; asgn2], NUM_VAR tmp) - | (XMult, [ XConst (IntConst n) ; XVar v ]) - | (XMult, [ XVar v ; XConst (IntConst n) ]) when n#equal (mkNumerical 8) -> + | (XMult, [XConst (IntConst n); XVar v]) + | (XMult, [XVar v; XConst (IntConst n)]) when n#equal (mkNumerical 8) -> let tmp1 = reqN () in let tmp2 = reqN () in let asgn1 = make_nested_cmd (ASSIGN_NUM (tmp1, PLUS (v,v))) in let asgn2 = make_nested_cmd (ASSIGN_NUM (tmp2, PLUS (tmp1,tmp1))) in let asgn3 = make_nested_cmd (ASSIGN_NUM (tmp2, PLUS (tmp2,tmp2))) in - (make_nested_cmd_block [ asgn1 ; asgn2 ; asgn3 ], NUM_VAR tmp2) - - | (XPlus, [ e1 ; e2 ]) - | (XMinus, [ e1 ; e2 ]) - | (XMult, [ e1 ; e2 ]) - | (XDiv, [ e1 ; e2 ]) -> + (make_nested_cmd_block [asgn1; asgn2; asgn3], NUM_VAR tmp2) + + | (XMult, [XConst (IntConst n); XVar v]) + | (XMult, [XVar v; XConst (IntConst n)]) when n#equal (mkNumerical 16) -> + let tmp1 = reqN () in + let tmp2 = reqN () in + let tmp3 = reqN () in + let asgn1 = make_nested_cmd (ASSIGN_NUM (tmp1, PLUS (v,v))) in + let asgn2 = make_nested_cmd (ASSIGN_NUM (tmp2, PLUS (tmp1,tmp1))) in + let asgn3 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp2,tmp2))) in + let asgn4 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp3,tmp3))) in + (make_nested_cmd_block [asgn1; asgn2; asgn3; asgn4], NUM_VAR tmp3) + + | (XMult, [XConst (IntConst n); XVar v]) + | (XMult, [XVar v; XConst (IntConst n)]) when n#equal (mkNumerical 16) -> + let tmp1 = reqN () in + let tmp2 = reqN () in + let tmp3 = reqN () in + let tmp4 = reqN () in + let asgn1 = make_nested_cmd (ASSIGN_NUM (tmp1, PLUS (v,v))) in + let asgn2 = make_nested_cmd (ASSIGN_NUM (tmp2, PLUS (tmp1,tmp1))) in + let asgn3 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp2,tmp2))) in + let asgn4 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp3,tmp3))) in + let asgn5 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp4,tmp4))) in + (make_nested_cmd_block [asgn1; asgn2; asgn3; asgn4; asgn5], NUM_VAR tmp4) + + | (XMult, [XConst (IntConst n); XVar v]) + | (XMult, [XVar v; XConst (IntConst n)]) when n#equal (mkNumerical 32) -> + let tmp1 = reqN () in + let tmp2 = reqN () in + let tmp3 = reqN () in + let tmp4 = reqN () in + let tmp5 = reqN () in + let asgn1 = make_nested_cmd (ASSIGN_NUM (tmp1, PLUS (v,v))) in + let asgn2 = make_nested_cmd (ASSIGN_NUM (tmp2, PLUS (tmp1,tmp1))) in + let asgn3 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp2,tmp2))) in + let asgn4 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp3,tmp3))) in + let asgn5 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp4,tmp4))) in + let asgn6 = make_nested_cmd (ASSIGN_NUM (tmp3, PLUS (tmp5,tmp5))) in + (make_nested_cmd_block [asgn1; asgn2; asgn3; asgn4; asgn5; asgn6], NUM_VAR tmp5) + + | (XPlus, [e1; e2]) + | (XMinus, [e1; e2]) + | (XMult, [e1; e2]) + | (XDiv, [e1; e2]) -> let (c1,r1) = xpr_2_numvar reqN reqC e1 in let (c2,r2) = xpr_2_numvar reqN reqC e2 in let num_expr = @@ -117,54 +159,58 @@ and xop_2_numexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (op:xop_t) (l:xpr_ | XDiv -> DIV (r1, r2) | _ -> failwith "Unexpected operator in xop_2_numexpr" in - (make_nested_cmd_block [ c1 ; c2 ], num_expr) + (make_nested_cmd_block [c1; c2], num_expr) - | (XMod, [ XConst (IntConst n1) ; XConst (IntConst n2) ]) -> + | (XMod, [XConst (IntConst n1); XConst (IntConst n2)]) -> (make_nested_nop (), NUM (n1#modulo n2)) - | (XNumRange, [e1 ; e2]) -> + | (XNumRange, [e1; e2]) -> let tmp = reqN () in - let lb = XOp (XGe, [ XVar tmp ; e1 ]) in - let ub = XOp (XLe, [ XVar tmp ; e2 ]) in + let lb = XOp (XGe, [XVar tmp; e1]) in + let ub = XOp (XLe, [XVar tmp; e2]) in let (lbc,lbe) = xpr_2_boolexpr reqN reqC lb in let (ubc,ube) = xpr_2_boolexpr reqN reqC ub in let lba = make_nested_cmd (ASSERT lbe) in let uba = make_nested_cmd (ASSERT ube) in - let code = make_nested_cmd_block [ lbc ; ubc ; lba ; uba ] in + let code = make_nested_cmd_block [lbc; ubc; lba; uba] in (code, NUM_VAR tmp) | _ -> (make_nested_nop (), NUM_VAR (reqN ())) + and xpr_2_numvar (reqN:tmp_provider_t) (reqC:cst_provider_t) (xpr:xpr_t):code_var_t = match xpr with | XVar v -> (make_nested_nop (), v) - | XConst (IntConst n) -> + | XConst (IntConst n) -> let v = reqC n in (make_nested_nop (), v) | _ -> let (c,r) = xpr_2_numexpr reqN reqC xpr in let tmp = reqN () in let asgn = make_nested_cmd (ASSIGN_NUM (tmp, r)) in - let code = make_nested_cmd_block [ c ; asgn ] in + let code = make_nested_cmd_block [c; asgn] in (code, tmp) + and xpr_2_boolexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (xpr:xpr_t):code_bool_t = match xpr with | XVar v -> xvar_2_boolexpr reqN reqC v | XConst c -> xconst_2_boolexpr reqN reqC c | XOp (op, l) -> xop_2_boolexpr reqN reqC op l | _ -> - raise (CHFailure (LBLOCK [ STR "Unexpected expression in expr_2_boolexpr" ])) + raise (CHFailure (LBLOCK [STR "Unexpected expression in expr_2_boolexpr"])) + and xvar_2_boolexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (v:variable_t):code_bool_t = let bxpr = if v#isNumerical then - XOp (XNe, [XVar v ; zero_constant_expr ]) + XOp (XNe, [XVar v; zero_constant_expr]) else XConst XRandom in xpr_2_boolexpr reqN reqC bxpr + and xop_2_boolexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (op:xop_t) (l:xpr_t list) = let default = (make_nested_nop (), RANDOM) in match (op, l) with @@ -172,17 +218,17 @@ and xop_2_boolexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (op:xop_t) (l:xpr raise (CHFailure (STR "Empty operand list in xop_2_boolexpr")) | (XNeg, [_e]) -> - xpr_2_boolexpr reqN reqC (XOp (XNe, [ XOp (op, l) ; zero_constant_expr])) + xpr_2_boolexpr reqN reqC (XOp (XNe, [XOp (op, l); zero_constant_expr])) | (XLNot, [_e]) | (XBNot, [_e]) | (XXlsb, [_e]) | (XXlsh, [_e]) -> default - | (XDisjoint, [XVar v ; XConst (SymSet l) ]) -> + | (XDisjoint, [XVar v; XConst (SymSet l)]) -> (make_nested_nop (), DISJOINT (v,l)) - | (XSubset, [ XVar v; XConst (SymSet l) ]) -> + | (XSubset, [XVar v; XConst (SymSet l)]) -> (make_nested_nop (), SUBSET (v, l)) | (XPlus, _) @@ -218,7 +264,7 @@ and xop_2_boolexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (op:xop_t) (l:xpr in (make_nested_cmd_block [c1; c2], bxpr) - | _ -> + | _ -> default @@ -226,14 +272,17 @@ let xpr2numexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (xpr:xpr_t):code_num let (_, sim_expr) = simplify_expr xpr in xpr_2_numexpr reqN reqC sim_expr + let xpr2numvar (reqN:tmp_provider_t) (reqC:cst_provider_t) (xpr:xpr_t):code_var_t = let (_, sim_expr) = simplify_expr xpr in xpr_2_numvar reqN reqC sim_expr + let xpr2boolexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) (xpr:xpr_t):code_bool_t = let (_, sim_expr) = simplify_expr xpr in xpr_2_boolexpr reqN reqC sim_expr + let xpr_to_numexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) @@ -241,6 +290,7 @@ let xpr_to_numexpr let (c,e) = xpr2numexpr reqN reqC xpr in (nested_cmd_2_cmds c, e) + let xpr_to_numvar (reqN:tmp_provider_t) (reqC:cst_provider_t) @@ -248,6 +298,7 @@ let xpr_to_numvar let (c,v) = xpr2numvar reqN reqC xpr in (nested_cmd_2_cmds c, v) + let xpr_to_boolexpr (reqN:tmp_provider_t) (reqC:cst_provider_t) @@ -284,6 +335,7 @@ let occurs_check (var:variable_t) (x:xpr_t) = | _ -> false in aux x + (* PEPR Conversion *) let pepr_parameter_expr_to_xpr @@ -291,34 +343,42 @@ let pepr_parameter_expr_to_xpr (coeffs:coeff_vector_int) (n:numerical_t) = let factors = coeffs#get_pairs in - simplify_xpr (List.fold_left (fun acc (i,c) -> - let v = (params#nth i)#get_variable in - XOp (XPlus, [ XOp (XMult, [ XVar v ; num_constant_expr c ]) ; acc ])) - (num_constant_expr n) factors) + simplify_xpr + (List.fold_left (fun acc (i,c) -> + let v = (params#nth i)#get_variable in + XOp (XPlus, [XOp (XMult, [XVar v; num_constant_expr c]); acc])) + (num_constant_expr n) factors) + let pex_to_xpr (params:pepr_params_int) (x:pex_int) = if x#is_number then num_constant_expr x#get_number else - pepr_parameter_expr_to_xpr params x#get_k x#get_n + pepr_parameter_expr_to_xpr params x#get_k x#get_n + let pex_set_to_xpr_list (params:pepr_params_int) (s:pex_set_int):xpr_t list = List.map (pex_to_xpr params) s#get_s + let pex_pset_to_xpr_list_list (params:pepr_params_int) (p:pex_pset_int):xpr_t list list = List.map (pex_set_to_xpr_list params) p#get_p + (* disjunction of conjunction *) -let pepr_bound_to_xpr_list_list (params:pepr_params_int) (b:pepr_bounds_t):xpr_t list list = +let pepr_bound_to_xpr_list_list + (params:pepr_params_int) (b:pepr_bounds_t):xpr_t list list = match b with - | XTOP -> [ [ random_constant_expr ] ] + | XTOP -> [[random_constant_expr]] | XPSET x -> pex_pset_to_xpr_list_list params x - -let get_pepr_range_xprs (params:pepr_params_int) (range:pepr_range_int):pepr_xpr_extract = + + +let get_pepr_range_xprs + (params:pepr_params_int) (range:pepr_range_int):pepr_xpr_extract = let result = { - pepr_n = None ; - pepr_i = None ; - pepr_equalities = [] ; + pepr_n = None; + pepr_i = None; + pepr_equalities = []; pepr_bounds = [] } in let (range,result) = @@ -332,26 +392,30 @@ let get_pepr_range_xprs (params:pepr_params_int) (range:pepr_range_int):pepr_xpr let (range,result) = List.fold_left (fun (ran,_res) (k,n) -> (ran#remove_equality k n, - { result with pepr_equalities = - (pepr_parameter_expr_to_xpr params k n) :: result.pepr_equalities} )) - (range, result) range#parameter_exprs in + { result with + pepr_equalities = + (pepr_parameter_expr_to_xpr params k n) :: result.pepr_equalities} )) + (range, result) range#parameter_exprs in let result = match range#get_min#get_bound with | XTOP -> result | b -> { result with - pepr_bounds = (LB,pepr_bound_to_xpr_list_list params b) :: result.pepr_bounds } in + pepr_bounds = + (LB,pepr_bound_to_xpr_list_list params b) :: result.pepr_bounds } in match range#get_max#get_bound with | XTOP -> result | b -> { result with pepr_bounds = (UB,pepr_bound_to_xpr_list_list params b) :: result.pepr_bounds } -let get_pepr_dependency_xprs (params:pepr_params_int) (s:param_constraint_set_int):xpr_t list = + +let get_pepr_dependency_xprs + (params:pepr_params_int) (s:param_constraint_set_int):xpr_t list = List.map (fun x -> let factors = x#get_k#get_pairs in let xpr = - simplify_xpr (List.fold_left (fun acc (i,c) -> - let v = (params#nth i)#get_variable in - XOp (XPlus, [ XOp (XMult, [ XVar v ; num_constant_expr c ]) ; acc ])) - (num_constant_expr x#get_n) factors) in - XOp (XGe, [ xpr ; zero_constant_expr ])) s#get_s - + simplify_xpr + (List.fold_left (fun acc (i,c) -> + let v = (params#nth i)#get_variable in + XOp (XPlus, [XOp (XMult, [XVar v; num_constant_expr c]); acc])) + (num_constant_expr x#get_n) factors) in + XOp (XGe, [xpr; zero_constant_expr])) s#get_s diff --git a/CodeHawk/CH/xprlib/xprt.ml b/CodeHawk/CH/xprlib/xprt.ml index 410b7add..a6886d20 100644 --- a/CodeHawk/CH/xprlib/xprt.ml +++ b/CodeHawk/CH/xprlib/xprt.ml @@ -254,6 +254,13 @@ let vars_in_expr (expr:xpr_t):VariableCollections.set_t = let variables_in_expr (x:xpr_t):variable_t list = (vars_in_expr x)#toList +let loop_counters_in_expr (x: xpr_t): variable_t list = + List.filter (fun v -> + match v#getType with + | NUM_LOOP_COUNTER_TYPE -> true + | _ -> false) (variables_in_expr x) + + let vars_in_expr_list (exprs:xpr_t list) = let s = new VariableCollections.set_t in begin diff --git a/CodeHawk/CH/xprlib/xprt.mli b/CodeHawk/CH/xprlib/xprt.mli index 03a2f321..83a93941 100644 --- a/CodeHawk/CH/xprlib/xprt.mli +++ b/CodeHawk/CH/xprlib/xprt.mli @@ -53,6 +53,8 @@ val get_disjuncts: xpr_t -> xpr_t list val variables_in_expr: xpr_t -> variable_t list val vars_in_expr_list: xpr_t list -> variable_t list +val loop_counters_in_expr: xpr_t -> variable_t list + val is_zero: xpr_t -> bool val is_one: xpr_t -> bool val is_intconst: xpr_t -> bool From e45644f7ec5acf9fdbe7bb0c1d1f5e0e9009d127 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 21 Oct 2025 19:12:46 -0700 Subject: [PATCH 2/7] CHB:ARM: analyze with loop counters --- CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.ml | 2 +- CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml | 10 ++++++++++ CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml | 2 +- CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml | 2 +- CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 2 ++ CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml | 2 +- 6 files changed, 16 insertions(+), 4 deletions(-) diff --git a/CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.ml b/CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.ml index 430c46c6..5e0be0cb 100644 --- a/CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.ml +++ b/CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.ml @@ -91,7 +91,7 @@ let analyze_procedure_with_linear_equalities begin analysis_setup#addLinearEqualities; analysis_setup#setOpSemantics (default_opsemantics "karr"); - analysis_setup#analyze_procedure system proc + analysis_setup#analyze_procedure system ~do_loop_counters:true proc end let analyze_procedure_with_intervals (proc:procedure_int) (system:system_int) = diff --git a/CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml b/CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml index 74677176..c2f4eab9 100644 --- a/CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml +++ b/CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml @@ -232,6 +232,16 @@ let extract_external_value_equalities let extract_relational_facts finfo iaddr domain = + let vars = domain#observer#getObservedVariables in + let lcs = + List.filter (fun v -> match v#getType with NUM_LOOP_COUNTER_TYPE -> true | _ -> false) + vars in + let _ = + ch_diagnostics_log#add + "project out loopcounters" + (LBLOCK [STR iaddr; STR ": "; + pretty_print_list lcs (fun v -> v#toPretty) "[" ", " "]"]) in + let domain = domain#projectOut lcs in let constraints = domain#observer#getNumericalConstraints ~variables:None () in List.iter (finfo#finv#add_lineq iaddr) constraints diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml index d3f96775..8d3c9d39 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml @@ -726,7 +726,7 @@ object (self:'a) | ARMImmediate _ -> let num = self#to_numerical in (try - num#toInt >= 0 && num#toInt < 5 + num#toInt >= 0 && num#toInt < 7 with | _ -> false) | _ -> false diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index f869ca48..d7d5c89a 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -159,7 +159,7 @@ object (self) () in let rewrite_expr ?(restrict:int option) (x: xpr_t): xpr_t = try - let xpr = floc#inv#rewrite_expr x in + let xpr = floc#inv#rewrite_expr ~loopcounter:true x in let xpr = simplify_xpr xpr in let xpr = let vars = variables_in_expr xpr in diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 227bcd78..5d61298c 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -1987,6 +1987,8 @@ let translate_arm_instruction | 2 -> 4 | 3 -> 8 | 4 -> 16 + | 5 -> 32 + | 6 -> 64 | _ -> 1 in (* not reachable by small immediate *) let usevars = get_register_vars [rn] in let usehigh = get_use_high_vars_r [xxrn_r] in diff --git a/CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml b/CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml index fd529628..f476616e 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml @@ -268,7 +268,7 @@ let translate_mips_instruction let frozenasserts = List.map (fun (v, fv) -> ASSERT (EQ (v, fv))) (finfo#get_test_variables ctxtiaddr) in - let rewrite_expr floc x:xpr_t = + let rewrite_expr (floc: floc_int) (x: xpr_t):xpr_t = let rec expand x = match x with | XVar v From 985e20d28f14ed1b2f510032a6bb4406f9bc9f48 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 21 Oct 2025 19:19:13 -0700 Subject: [PATCH 3/7] CHB: add loopcounter and const-globals to function annotations --- CodeHawk/CHB/bchlib/bCHFunctionData.ml | 136 +++++++++++++++---------- 1 file changed, 82 insertions(+), 54 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionData.ml b/CodeHawk/CHB/bchlib/bCHFunctionData.ml index 84ef74e0..d77d1ecd 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionData.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionData.ml @@ -75,7 +75,8 @@ let stackvar_intro_to_string (svi: stackvar_intro_t) = match svi.svi_vartype with | Some t -> " (" ^ (btype_to_string t) ^ ")" | _ -> "" in - (string_of_int svi.svi_offset) ^ ": " ^ svi.svi_name ^ ptype + let lc_p = if svi.svi_loopcounter then " (lc)" else "" in + (string_of_int svi.svi_offset) ^ ": " ^ svi.svi_name ^ ptype ^ lc_p let reachingdef_spec_to_string (rds: reachingdef_spec_t) = @@ -374,6 +375,11 @@ object (self) else BCHSystemSettings.system_settings#is_typing_rule_enabled name + method is_const_global_variable (name: string): bool = + match self#get_function_annotation with + | None -> false + | Some a -> List.mem name a.constglobalvars + method filter_deflocs (iaddr: string) (v: variable_t) (deflocs: symbol_t list): symbol_t list = match self#get_function_annotation with @@ -689,6 +695,7 @@ let read_xml_stackvar_intro (node: xml_element_int): stackvar_intro_t traceresul else let svi_offset = (-(geti "offset")) in let svi_name = get "name" in + let svi_loopcounter = has "loopcounter" && (get "loopcounter") = "yes" in let (svi_vartype, svi_cast) = if has "typename" then let typename = get "typename" in @@ -712,6 +719,7 @@ let read_xml_stackvar_intro (node: xml_element_int): stackvar_intro_t traceresul (None, false) in Ok {svi_offset = svi_offset; svi_name = svi_name; + svi_loopcounter = svi_loopcounter; svi_vartype = svi_vartype; svi_cast = svi_cast} @@ -757,6 +765,66 @@ let read_xml_reachingdef_spec } +let read_xml_stackvarintros (node: xml_element_int): stackvar_intro_t list = + List.fold_left + (fun acc n -> + TR.tfold + ~ok:(fun svi -> svi :: acc) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ e; + acc + end) + (read_xml_stackvar_intro n)) + [] + (node#getTaggedChildren "vintro") + + +let read_xml_regvarintros (node: xml_element_int): regvar_intro_t list = + List.fold_left + (fun acc n -> + TR.tfold + ~ok:(fun rvi -> rvi :: acc) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ e; + acc + end) + (read_xml_regvar_intro n)) + [] + (node#getTaggedChildren "vintro") + + +let read_xml_typingrules (node: xml_element_int): typing_rule_t list = + List.fold_left + (fun acc n -> + TR.tfold + ~ok:(fun tr -> tr :: acc) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ e; + acc + end) + (read_xml_typing_rule n)) + [] + (node#getTaggedChildren "typingrule") + + +let read_xml_removerdefs (node: xml_element_int): reachingdef_spec_t list = + List.fold_left + (fun acc n -> + TR.tfold + ~ok:(fun rds -> rds :: acc) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ e; + acc + end) + (read_xml_reachingdef_spec n)) + [] + (node#getTaggedChildren "remove-var-rdefs") + + let read_xml_function_annotation (node: xml_element_int) = let get = node#getAttribute in let getc = node#getTaggedChild in @@ -771,77 +839,37 @@ let read_xml_function_annotation (node: xml_element_int) = functions_data#add_function dw in let stackvintros = if hasc "stackvar-intros" then - let svintros = getc "stackvar-intros" in - List.fold_left - (fun acc n -> - TR.tfold - ~ok:(fun svi -> svi :: acc) - ~error:(fun e -> - begin - log_error_result __FILE__ __LINE__ e; - acc - end) - (read_xml_stackvar_intro n)) - [] - (svintros#getTaggedChildren "vintro") + read_xml_stackvarintros (getc "stackvar-intros") else [] in let regvintros = if hasc "regvar-intros" then - let rvintros = getc "regvar-intros" in - List.fold_left - (fun acc n -> - TR.tfold - ~ok:(fun rvi -> rvi :: acc) - ~error:(fun e -> - begin - log_error_result __FILE__ __LINE__ e; - acc - end) - (read_xml_regvar_intro n)) - [] - (rvintros#getTaggedChildren "vintro") + read_xml_regvarintros (getc "regvar-intros") else [] in let typingrules = if hasc "typing-rules" then - let trules = getc "typing-rules" in - List.fold_left - (fun acc n -> - TR.tfold - ~ok:(fun tr -> tr :: acc) - ~error:(fun e -> - begin - log_error_result __FILE__ __LINE__ e; - acc - end) - (read_xml_typing_rule n)) - [] - (trules#getTaggedChildren "typingrule") + read_xml_typingrules (getc "typing-rules") else [] in let rdefspecs = if hasc "remove-rdefs" then - let rrds = getc "remove-rdefs" in - List.fold_left - (fun acc n -> - TR.tfold - ~ok:(fun rds -> rds :: acc) - ~error:(fun e -> - begin - log_error_result __FILE__ __LINE__ e; - acc - end) - (read_xml_reachingdef_spec n)) - [] - (rrds#getTaggedChildren "remove-var-rdefs") + read_xml_removerdefs (getc "remove-rdefs") + else + [] in + let constglobals = + if hasc "const-global-variables" then + let gnode = getc "const-global-variables" in + List.map + (fun n -> n#getAttribute "name") (gnode#getTaggedChildren "gvar") else [] in fndata#set_function_annotation {regvarintros = regvintros; stackvarintros = stackvintros; typingrules = typingrules; - reachingdefspecs = rdefspecs + reachingdefspecs = rdefspecs; + constglobalvars = constglobals }) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) (string_to_doubleword faddr) From 16ab1eed78c77ab57b21219b0d6b6cc55962e5e7 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 21 Oct 2025 19:30:23 -0700 Subject: [PATCH 4/7] CHB: add rewriting with loop counters --- CodeHawk/CHB/bchlib/bCHLocationInvariant.ml | 76 ++++++++++++++------ CodeHawk/CHB/bchlib/bCHLocationInvariant.mli | 2 +- 2 files changed, 56 insertions(+), 22 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml index 57cc1fae..3e937ac8 100644 --- a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml +++ b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml @@ -231,38 +231,34 @@ let get_variable_equality_variables (lineq: linear_equality_t) = [] -let linear_equality_get_expr e v = +(* Note: the signature of this function should be changed into a result + type; the function should not raise an exception. + *) +let linear_equality_get_expr (lineq: linear_equality_t) (v: variable_t): xpr_t option = let make_factor c f = if c#equal numerical_one then XVar f else XOp (XMult, [num_constant_expr c; XVar f]) in try - let (c, _f) = List.find (fun (_, f) -> f#equal v) e.leq_factors in - let xfactors = List.filter (fun (_, f) -> not (f#equal v)) e.leq_factors in + let (c, _f) = List.find (fun (_, f) -> f#equal v) lineq.leq_factors in + let xfactors = List.filter (fun (_, f) -> not (f#equal v)) lineq.leq_factors in let x = if c#equal numerical_one then List.fold_left (fun a (c,f) -> XOp (XPlus, [a; make_factor c#neg f])) - (num_constant_expr e.leq_constant) xfactors + (num_constant_expr lineq.leq_constant) xfactors else if c#equal numerical_one#neg then List.fold_left (fun a (c,f) -> XOp (XPlus, [a; make_factor c f])) - (num_constant_expr e.leq_constant#neg) xfactors + (num_constant_expr lineq.leq_constant#neg) xfactors else - raise + raise (BCH_failure - (LBLOCK [ - STR "Case with higher coefficients not yet handled: "; - linear_equality_to_pretty e])) in - simplify_xpr x + (LBLOCK [STR "Case with higher coefficients not yet handled: "; + linear_equality_to_pretty lineq])) in + Some (simplify_xpr x) with - Not_found -> - raise - (BCH_failure - (LBLOCK [ - STR "Variable "; - v#toPretty; - STR " not found in linear equality "; - linear_equality_to_pretty e])) + | Not_found -> + None let linear_equality_compare e1 e2 = @@ -416,6 +412,13 @@ object (self:'a) is_variable_equality lineq | _ -> false + method is_loopcounter_equality = + match fact with + | RelationalFact lineq -> + List.exists (fun (_, f) -> List.mem "lc" f#getName#getAttributes) + lineq.leq_factors + | _ -> false + method get_variable_equality_variables = match fact with | RelationalFact lineq when is_variable_equality lineq -> @@ -425,6 +428,14 @@ object (self:'a) (BCH_failure (LBLOCK [STR "Not a variable-equality: "; self#toPretty])) + method get_var_loopcounter_expr (v: variable_t): xpr_t option = + if self#is_loopcounter_equality then + match fact with + | RelationalFact lineq -> linear_equality_get_expr lineq v + | _ -> None + else + None + method is_smaller (other:'a) = match (fact, other#get_fact) with | (NonRelationalFact (_, i1), NonRelationalFact (_, i2)) -> is_smaller_nrv i1 i2 @@ -643,7 +654,13 @@ object (self) | NonRelationalFact (w, FSymbolicExpr x) when w#equal v -> Some x | _ -> None) None (self#get_var_facts v) - method rewrite_expr (x:xpr_t) = + method private get_var_loopcounter_expr (v: variable_t): xpr_t option = + List.fold_left (fun acc inv -> + match acc with + | Some _ -> acc + | _ -> inv#get_var_loopcounter_expr v) None self#get_facts + + method rewrite_expr ?(loopcounter=false) (x:xpr_t) = let subst1 v = if self#is_constant v then XConst (IntConst (self#get_constant v)) @@ -662,7 +679,19 @@ object (self) match self#get_external_exprs v with | [] -> XVar v | x :: _tl -> x in - let x1 = simplify_xpr (substitute_expr subst1 x) in + let subst_lc v = + (* For now only user-designated loop counter variables are annotated + with the lc attribute. Loop counter does not refer to the engine + loop-counter variable. *) + if loopcounter && (not (List.mem "lc" v#getName#getAttributes)) then + let eq = self#get_var_loopcounter_expr v in + match eq with + | Some x -> x + | _ -> XVar v + else + XVar v in + let x0 = simplify_xpr (substitute_expr subst_lc x) in + let x1 = simplify_xpr (substitute_expr subst1 x0) in let x2 = simplify_xpr (substitute_expr subst2 x1) in let x3 = simplify_xpr (substitute_expr subst3 x2) in let x4 = simplify_xpr (substitute_expr subst4 x3) in @@ -920,6 +949,9 @@ object (self) | NonRelationalFact (w, FSymbolicExpr _) when v#equal w -> true | _ -> false) false (self#get_var_facts v) + method has_loop_counter_equality: bool = + List.exists (fun inv -> inv#is_loopcounter_equality) self#get_facts + method write_xml (node:xml_element_int) = let invs = List.sort Stdlib.compare (H.fold (fun k _ a -> k::a) facts []) in if (List.length invs) > 0 then @@ -1134,7 +1166,9 @@ object (self) self#add iaddr (TestVarEquality (tvar,tval,taddr,jaddr)) method add_lineq (iaddr:string) (nc:numerical_constraint_t) = - self#add iaddr (RelationalFact (numerical_constraint_to_linear_equality nc)) + let lineq = numerical_constraint_to_linear_equality nc in + let fact = RelationalFact lineq in + self#add iaddr fact method get_location_invariant (iaddr:string) = match invariants#get iaddr with diff --git a/CodeHawk/CHB/bchlib/bCHLocationInvariant.mli b/CodeHawk/CHB/bchlib/bCHLocationInvariant.mli index 8b8c1303..805119f8 100644 --- a/CodeHawk/CHB/bchlib/bCHLocationInvariant.mli +++ b/CodeHawk/CHB/bchlib/bCHLocationInvariant.mli @@ -46,7 +46,7 @@ val numerical_constraint_to_linear_equality: val linear_equality_get_vars: linear_equality_t -> variable_t list -val linear_equality_get_expr: linear_equality_t -> variable_t -> xpr_t +val linear_equality_get_expr: linear_equality_t -> variable_t -> xpr_t option val mk_invariant_io: xml_element_int option -> vardictionary_int -> string -> invariant_io_int From b5220b03d90bb643345f18de6e2c7ee612e3a77d Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 21 Oct 2025 19:43:38 -0700 Subject: [PATCH 5/7] CHB: add attributes to assembly variables --- CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 43 +++++++++++++++++++------ CodeHawk/CHB/bchlib/bCHVarDictionary.ml | 37 ++++++++++++++++++++- CodeHawk/CHB/bchlib/bCHVariable.ml | 6 ++++ 3 files changed, 75 insertions(+), 11 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index f248756b..b52a1fc2 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -133,6 +133,7 @@ let pr_expr = xpr_formatter#pr_expr class function_environment_t (faddr:doubleword_int) + (fndata: function_data_int) (varmgr:variable_manager_int):function_environment_int = object (self) @@ -142,7 +143,8 @@ object (self) initializer List.iter (fun av -> - ignore (self#mk_variable av)) varmgr#get_assembly_variables + let atts = self#varmgr#get_av_attributes av#index in + ignore (self#mk_variable ~atts av)) varmgr#get_assembly_variables method get_variable_comparator = varmgr#get_external_variable_comparator @@ -161,7 +163,7 @@ object (self) method variable_names = variable_names - method varmgr = varmgr + method varmgr: variable_manager_int = varmgr method set_variable_name (v:variable_t) (name:string) = variable_names#add v#getName#getSeqNumber name @@ -578,19 +580,21 @@ object (self) (* Keep a separate map of symbolic variables per domain *) val dom_symchifvars = H.create 5 - method private add_chifvar (v:assembly_variable_int) (vt:variable_type_t) = + method private add_chifvar + ?(atts = []) (v:assembly_variable_int) (vt:variable_type_t) = if H.mem chifvars v#index then H.find chifvars v#index else - let vname = new symbol_t ~seqnr:v#index v#get_name in + let vname = new symbol_t ~atts ~seqnr:v#index v#get_name in let chifvar = scope#mkVariable vname vt in begin - H.add chifvars v#index chifvar ; + H.add chifvars v#index chifvar; + (if (List.length atts) > 0 then self#varmgr#set_av_attributes v#index atts); chifvar end - method private mk_variable (v:assembly_variable_int) = - self#add_chifvar v NUM_VAR_TYPE + method private mk_variable ?(atts = []) (v:assembly_variable_int) = + self#add_chifvar ~atts v NUM_VAR_TYPE method private add_domain_symchifvar (domain: string) (seqnr: int) (v: variable_t) = @@ -772,7 +776,12 @@ object (self) (LBLOCK [STR "Unknown memory reference in mk_offset_memory_variable"])) else let avar = varmgr#make_memory_variable memref ~size offset in - self#mk_variable avar + let var = self#mk_variable avar in + let _ = + ch_diagnostics_log#add + "mk_offset_memory_variable" + (LBLOCK [var#toPretty]) in + var method mk_basevar_memory_variable ?(size=4) @@ -893,11 +902,21 @@ object (self) tmap ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:stack") (fun memoffset -> + let atts: string list = if stackslot#is_loopcounter then ["lc"] else [] in let svar = self#mk_variable + ~atts (self#varmgr#make_local_stack_variable ~offset:memoffset (mkNumerical stackslot#offset)) in let name = stackslot#name ^ (memory_offset_to_string memoffset) in + let _ = + match atts with + | [] -> () + | _ -> + ch_diagnostics_log#add + "loopcounter variable on the stack" + (LBLOCK [STR "Offset: "; offset#toPretty; STR ": "; STR name; + STR "; "; svar#toPretty]) in begin self#set_variable_name svar name; svar @@ -1290,7 +1309,7 @@ object (self) method get_sideeffvar_count = List.length (List.filter self#is_sideeffect_value self#get_variables) - method is_global_variable (v:variable_t) = + method is_global_variable (v: variable_t) = (varmgr#is_global_variable v) || ((varmgr#is_initial_memory_value v) && (tfold_default @@ -1298,6 +1317,10 @@ object (self) false (varmgr#get_initial_memory_value_variable v))) + method is_mutable_global_variable (v: variable_t): bool = + (varmgr#is_global_variable v) + && (not (fndata#is_const_global_variable (self#variable_name_to_string v))) + method has_global_variable_address (v: variable_t): bool = varmgr#has_global_variable_address v @@ -1632,7 +1655,7 @@ object (self) * These data items are saved and reloaded as part of the intermediate * * analysis results. * * ------------------------------------------------------------------------- *) - val env = new function_environment_t faddr varmgr + val env = new function_environment_t faddr fndata varmgr val constant_table = new VariableCollections.table_t (* constants *) val calltargets = H.create 5 (* call-targets *) diff --git a/CodeHawk/CHB/bchlib/bCHVarDictionary.ml b/CodeHawk/CHB/bchlib/bCHVarDictionary.ml index c8435b97..fa0a10b0 100644 --- a/CodeHawk/CHB/bchlib/bCHVarDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHVarDictionary.ml @@ -44,6 +44,7 @@ open BCHBasicTypes open BCHLibTypes open BCHSumTypeSerializer +module H = Hashtbl module TR = CHTraceResult @@ -74,6 +75,9 @@ object (self) val faddr = faddr val xd = xd + + val assembly_variable_attributes = H.create 5 (* avar#index -> atts *) + val memory_base_table = mk_index_table "memory-base-table" val memory_offset_table = mk_index_table "memory-offset-table" val sideeffect_argument_location_table = @@ -106,6 +110,18 @@ object (self) method xd = xd + method set_av_attributes (index: int) (atts: string list) = + H.replace assembly_variable_attributes index atts + + method get_av_attributes (index: int): string list = + if H.mem assembly_variable_attributes index then + H.find assembly_variable_attributes index + else + [] + + method private list_av_attributes: (int * string list) list = + H.fold (fun k v a -> (k, v) :: a) assembly_variable_attributes [] + method get_indexed_variables = List.map (fun (_,index) -> (index,self#get_assembly_variable_denotation index)) assembly_variable_denotation_table#items @@ -346,10 +362,27 @@ object (self) ?(tag="isa") (node: xml_element_int) (sa: stack_access_t) = node#setIntAttribute tag (self#index_stack_access sa) + method private read_xml_av_attributes (node: xml_element_int) = + List.iter (fun avnode -> + let index = avnode#getIntAttribute "ix" in + let atts = avnode#getAttribute "atts" in + let atts = String.split_on_char ',' atts in + self#set_av_attributes index atts) (node#getTaggedChildren "av") + method write_xml (node:xml_element_int) = + let anode = xmlElement "av-attributes" in let vnode = xmlElement "var-dictionary" in let xnode = xmlElement "xpr-dictionary" in begin + anode#appendChildren + (List.map + (fun (k, v) -> + let avnode = xmlElement "av" in + begin + avnode#setIntAttribute "ix" k; + avnode#setAttribute "atts" (String.concat "," v); + avnode + end) self#list_av_attributes); vnode#appendChildren (List.map (fun t -> @@ -360,13 +393,15 @@ object (self) end) tables); xd#write_xml xnode; vnode#appendChildren [xnode]; - node#appendChildren [vnode] + node#appendChildren [anode; vnode] end method read_xml (node:xml_element_int) = let vnode = node#getTaggedChild "var-dictionary" in let getc = vnode#getTaggedChild in begin + (if node#hasOneTaggedChild "av-attributes" then + self#read_xml_av_attributes (node#getTaggedChild "av-attributes")); xd#read_xml (getc "xpr-dictionary"); List.iter (fun t -> t#read_xml (getc t#get_name)) tables end diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml index 2082babb..ac6272fd 100644 --- a/CodeHawk/CHB/bchlib/bCHVariable.ml +++ b/CodeHawk/CHB/bchlib/bCHVariable.ml @@ -543,6 +543,12 @@ object (self) method memrefmgr = memrefmgr + method set_av_attributes (avindex: int) (atts: string list) = + self#vard#set_av_attributes avindex atts + + method get_av_attributes (avindex: int): string list = + self#vard#get_av_attributes avindex + method private mk_variable (denotation:assembly_variable_denotation_t) = let index = vard#index_assembly_variable_denotation denotation in if H.mem vartable index then From 332be205920a307d6d4042554db26fa7552aeec5 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 21 Oct 2025 21:17:12 -0700 Subject: [PATCH 6/7] CHB: incorporate loop counters in result rewriting --- CodeHawk/CHB/bchlib/bCHFloc.ml | 54 ++++++++++++++++++-- CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml | 21 +++++++- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 30 +++++++++-- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +- 4 files changed, 100 insertions(+), 9 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index d4ef79ba..d79bc23d 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -1609,6 +1609,32 @@ object (self) TR.tfold_default BCHBCTypeUtil.is_pointer false (self#get_xpr_type y) in let default () = self#convert_xpr_offsets ~xtype ~size x in match x with + | XOp (XPlus, [y; XOp (XMult, [XConst (IntConst n); XVar v])]) -> + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"xpr_to_cxpr:scaled expr" + __FILE__ __LINE__ + ["y: " ^ (x2s y); + "var: " ^ (p2s v#toPretty); + "n: " ^ n#toString] in + let gloc_o = memmap#xpr_containing_location x in + (match gloc_o with + | Some gloc -> + let memoff_o = TR.to_option (gloc#address_memory_offset self#l x) in + (match memoff_o with + | Some memoff -> + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"xpr_to_cxpr:scaled gloc expr" + __FILE__ __LINE__ + [(x2s x); gloc#name; memory_offset_to_string memoff] in + Ok (XOp ((Xf "addressofvar"), + [XVar (self#f#env#mk_gloc_variable gloc memoff)])) + | _ -> default ()) + | _ -> default ()) + | XOp (XPlus, [y; XConst (IntConst n)]) when is_pointer y && arithm -> let derefty = BCHBCTypeUtil.ptr_deref (TR.tget_ok (self#get_xpr_type y)) in let _ = @@ -2374,8 +2400,20 @@ object (self) match rhs with | XConst (IntConst n) when n#gt CHNumerical.numerical_zero -> let dw = numerical_mod_to_doubleword n in - if memmap#has_location dw then - TR.tvalue (self#f#env#mk_global_variable_address dw) ~default:rhs + (* do not rewrite to global addresses in the presence of loop counter + equalities, because the presence of symbolic constants derails the + generation of loop invariants. *) + if (memmap#has_location dw) + && (not (self#inv#has_loop_counter_equality)) then + let newrhs = + TR.tvalue (self#f#env#mk_global_variable_address dw) ~default:rhs in + let _ = + ch_diagnostics_log#add + "rewrite constant to global address" + (LBLOCK [ + self#l#toPretty; STR ": "; + dw#toPretty; STR " ==> "; (x2p newrhs)]) in + newrhs else rhs | _ -> rhs in @@ -2426,6 +2464,7 @@ object (self) let reqC = self#env#request_num_constant in let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in + let fndata = self#f#get_function_data in match fndata#get_regvar_intro self#ia with | Some rvi when rvi.rvi_cast && Option.is_some rvi.rvi_vartype -> @@ -3216,7 +3255,16 @@ object (self) let bridgeVars = self#env#get_bridge_values_at self#cia in let abstractglobals = let globals = - List.filter self#env#is_global_variable self#env#get_variables in + List.filter self#f#env#is_mutable_global_variable self#env#get_variables in + let _ = + ch_diagnostics_log#add + "call: abstract globals" + (LBLOCK [ + self#l#toPretty; STR ": "; + pretty_print_list + globals + (fun v -> STR (self#f#env#variable_name_to_string v)) + "[" ", " "]"]) in [ABSTRACT_VARS globals] in let sideeffect_assigns = self#get_sideeffect_assigns termev self#get_call_target#get_semantics in diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml index 4b0c0d35..84483d66 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml @@ -107,6 +107,8 @@ object (self) | Ok t -> is_scalar t | _ -> false + method is_loopcounter: bool = sslot.sslot_loopcounter + method size: int option = sslot.sslot_size method desc = sslot.sslot_desc @@ -365,6 +367,7 @@ object (self) sslot_name = svintro.svi_name; sslot_btype = ty; sslot_spill = None; + sslot_loopcounter = svintro.svi_loopcounter; sslot_desc = Some ("svintro"); sslot_size = size} in let stackslot = new stackslot_t sslot in @@ -449,6 +452,7 @@ object (self) sslot_btype = btype; sslot_spill = spill; sslot_size = size; + sslot_loopcounter = false; sslot_desc = desc } in let sslot = new stackslot_t ssrec in @@ -495,6 +499,7 @@ object (self) sslot_btype = t_unknown; sslot_spill = Some reg; sslot_size = Some 4; + sslot_loopcounter = false; sslot_desc = Some "register spill" } in let sslot = new stackslot_t ssrec in @@ -534,6 +539,7 @@ object (self) sslot_btype = t_unknown; sslot_spill = Some reg; sslot_size = Some 4; + sslot_loopcounter = false; sslot_desc = Some "register_spill" } in let sslot = new stackslot_t ssrec in @@ -571,7 +577,20 @@ object (self) (iaddr:ctxt_iaddress_t) = let ty = match typ with Some t -> t | _ -> t_unknown in let blread = StackBlockRead (offset, size, ty) in - self#add_access offset iaddr blread + let ssrec = { + sslot_name = "blockread"; + sslot_offset = offset; + sslot_btype = ty; + sslot_size = size; + sslot_spill = None; + sslot_loopcounter = false; + sslot_desc = None + } in + let sslot = new stackslot_t ssrec in + begin + self#add_access offset iaddr blread; + H.add stackslots offset sslot + end method add_block_write ~(offset:int) diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index a6034fb8..b24362d1 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1511,7 +1511,8 @@ type stackvar_intro_t = { svi_offset: int; svi_name: string; svi_vartype: btype_t option; - svi_cast: bool + svi_cast: bool; + svi_loopcounter: bool } type typing_rule_t = { @@ -1531,7 +1532,8 @@ type function_annotation_t = { regvarintros: regvar_intro_t list; stackvarintros: stackvar_intro_t list; typingrules: typing_rule_t list; - reachingdefspecs: reachingdef_spec_t list + reachingdefspecs: reachingdef_spec_t list; + constglobalvars: string list } class type function_data_int = @@ -1592,6 +1594,7 @@ class type function_data_int = method has_regvar_type_cast: doubleword_int -> bool method has_stackvar_type_annotation: int -> bool method has_stackvar_type_cast: int -> bool + method is_const_global_variable: string -> bool method filter_deflocs: string -> variable_t -> symbol_t list -> symbol_t list method is_typing_rule_enabled: ?rdef:string option -> string -> string -> bool method has_class_info: bool @@ -1858,11 +1861,13 @@ object ('a) method get_fact: invariant_fact_t method get_variables: variable_t list method get_variable_equality_variables: variable_t list + method get_var_loopcounter_expr: variable_t -> xpr_t option method is_constant: bool method is_interval: bool method is_base_offset_value: bool method is_symbolic_expr: bool method is_linear_equality: bool + method is_loopcounter_equality: bool method is_variable_equality: bool method is_smaller: 'a -> bool method write_xml: xml_element_int -> unit @@ -1893,7 +1898,7 @@ object method get_known_initial_values: variable_t list method get_init_disequalities: variable_t list (* initial values *) method get_init_equalities: variable_t list (* initial values *) - method rewrite_expr: xpr_t -> xpr_t + method rewrite_expr: ?loopcounter:bool -> xpr_t -> xpr_t (* predicates *) method is_unreachable: bool @@ -1907,6 +1912,7 @@ object variable_t -> ctxt_iaddress_t -> ctxt_iaddress_t -> bool method var_has_initial_value: variable_t -> bool method var_has_symbolic_expr: variable_t -> bool + method has_loop_counter_equality: bool (* xml *) method write_xml: xml_element_int -> unit @@ -3780,6 +3786,10 @@ class type vardictionary_int = method xd: xprdictionary_int method faddr: doubleword_int method reset: unit + + method set_av_attributes: int -> string list -> unit + method get_av_attributes: int -> string list + method get_indexed_variables: (int * assembly_variable_denotation_t) list method get_indexed_bases: (int * memory_base_t) list @@ -3840,6 +3850,9 @@ object (** Returns the memory reference manager for this function.*) method memrefmgr: memory_reference_manager_int + method set_av_attributes: int -> string list -> unit + method get_av_attributes: int -> string list + (** {1 Creating variables}*) (** {2 Registers and flags}*) @@ -4580,6 +4593,7 @@ end sslot_btype: btype_t; sslot_size: int option; sslot_spill: register_t option; + sslot_loopcounter: bool; sslot_desc: string option } @@ -4612,6 +4626,7 @@ class type stackslot_int = method is_struct: bool method is_array: bool method is_spill: bool + method is_loopcounter: bool method write_xml: xml_element_int -> unit end @@ -5018,6 +5033,15 @@ class type function_environment_int = or if [var] is the initial value of a global variable. *) method is_global_variable: variable_t -> bool + (** [is_mutable_global_variable var] returns [true] if [var] is a global + variable, but not an initial memory value and not a const global variable + (as annotated in the function annotations). + + Note: non-mutability is asserted only in the context of a given function + (as derived from the function annotations). + *) + method is_mutable_global_variable: variable_t -> bool + (** Returns true if [var] is a global variable with a constant offset (i.e., a numerical value). *) method has_global_variable_address: variable_t -> bool diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 5d046b3b..169e0e43 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20251012" - ~date:"2025-10-12" + ~version:"0.6.0_20251021" + ~date:"2025-10-21" ~licensee: None ~maxfilesize: None () From c37cbb559af220bc169df0d7755a66e69d8a5d73 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 22 Oct 2025 11:22:02 -0700 Subject: [PATCH 7/7] CHB: add scaled expression term arrangement --- CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml | 2 +- CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml | 3 ++- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 ++-- CodeHawk/CHB/bchlib/bCHXprUtil.ml | 10 ++++++++-- 4 files changed, 13 insertions(+), 6 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml index 84483d66..7c0996bd 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml @@ -578,7 +578,7 @@ object (self) let ty = match typ with Some t -> t | _ -> t_unknown in let blread = StackBlockRead (offset, size, ty) in let ssrec = { - sslot_name = "blockread"; + sslot_name = "localvar_" ^ (string_of_int (-offset)); sslot_offset = offset; sslot_btype = ty; sslot_size = size; diff --git a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml index 584dc99f..3381fbf2 100644 --- a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml +++ b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml @@ -440,7 +440,8 @@ object (self) match optindex with | None -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Unable to extract index from " ^ (x2s xoffset)] + ^ "Unable to extract index from " ^ (x2s xoffset) + ^ " with element size " ^ (string_of_int elsize)] | Some (indexxpr, xrem) when iszero xrem && Option.is_none tgtsize diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 169e0e43..3112e833 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20251021" - ~date:"2025-10-21" + ~version:"0.6.0_20251022" + ~date:"2025-10-22" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlib/bCHXprUtil.ml b/CodeHawk/CHB/bchlib/bCHXprUtil.ml index 237b3640..29d04639 100644 --- a/CodeHawk/CHB/bchlib/bCHXprUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHXprUtil.ml @@ -127,7 +127,10 @@ let get_array_index_offset (xpr: xpr_t) (size: int): (xpr_t * xpr_t) option = when n#equal numsize -> Some (XVar v, xzero) | XOp (XPlus, [XOp (XMult, [XConst (IntConst n1); XVar v]); - XConst (IntConst n2)]) when n1#equal numsize -> + XConst (IntConst n2)]) + | XOp (XPlus, [XConst (IntConst n2); + XOp (XMult, [XConst (IntConst n1); XVar v])]) + when n1#equal numsize -> if n2#equal numerical_zero then Some (XVar v, xzero) else @@ -136,7 +139,10 @@ let get_array_index_offset (xpr: xpr_t) (size: int): (xpr_t * xpr_t) option = if quo#equal numerical_zero then Some (XVar v, xrem) else - Some (XOp (XPlus, [XVar v; num_constant_expr quo]), xrem) + if quo#lt numerical_zero then + Some (XOp (XMinus, [XVar v; num_constant_expr quo#neg]), xrem) + else + Some (XOp (XPlus, [XVar v; num_constant_expr quo]), xrem) | XOp (XMinus, [XOp (XMult, [XConst (IntConst n1); XVar v]); XConst (IntConst n2)]) when n1#equal numsize -> if n2#equal numerical_zero then