From 5801d40ea4ddaf8f7896d75de73119fc5c452889 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Mon, 8 Jun 2026 00:07:11 -0700 Subject: [PATCH] CHC: allow for pointer types in lifting to api --- CodeHawk/CHC/cchanalyze/cCHPOQuery.ml | 133 +++++++++++++++++++------- CodeHawk/CHC/cchlib/cCHTypesUtil.ml | 6 ++ CodeHawk/CHC/cchlib/cCHTypesUtil.mli | 2 + 3 files changed, 106 insertions(+), 35 deletions(-) diff --git a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml index f65622ba..6533f6bf 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml @@ -1621,14 +1621,25 @@ object (self) match (self#x2global x1, self#x2global x2) with | (Some a1, Some a2) -> TR.tfold - ~ok:(fun ty -> - begin - match op with - | XPlus -> Some (BinOp (PlusA, a1, a2, ty)) - | XMinus -> Some (BinOp (MinusA, a1, a2, ty)) - | XMult -> Some (BinOp (Mult, a1, a2, ty)) - | _ -> None - end) + ~ok:(fun ty1 -> + TR.tfold + ~ok:(fun ty2 -> + if is_arithmetic_type ty1 && is_arithmetic_type ty2 then + self#x2api_arithmetic_expr op a1 a2 ty1 ty2 + else + self#x2api_pointer_expr op a1 a2 ty1 ty2) + ~error:(fun e -> + begin + log_diagnostics_result + ~tag:"x2global" + ~msg:self#fname + __FILE__ __LINE__ + ["Unable to determine type of exp: " + ^ (p2s (exp_to_pretty a2)); + String.concat "; " e]; + None + end) + (type_of_exp fenv a2)) ~error:(fun e -> begin log_diagnostics_result @@ -1640,7 +1651,7 @@ object (self) String.concat "; " e]; None end) - (type_of_exp fenv a1) + (type_of_exp fenv a1) | _ -> None end | _ -> @@ -1649,6 +1660,80 @@ object (self) None end + method private x2api_arithmetic_expr + (op: xop_t) (a1: exp) (a2: exp) (ty1: typ) (ty2: typ): exp option = + TR.tfold + ~ok:(fun resulttyp -> + begin + match op with + | XPlus -> Some (BinOp (PlusA, a1, a2, resulttyp)) + | XMinus -> Some (BinOp (MinusA, a1, a2, resulttyp)) + | XMult -> Some (BinOp (Mult, a1, a2, resulttyp)) + | XDiv -> Some (BinOp (Div, a1, a2, resulttyp)) + | XShiftrt -> Some (BinOp (Shiftrt, a1, a2, ty1)) + | XShiftlt -> Some (BinOp (Shiftlt, a1, a2, ty1)) + | XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool, []))) + | XLe -> Some (BinOp (Le, a1, a2, TInt (IBool, []))) + | XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool, []))) + | XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool, []))) + | _ -> None + end) + ~error:(fun err -> + begin + log_diagnostics_result + ~tag:"x2api_arithmetic_expr" + ~msg:self#env#get_functionname + __FILE__ __LINE__ + [String.concat ", " err]; + None + end) + (usual_arithmetic_conversion ty1 ty2) + + method private x2api_pointer_expr + (op: xop_t) (a1: exp) (a2: exp) (ty1: typ) (ty2: typ): exp option = + if is_pointer_type ty1 && is_arithmetic_type ty2 then + match op with + | XPlus -> Some (BinOp (PlusPI, a1, a2, ty1)) + | XMinus -> Some (BinOp (MinusPI, a1, a2, ty1)) + | _ -> + begin + log_diagnostics_result + ~tag:"x2api_pointer_expr" + ~msg:self#env#get_functionname + __FILE__ __LINE__ + ["pointer type and arithmetic type with operator " + ^ (XprToPretty.xop_to_string op)]; + None + end + else if is_pointer_type ty1 && is_pointer_type ty2 then + match op with + | XMinus -> Some (BinOp (MinusPP, a1, a2, TInt (IInt, []))) + | XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool, []))) + | XLe -> Some (BinOp (Le, a1, a2, TInt (IBool, []))) + | XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool, []))) + | XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool, []))) + | _ -> + begin + log_diagnostics_result + ~tag:"x2api_pointer_expr" + ~msg:self#env#get_functionname + __FILE__ __LINE__ + ["2-pointer expr with operator: " + ^ (XprToPretty.xop_to_string op)]; + None + end + else + begin + log_diagnostics_result + ~tag:"x2api_pointer_expr" + ~msg:self#env#get_functionname + __FILE__ __LINE__ + ["op: " ^ (XprToPretty.xop_to_string op); + "ty1: " ^ (p2s (typ_to_pretty ty1)); + "ty2: " ^ (p2s (typ_to_pretty ty2))]; + None + end + method x2api (x:xpr_t):exp option = match x with | XConst (IntConst n) -> Some (make_constant_exp n) @@ -1686,32 +1771,10 @@ object (self) ~ok:(fun ty1 -> TR.tfold ~ok:(fun ty2 -> - TR.tfold - ~ok:(fun resulttyp -> - begin - match op with - | XPlus -> Some (BinOp (PlusA, a1, a2, resulttyp)) - | XMinus -> Some (BinOp (MinusA, a1, a2, resulttyp)) - | XMult -> Some (BinOp (Mult, a1, a2, resulttyp)) - | XDiv -> Some (BinOp (Div, a1, a2, resulttyp)) - | XShiftrt -> Some (BinOp (Shiftrt, a1, a2, ty1)) - | XShiftlt -> Some (BinOp (Shiftlt, a1, a2, ty1)) - | XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool, []))) - | XLe -> Some (BinOp (Le, a1, a2, TInt (IBool, []))) - | XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool, []))) - | XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool, []))) - | _ -> None - end) - ~error:(fun err -> - begin - log_diagnostics_result - ~tag:"x2api:integer-promotion" - ~msg:self#env#get_functionname - __FILE__ __LINE__ - [String.concat ", " err]; - None - end) - (usual_arithmetic_conversion ty1 ty2)) + if is_arithmetic_type ty1 && is_arithmetic_type ty2 then + self#x2api_arithmetic_expr op a1 a2 ty1 ty2 + else + self#x2api_pointer_expr op a1 a2 ty1 ty2) ~error:(fun err -> begin log_diagnostics_result diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml index d4346fee..fec9d193 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml +++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml @@ -716,6 +716,12 @@ let is_system_struct (t: typ): bool = | _ -> false +let is_arithmetic_type (t: typ): bool = + match fenv#get_type_unrolled t with + | TInt _ | TEnum _ | TFloat _ -> true + | _ -> false + + let is_integral_type (t:typ) = match fenv#get_type_unrolled t with | TInt _ -> true diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli index 28eaa363..b22f2b2d 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli +++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli @@ -105,6 +105,8 @@ val returntype_of_exp: cfundeclarations_int -> exp -> typ traceresult val is_system_struct: typ -> bool +val is_arithmetic_type: typ -> bool + val is_integral_type: typ -> bool val is_pointer_type : typ -> bool