From 27f962cc60415cd30c028357730ca1494d98346b Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Jun 2026 12:51:29 -0700 Subject: [PATCH 1/3] CHT:CHC: move cCHPOCheckInitializedTest to regression tests in CodeHawk-C --- .../cchanalyze_tests/txcchanalyze/Makefile | 9 +- .../txcchanalyze/cCHPOCheckInitializedTest.ml | 182 ------------------ .../cCHPOCheckInitializedTest.mli | 27 --- .../cchanalyze_tests/txcchanalyze/dune | 9 - .../PInitialized/gl_inv_001.cch.tar.gz | Bin 1349 -> 0 bytes .../PInitialized/gl_inv_002.cch.tar.gz | Bin 1565 -> 0 bytes .../PInitialized/gl_inv_003.cch.tar.gz | Bin 1568 -> 0 bytes .../gl_inv_bounded_xpr_001.cch.tar.gz | Bin 1746 -> 0 bytes .../PInitialized/gl_inv_xpr_001.cch.tar.gz | Bin 1460 -> 0 bytes .../PInitialized/gl_inv_xpr_002.cch.tar.gz | Bin 1493 -> 0 bytes .../PInitialized/gl_inv_xpr_003.cch.tar.gz | Bin 1479 -> 0 bytes .../PInitialized/gl_stackvar_001.cch.tar.gz | Bin 1725 -> 0 bytes 12 files changed, 2 insertions(+), 225 deletions(-) delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.mli delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_001.cch.tar.gz delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_002.cch.tar.gz delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_003.cch.tar.gz delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_bounded_xpr_001.cch.tar.gz delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_001.cch.tar.gz delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_002.cch.tar.gz delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_003.cch.tar.gz delete mode 100644 CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_stackvar_001.cch.tar.gz diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile index f8cd3ccc4..cde3ad979 100644 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile +++ b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile @@ -58,7 +58,7 @@ SOURCES := \ OBJECTS := $(addprefix cmx/,$(SOURCES:%=%.cmx)) -all: make_dirs cCHPOCheckInitializedTest cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest +all: make_dirs cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest doc: @@ -66,17 +66,13 @@ make_dirs: @mkdir -p cmx @mkdir -p cmi -cCHPOCheckInitializedTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa cmi/cCHPOCheckInitializedTest.cmi cmx/cCHPOCheckInitializedTest.cmx - $(CAMLLINK) -o cCHPOCheckInitializedTest $(OBJECTS) cmx/cCHPOCheckInitializedTest.cmx - cCHPOCheckLocallyInitializedTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa cmi/cCHPOCheckLocallyInitializedTest.cmi cmx/cCHPOCheckLocallyInitializedTest.cmx $(CAMLLINK) -o cCHPOCheckLocallyInitializedTest $(OBJECTS) cmx/cCHPOCheckLocallyInitializedTest.cmx cCHPOCheckOutputParameterInitializedTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa cmi/cCHPOCheckOutputParameterInitializedTest.cmi cmx/cCHPOCheckOutputParameterInitializedTest.cmx $(CAMLLINK) -o cCHPOCheckOutputParameterInitializedTest $(OBJECTS) cmx/cCHPOCheckOutputParameterInitializedTest.cmx -run: cCHPOCheckInitializedTest cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest - ./cCHPOCheckInitializedTest +run: cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest ./cCHPOCheckLocallyInitializedTest ./cCHPOCheckOutputParameterInitializedTest @@ -100,6 +96,5 @@ clean: rm -f *.ml~ rm -f *.mli~ rm -f Makefile~ - rm -f cCHPOCheckInitializedTest rm -f cCHPOCheckLocallyInitializedTest rm -f cCHPOCheckOutputParameterInitialized diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml deleted file mode 100644 index 4f7b68935..000000000 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml +++ /dev/null @@ -1,182 +0,0 @@ -(* ============================================================================= - CodeHawk Unit Testing Framework - Author: Henny Sipma - Adapted from: Kaputt (https://kaputt.x9c.fr/index.html) - ------------------------------------------------------------------------------ - The MIT License (MIT) - - Copyright (c) 2025 Aarno Labs LLC - - Permission is hereby granted, free of charge, to any person obtaining a copy - of this software and associated documentation files (the "Software"), to deal - in the Software without restriction, including without limitation the rights - 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 - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) - -open CCHPreTypes -open CCHProofScaffolding - -module A = TCHAssertion -module TS = TCHTestSuite -module CA = TCHCchanalyzeAssertion -module CU = TCHCchanalyzeUtils - - -let testname = "cCHPOCheckInitializedTest" -let lastupdated = "2025-11-10" - - -let po_filter (po: proof_obligation_int): proof_obligation_int option = - match po#get_predicate with - | PInitialized _ -> Some po - | _ -> None - - -(* See CHT/CHC_tests/cchanalyze_tests/tcchanalyze/tCHCchanalyzeUtils.mli - for a description and example of how to specify the tests. - - Tests: - - Test: gl-inv-001: - ================= - int gl_inv_001(void) { - - int i = 5; - - return i; - } - - Test: gl-inv-002: - ================= - typedef struct mystruct_s { - int fld1; - int fld2; - } mystruct; - - - int gl_inv_002(void) { - - mystruct s = {.fld1 = 5, .fld2 = 3 }; - - return s.fld1; - } - - Test: gl-inv-003: - ================= - int gl_inv_003(int k) { - - int i; - - if (k > 0) { - i = 5; - } else { - i = 3; - } - - return i; - } - - Test gl-inv-xpr-001: - ==================== - int gl_inv_xpr_001(void) { - - int i = 5; - - int *p = &i; - - return *p; - } - - - *) -let check_safe () = - let tests = [ - ("gl-inv-001", - "gl_inv_001", "gl_inv_001", - [], -1, -1, - Some "inv_implies_safe", "assignedAt#5"); - ("gl-inv-002", - "gl_inv_002", "gl_inv_002", - [], -1, -1, - Some "inv_implies_safe", "assignedAt#11"); - ("gl-inv-003", - "gl_inv_003", "gl_inv_003", - [], 14, -1, - Some "inv_implies_safe", "") - (* disabling the tests based on the presence of an - initial value - ("gl-inv-xpr-001", - "gl_inv_xpr_001", "gl_inv_xpr_001", - ["(*p)"], -1, -1, - "inv_xpr_implies_safe", "variable (*p) has the value 5"); - ("gl-inv-xpr-002", - "gl_inv_xpr_002", "gl_inv_xpr_002", - ["(*p)"], -1, -1, - "inv_xpr_implies_safe", "variable (*p) has the value 8"); - ("gl-inv-xpr-003", - "gl_inv_xpr_003", "gl_inv_xpr_003", - [], 11, -1, - "inv_xpr_implies_safe", "variable i has the value 8"); - ("gl-inv-bounded-xpr-001", - "gl_inv_bounded_xpr_001", "gl_inv_bounded_xpr_001", - ["(*p)"], 14, -1, - "inv_bounded_xpr_implies_safe", "variable (*p) is bounded by LB: 3 and UB: 5"); - ("gl-stackvar-001", - "gl_stackvar_001", "gl_stackvar_001", - ["(*p)"], 14, -1, - "memlval_vinv_memref_stackvar_implies_safe", - "assignment(s) to i: assignedAt#11_xx_assignedAt#9") - *) - ] in - begin - TS.new_testsuite (testname ^ "_check_safe") lastupdated; - CHTiming.disable_timing (); - - List.iter - (fun (title, filename, funname, reqargs, line, byte, xdetail, expl) -> - TS.add_simple_test - ~title - (fun () -> - let _ = CCHSettings.system_settings#set_undefined_behavior_analysis in - let _ = CU.analysis_setup "PInitialized" filename in - let po_s = proof_scaffolding#get_proof_obligations funname in - let po_s = List.filter_map po_filter po_s in - let tgtpo_o = CU.select_target_po ~reqargs ~line ~byte po_s in - begin - CU.analysis_take_down filename; - match tgtpo_o with - | Some po -> CA.expect_safe_detail ~po ~xdetail ~expl () - | _ -> - let s_po_s = List.map CU.located_po_to_string po_s in - A.fail_msg - ("Unable to uniquely select target proof obligation: " - ^ "[" - ^ (String.concat "; " s_po_s) - ^ "]") - end - ) - ) tests; - - TS.launch_tests() - end - - -let () = - begin - TS.new_testfile testname lastupdated; - check_safe (); - TS.exit_file () - end diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.mli b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.mli deleted file mode 100644 index 25735d4d3..000000000 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* ============================================================================= - CodeHawk Unit Testing Framework - Author: Henny Sipma - Adapted from: Kaputt (https://kaputt.x9c.fr/index.html) - ------------------------------------------------------------------------------ - The MIT License (MIT) - - Copyright (c) 2025 Aarno Labs LLC - - Permission is hereby granted, free of charge, to any person obtaining a copy - of this software and associated documentation files (the "Software"), to deal - in the Software without restriction, including without limitation the rights - 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 - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/dune b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/dune index e7231e3c3..2fd1fcbe6 100644 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/dune +++ b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/dune @@ -1,19 +1,10 @@ (tests (names - cCHPOCheckInitializedTest cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest cCHPOCheckErrnoWrittenTest ) (deps - testinputs/PInitialized/gl_inv_001.cch.tar.gz - testinputs/PInitialized/gl_inv_002.cch.tar.gz - testinputs/PInitialized/gl_inv_003.cch.tar.gz - testinputs/PInitialized/gl_inv_xpr_001.cch.tar.gz - testinputs/PInitialized/gl_inv_xpr_002.cch.tar.gz - testinputs/PInitialized/gl_inv_xpr_003.cch.tar.gz - testinputs/PInitialized/gl_inv_bounded_xpr_001.cch.tar.gz - testinputs/PInitialized/gl_stackvar_001.cch.tar.gz testinputs/PLocallyInitialized/locally_initialized_gl_inv_001.cch.tar.gz testinputs/PLocallyInitialized/locally_initialized_gl_memlval_memref_001.cch.tar.gz testinputs/PLocallyInitialized/locally_initialized_rl_xpr_001.cch.tar.gz diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_001.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_001.cch.tar.gz deleted file mode 100644 index 103afd723af644ffcd063a03c54fc8ec168c91d3..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1349 zcmV-L1-kkliwFpLN93FfcJLV`FG8bYXG;?OIE3<2De^*}sC&UfP9i zJ#1N=ouou|DiG9R*#%^`;)e#0SWysPAn zi`|{$xZ@~V+gIm+0|)|NKi$B0n$HSXuJ1b2VCMOOd*!&E@64`*x*h)onLax?K zi2aFvkIDb1She}5=kS0R@E>@{|3%Q_zixOlS9m`EQ-3x^{x5-3{MR4vq9sq*_&!Zu zGKVI32815r-}RiJ&A;bNbo_VT`ejY{;QWW*fmE_%x#XFcTkhDg2oq5jbFrFRfBgQ- z=!^CJW)MarDrmBoT;2=_3D=CqEY~05OO!LJSWL8!%&ppMEV9Y7KUt(kG0)+V<@>p1 zud|fd#cJBOw^__=#iY_hW$_6HbH!=G|7Nj86i-2==Xn0eb>WY=!Plwt)w#B6n{R(} z$F5};cGPQayxfYYXehty0nkKvl10F{Mfi@3Wu`w?BkazQY6dDLOBcz0 z1e->&lnK?fVUyEUO1rI!-KzsZB`e@jcGIPP^fvggcxwEQd8E!1|0ka3_Ts(|rFB5UEo62I6KqQgo3pyCvX@tzt(7vXoQ;5J70YZ$wjV z%dy^J1Tj`op^hpcYHo3%hW?Plqp8z8G-UT1gECr1`UjQ8;96U!k5}|bb~I^D*wd^} z7MicROH;N!X&C+$dPN=7c@ndN#>>+?1^euNJA6Nbpe6?yt}2?q<>Z zr*X%q7deZHmZJ-OJsD1Vi(SjT$z&Lm@~KhoUJw0JJ~7I@NhSAMWE$-Xi_ikMp6)6f zh|^-j(lOHz@WHyd@2|no8y55x|D2}x*70%JBGafbTymDgCIj^C)6}jnlpL;U#&$#h z>ZW|$NkI-z@W5Tu_;J+Q(grPsBXzt6+VCd$!|}BH-|I?2&#(W?rk;oOpG)8r{|`yv zD=UF7;NK6h{&x{PjsMq0f@kyZInxR5|BK++{5OgMt@`j*94!w#R{xzjUWb3!{vPK4 zm%zu!|0_>67K816U0A{m+)x%hn)np8*HcNr^&tgtAQ|W+0la!_CJ54IUd{plUaZN>;M0Q`~Up-L>$sC z=$ z3&ayLHI5}-Il65t#v=p*fj}S-2m}IwKp+qZ1OkCTAP@)y0)apv5C{YU@nP{F9hs)m H08jt`QMbTo diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_002.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_002.cch.tar.gz deleted file mode 100644 index 979ba648e413131571daf68a8f3e1c11270f8f62..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1565 zcmV+&2IBc2iwFoE=o4uG17~bsX>N93FfcMMV`FG8bYXG;?OIE7qc{-GIln^1Tz03x zfB=(BaORMzt=iihcF!pcvZGxPE+o6+otpo?EePf%oVRyVqc2l2)7|QBsUMPX*4Zs( zyIaS>vn08*&)x$LAPfWf>4t&R{cLdN2Cn0WbKmhm&c%V_pP}GgycuB2MO-3uc1IZ7 zACY^E|3R_t$3K3L40u8OL#*R}5{%;C65cEoo*#cdn0q?@r@*oJzf~$cKmKzcV;%of z;8^@uTb2k~F#gI;@PhaUp|1av;A!!HT_<>U{ITPEy8cgsXUD&NyzM+DAUnIyGo=j~ z;Q8F2ioY9<;va-Q)W36z1^CJ1AANhpK7Uz?0KFo;kASdXKvQ+_VQY!>a9TE(N#Zj&mR;^X-wbyv<8xN~j60t4Wz*yyl z!oGCOH731?>}~{s*F-lu^kOJQyIYH|t^cQ;|DnG_;Y>F8NAOtx_uX)~|9h^h`~NBM zp8fwnZu*HOwJKYF)92S&v4n0b_8VfQWL25&_V%^pJXCxjyVGz-u#akJ^e08Wfo7pL z@xVkhX_Oxf4y{b;85?SM3cD{t*ft;Nn3R}Q0^8FO1vPg(_;8+VCl92D*~)2;He7o! zq_GflPV!~8x1e|h$q5rfA2wyY&f_6fkbCivD0OzcbvylVcxwMoX(HaK|NEXl?*H=r zkM95PkDufGpVYNpduz#D2JyITPtLIr=&4?mMUYDd{MI z-X>xuCY8u50%gJsObQ>pvtuoS4=d$j zOuYk;l*#l6F3rnhDT3#w>orTJT7XNh$)iBU#}|R=9x_2C;9Z(Q%@39QOaGuinLikZ zreE{t!}k^AsYg}oKD@!OhgmM!is+E(cPM_hUdOpoC4pji^vH{u(8OkyU-j#mu90^4 z>c62;YK&HtWa+deX~UAg=3Nv0Djdm%y_)S6HuOBT!AREHaX;h_RxRf(?{6L|MUlK7 zP&jlC!&lK25pV8a)13tP@ChF6x{E$b`m-HtsVa0(jzH7r`e$Hp{(tRPeM-FK??3#x z{{H6_7{$Lspl@X3k^7$$;Bff&AK_eo|8o+2LJsOT-Sbb#MbEmM*|r=6dZOi)W^!}C zZV0f4vE;jPvYOo)!1j=@9E)&0y6@}xx!m?)FsgSj z)NWN93FfcPNV`FG8bYXG;?OIE3<2De^IlqF?UbYL_ zdP_-H$sQIc&|44fc_B-*%|@aOkv8HM``hsf48`B0>}2F&=0-v!gk!i@h?#DCe{qFWjv`6x>#dM z_b2!sqW?#+>ia)=ixuz;|3{wo|5-5df7kG8OX2DM_k&3L|13D=|L*Zynvs;x?~D97 zI)sD6(4X?Z?>J%K|E}%1;RUi^d$20};Qo)lfK$;9SB#YO#&G7gfiO+WjL_AM@yGAK z%&v?tx0i7`OK6hs8DY1V2*qohWVjNK@FT5o!f}R{B*!;~ase4=Ql+Q9!!B<)B zZwzZ)7TBsM*82Lj%&^5V<3b9npP)10B+1ENI5Q9@1xR;oH<&pNe2^3U9KZ(*KAQja zH)rk`R&Aoy*%+rnXlw0EtYu(Ns(sT0jS1(~CaIEQ#*;;ktsa3awj56qSVL(EK%$7; z!&Dj_vo*yXrzM32Ncp4?#BU5jxoMjOzB-vl7VpU7O|iH~mSDgVTWSMhe7{kcl++e= zhSi-13X@u&;PFrKcnwc*QjY1E2Yt;b7lf7@bERNCur(vicS$~JRj6Qzt3tc7MbIhwYJmux09C=)y3v^iy=lQTS1X%EWk6aM8&x}|+k$XBI*{si1;04q zXj0(mFaSDy!y4bo#?RBji=&q_y3orf=|!?LSN_q z=fNre!#P+VQ0#@3fM@tWw6*`wg2(y)Wjn!>{qNeoul;`(JlX$JQAn;20qD=@(FuT zJdo1|DNjH4@Vd<7P{`>g9Fqpb*4W^fEy}E`do36*IFq!C--wY+Sl2ZR!X2R*BKUsO z)NVj)T}y%RfrUbrJ#LY3fnOKEbk}cJ=v3%-jWPLX!$Bj3tXj!dCx}2)sF2BrvH0y+ z>W5vDH-(~F2PBiSYkD%QX&tdu8>$|{Hcc6-2AR0Tu&HoXGdL;+5Dk+wno>(Or?EBR zgBa%wKifCn`FsVO?jHYkGaPjXm<-F|a`Lnm--QVLQuF8_gBw+lmg9 z)pjWK3)4KaU)Jf_(VqdJwL4IJykY1%!h7Md@BhTX`9|;m9M_J<@BeIl|2qfX^8WYU zFa2ghs`AR$-t$&@xezZT_8UCQ@Um7d@|`|elxSgJd=y7_-x{!py6tHp9mk{)xa6G> z&``&nk9pj2M_xhGVbd3P(a}ZM8gywjB#hx=k?&^^G#nS0@}UizDp?iDu$AL`esECZ z6}{pAOEB2~Us~!@;yM5S6@KZ?apLai@zc1mm5zpjv{j@|M@6au>1x1`p1l^$EGdzArA`_EZ zy}DI&YSJJf;rsvgfI1cb=_~1YDE{5RAIHC^+A diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_bounded_xpr_001.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_bounded_xpr_001.cch.tar.gz deleted file mode 100644 index a2df32a7d4ddfe3e99240eb317e3701c7b4a0587..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1746 zcmV;@1}*s?iwFqe_Y`RW17~bsX>N93VsCYBWMyPucyMxGFfcJLV`FG8bYXG;?OI!p zqc#+t=llwbm8y0{0_GBuU1qk@N|h?@Lm%4b5dkOT1`GlxnrXHFy*8I{Gh~v^us46w z2;y@%KK6Ic!8WrC?=d;vZ{h<9P;md4r1!cG7ry_X-MkcZ2FJ1a6*{)wyjHk@Hq>qC zn2rT+bZG02c?0Yh^I!yrjCv^mHxG!ArxCq#@^2KoVg9|BihwKlH=*Qz5{&XM7G4|{ z7xQmG+cG5oQ{Wo@FAa;!`L`VhO8%$7%kh8jZ*hngk5Sm|gA=@5T0{Ip!*n|QJIkeh z1N12-;0Nd5{lEwVN0eqbCbtS)=n6o@j{{70x5{6C{x)AJAMR$ZKlg|iK4mz&n*rcH zATK~EzhyuC6nPW{fb)N=h@(RRNgDr+d^!(s$}VyGbgO6&afGydX0?wW;{a(CWt5xA z@;hb-Q|yKK9~3Bn;)t0ySap~~IEMy+<~yjrvmK@O|KlHU0TnIxQLCL~?sKcThs2A9 zy(~wx3*(I!&goNv<^kH~Zp0+h+G0PB66)=qrQwHO>WNekIYi?|YK=i7M=u>QP)Pd^ zZx6)J8;alj0oDX?82c;|6o8MIY-4^~J)w0Tse16T3`LvpY0i>~q6iV%^&v^UUF3CJ zDSD(OSp`EZ(zIr%ed+Z0?(vfKKfpe{qW)WavDd5rOIiP?z*O~rAZWhyYoVw)#VF=H zewn(LKAj4pM`@a{x*5%>w+WHf65!2&qCr7cNGbsnvC{h3sHWVPA#K-ZHI{mW4jKXU zR>6d-wu;%Mws}%9PAXW9B;H(F^-3R-xjIsFV&FV?C8ROMw|z>&*#&ZF=cWJW;Tkfnuum zO-rKZN@Jo}sU3rTE8TDjAL2|DD}1ikEtlA0Ku!8{uxt_+p-8~lYTaan+t~}W)_QZs zxfX7^FL2c5Q+{?j`{dWbCJ04X`P%nTJ;g-RubvNXyxnGKJON45gh=0IOUO|RlqaYl zgKPGS>81%y1u803Tk}m>cr<opivBa#o zjs3i3h+hLbsyWCpR85odT;};&q+l%9>T)m;xZJMfwpgyK_F%9u2Mk?>uqren11qSm z3i(PXw^r2%4WWF!QrA@lYDT1R=G^?<$Cl+?p33OsVgb2G^axANy1Ae34zK4t!16!6 zSwzGybF~$ELhJ4pqc9LT!?#MJcE0<;Y)>I<7wA`8yy2{4ayC2`Q^%o!Ec{l*6DX4M{+l{~|I72g*T;{2{#Qlv*$+cQ?w2!=vCWR)bIIV2IR7Ryw)a|> zJ1?E>!Sv3VQgfTtIOI{y@(HWntrceniTDZq)Q8zUM!@Z@+@Q;@)*qsqZQ`IlLEU6D zqFJMN{u^XC;Nz*AxnPe;09ZQi__1Y1)0Q~j`m)BX-B>jPj2@HX%q0JO#kchQOs8nd zZL;lga~cZ&`!-!Iccksw!S^$ec6RVgkfbQcnscl1;R#1;h(=p@ZB<^clxqCj?%*lQ zhYeHO_r~9yVL{)f(icBt#@kaY=%Ohu$6{1tS)Ld$Mi{6kZnzHtBlQp}W^A$Lf*}EQ zC(|vys#ejQy4nB-E($YrH8<9D+}IU2&iBWSkb}`&HdRZM&0N$ziX6^qdpM_^YOdE+ zPN#?-Qqt)%_h!HgOEri6XwL(aRaLkCNdKIZsFC&GbB}k<;+p^eG;O*6p8})&4+!yv zeVkeU>x}L0|9`R@x&EI5Z-5SlPr+wz00bAU$2E;V#B92o0}lE3h`Xx6kE6&V!92tS z-BqR!S<2onet2M3GaC4FUj5K^@t`oV2`u5Wz$l&`_IozNgaWbrXD-_R0{)$`YRT{M z`|{>(0&c-i>?i-d1wZe>9k96~FR_@(Y_9nk@OMq4)y!M@Lq&;acHYlEf8_`NC9cVT z|H3}b<-ft+4ZZxgWd2V9?JfAd&R)J7KOzD)Px&1tJHXbwfUOh{2;dBqk+1-7HJM=& o5)u*;5)u*;5)u*;5)u*;5)u*;5)u*;5?>wu1GS438vsxM05pGa-T(jq diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_001.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_001.cch.tar.gz deleted file mode 100644 index be90d78c22f5347733c2b04d9a8724f32cd1e016..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1460 zcmV;l1xxxLiwFqu@)T(R17~bsX>N93cyMxGFfcJLV`FG8bYXG;?OIE3<2De^*}sC& z0!150mMB@)W>?N00u<=2hxQ!E5^b~9!w_jBZqfhVp=4Pv%CBS{wBd&Ywr0rTaAwGv zQL>DmX}W!WS?AA|g~wsIGVk6R7Qpjd@rgaxYJOI@!!EX5>|tk$?=0*%Q|}JBZ?1_1 z8^(hip}Q4H)7_DAr}+O-Ec^Zs-Z}!V@c-0O{=W&N{%;ds9S)cKe+n0X^8YPxj{jd9 z4j231#@5tT{=Wq-_y2Pk(U6Z{lK9*;goCHk$&mjY4^KM&x4o%-hpg|p@d_W@|Nb{{ zB-)ak(JY;5cx-8iq+u4(bUD+0|Ltevv-a(A0 zBDA0}nQ2FZM?>p8`-6nsh-eNUS-zWT<|<2wSs2)SddebVa>BTf#)@wsfN~nd^e+-= zh|>gCu`Sy*FgCD_u>EE7@WpksdK*u_;xX3DLRGWY)enWxN^3*JF$@p#T}c9Bz85WQdOSmQ6W0 zx2aQad7%)az3?fiF|F)ha~K@Pv^^eYo+rqjt=ttl? zSa+*~CgV?B-7ER7oc~bqC9xpnyOn%f%AaC=AN|u-yh!)u7q@V_$hubC$A(}_OiyG} z;CR&J{*m-_2xQ^@;@4^(&~`e}TLB@J>MtmXBbgFmmaJuTl5P^pNiPKybjf&;Q_>(I z!)F2b@HvG9)!o22Y~5ZGNku?*q7P_gA`{FyFJF`Y&#C|5+!Y6cUD*j3+ z!Darxt`of6|BmIU{_iGumH#`9VYg3&c}1IeqW`nur|o~o#;X6j4L(-?S4A?aGVLjK z_d8@zS|GX=*}qZC`GZwqY@DcY9`^N(Ra82y3Wqj}nnrt}JNp?vIUBSs^kT}>8@KWQ2vI6Om+w3J@ewvVh+-1P=698!|@s=4eDyj@lve<2Iww zPw4LvTH>b8G>oOAx^E7v%6{wKEGJO7TQ&i^g& z30bKBH>uGlgwaK1x@n3@Aj_X`Xe|C3_*fC3C{BVjGGdyN$4c~u2f`WpAf`WpAf`WpAf`WpAf`WpAf`WpAf`WpAf`Wp= Ohs3{A!ig{dPyhgoj@^|2 diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_002.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_002.cch.tar.gz deleted file mode 100644 index c694e880f461180310a689b7bb240cb7ae07014d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1493 zcmV;`1uFUN93cyMxGFfcMMV`FG8bYXG;?ONTBqc#xFbN&j8 zld5(F0YeD8cVzG3q)L73L;JjPz)9Tl5rGqJTJ?YL7()0m*(AG{Yj6FNBET~qk3C~% z#$**ev1Ir3yvd#{%boSMq~;hDvLo3E0VTEHdAUu3qM>{i9iR!ZC=I~!8e%(^EK_k?^)NeK zsu4(@(|8f>4cI)K#x&tw9X1(R#iZNH=`%kVsk97umf3WzZ@nGf9WH zsr>&oxF-IGEZ}b#|ECtvy77NDQ}O>6_}cN`{BNZLWy~qHHiRDoJIVIPfJivcHV`*s zgOf!>%@%!fCQoSxe-l;E<@aY05O)6gbxZqe6F#C>#ok=Qp-HD*hiN8 z4hw`>sdS${ZzSW9G8s6IT6FFVNQ&_U&$Qr)b|mVvI3~)Q_&oW7W#3?n`8IJ@zdopr>A{3X^N2X`;c{?l)!~gOPs#;jB-Kw zhG!BM9qX+%VPQBrULOJWXPuUu=YW-_U4tqLj^NXyu`+5;?oJLk&+b<1@mLVJ3 z7S^3XI|ALox?62V8GY*NUbPdY^oNQr@dcoJu!e_~_T&n)YuKEwK9d(2u6C7rlm zyzQY7=`QoZc?4Nv8!GDp`=@U1?^#a=PZ$1C{H*2c5-dGW%b55^%Zw9c(H4-vqC+f9GJJ_nlyy6vqTF)c-c_+TXFUXQ}%C7I_5(?JD% zv#+q9FVe6+|5)Ta=6Pdu@r-g73hnA}`rd>_3w9=KfWh-53?N(Yt!B(z)M)@{NI)fEjNX8e6wQIrEU<`3eU|Nl5smH*uWQu}usUpdAL`5%;fUibe$uC4z6aTAz#=$AUX64}{~ zLVA>Dh#<(C=n{TO02GLjTRK5^=6K8!j@mBr<1S_4Pw4M4#0o)WXpY=Z)zjSu9)Dov zGu+-6cV*xL;-~RHDvW$9oU{MgE5~?g|4*H1Z~r@L|K9{3kcIkZ#p4eMql@Y?(-fUR zmcQ7tNSx9?Rt-TK$0P}jh$Zx~61~kc$f$#83sQ3)28PH_>2k8xfb5{Dv@f#D-hF-5 vOG!aNK|w)5K|w)5K|w)5K|w)5K|w)5K|w)5K|w)5;oah28{_s+08jt`7Vzd> diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_003.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_003.cch.tar.gz deleted file mode 100644 index 1bad88dbb534e5b4ec4e6144f3c4e7e09870d44d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1479 zcmV;&1vvU2iwFqG_7rIV17~bsX>N93cyMxGFfcPNV`FG8bYXG;?OI)Lvo;j&b$^A$ zD@|KPVhka)?`YqPN|ScCi|x8{z)8G;iLetjoA%#ln~?Bf+9YkWP4&~NkmGag<8u!7 zgPTS6MA_!)c~w4nUNBCQCA@lXcoI<*sw;{@uX(L;g+k}uRo1$oo^4Q;V8N`eJR zfvSspr(G=$Se3=^BoU*Omhw`R+j|Eti=03mQTX^+qy!4Wg)-;*PIf>A#TosRqz(`? zm)-iFAC3?jAs?XNt2h0MBIn@u<1c889H@PR2j`^Qs#on9!+GDk-3%64F~iwNY*%EI zlDQtfU>vralOkUUyf{iD$#98HDuk``mpeIV40f`?0g8_MQ|x~(l>$D|$sb58PEwjIfbN06K_(e+_f;zf?TQbC@@E=g5pWM#o-Y5m)e z!>7YB>;Jw8&SZk8@BdyfvHb5MI4%F@F~QUGA0W^2zl-2a`R@?J9#32|O%q??f4=-} z=Rc5)5Ly0r34ApFga0WySXc5OA?&)ln<1B!%0Q2rBx}#9B%7)@n9?2zJX0(O><}}6 zrSrFUE|Nc<{PERQa<6Ai!Nk2oT~-g!u(;+{bqxC+#ZXV9J+XC?a8Rn?wt9$HB}sWRGf)M`7%SfttIF$1 z?e)~zMXw}cU9!$#+6%+@$}!{&dJ)5B24!2F-2;`kl-uHfbIyNKnuvEi{|O=#_RfFQ z|9|ZM|MB=-`+riMIaFScR2@roTpsp6EJV4IJ7iw%o3PbDXKO(Q8@OSwuXgpu-aMoo zCvry?n2EtoG&Nwty>+R)H2XB0#&WkAU>{Akfzz}s<_5x1DNVGJ+Fbi8s8R{Eigsd9 z$2W8n!=8tVpW$-R4RIwsD!xY5I9nFn6xoVcHNzoUle-#>Mm5!(4 z`YyyO9%ip3Idr;{tJ?y1ANal(?mpnnv3ujh#e6O)(u>8`;*=)+SZqxdcIZKaGiFsTgAVN-~r~ z-$QONm`B+@L2gt(XQuWra(7h~n(f2d-cSp&JqX>fR}YQ$>8*=)nV5FpAo>%F^)kGF zr-0pJQq6|g6O+j+uSb!7EmE&L=r6;*pbX}|dxdyVImWU0vsby{zds{?o{NN*3& za)W;TGCBM($aZ;^jDORez&L3wUxuD^MRv+h%HHYp+`#|NJ?0(6Ip6;X?D^kCV9bA4 z_{K3_;s28EPrKj$2z~qi--`g=fS(WSTCwvDVPIaAU{AXBvIE4jEY^!9kP^(Lrdn&& zA~gm#@cLSA@}ONc-){<<{s8{EmdllDr9akpH!E-tzNoqSSWl6S{y>gKzBXzn-=HsO!n*%U0+5*3_?)z(3APWl%3kwSi3kwSi3kwSi h3kwSi3kwSi3kwSi3kwSi3yV*Qe*jK8ey{*g00508-H`wQ diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_stackvar_001.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_stackvar_001.cch.tar.gz deleted file mode 100644 index ef540af26e4f42fcc50f078a2161dd2615be25a0..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1725 zcmV;u215BCiwFp;`4njY17~bsb97;2Yj$CBUobE+E@NY8E_7jX0PR|BZ`(Ey&S(D$ zLIsAdkS$TKcB`ZV3Je&K5Bsov4rGZ|I7^fv(m}kT|9zxnMQ@a2JBhole1Jd}?|3}& zIiAE*lJt(UFj_x^#hq!wSrpwHSFa3{!}ncrg}!UHuQjfq3r!dLj^{d8CbV7KyaMiP zJ0ioDPrm@*>K+lYJD~TR{5wS=;Xi!k2snd(Ay)if0CN6&tuKs+)A{#2wf`@J1DAoYO8MkYhmOF)T3M~Nb zk8u9c_O!9F%^OQN!&x)&XI6ToR6aqcyMA23&SN4LO(l4Z4siSk7GcMgu{}om%cn<@Q2% zM}vjS7YiNksqm!=o~h3(`CKZu{Cb9#RPOuwqRv3=h?K5eP(HNy`*feDee?;jgj^)+ z!Z&BrJlyWS$kigi%0IK6M0$^3y%Td%v%w0ZG?sZG4mYxPabCgv6d-Mv=+~#Q@$JUt z{Oa=u`d|jLsFPzQrplo2ML2I$rws|tdjCJM9(Z#7&k}d4{&xu+$Ny6i;H*mU>HM3X zqxioFPUZicOmI5?wreT=FM^pdGk&?vNpg$H`i;gY>pzZD^WDFiocm5Jm=JpW0&d^P zpAKsNi#%tC^q!M{r+Df9?^gzgUy8Qm=t7~w#c>J#pQ-=azSYbBwq={@``<X0f!@JolMz)XXt?Hm|?|V4SF~2H0ZR9=7 zr!nk){RwwV0i!Ml#&C)OUFLC9Ghb4cG1?kk+yjbZF`uSc2-cXyfG=+%YT1+(9dTJR z;f=K0ST_TV9ye97t^8mqYC)nHST&V4De6?`D*uNz1EX}L>)JMoC@6ZRA1>GwD5mYT zHN^C!v$bTit-N+>ujg7l|5bnTjPHOYS6UC|-(O+L*tRwlAF<-yC6)})7Vqa`)pPNl z7_bg7&@9~e7!pRBDb&oka?2G%66&5zclfGXWosH3BOC-MrRZ#KoXc@z*WCF3KW?NP z9Nf#c?#Ont5Or(V<9pg2-_u^b){A;i7l>^O(i^h$X2c6ex5xeHt^=3VS-1JOjF%QP zW$%CIRe8p7&i{Yiz!`cn3@%`NA@J2Ov1< zwcId7CvGfQZgDEUZr#)kQJ!TXiKi(h=%zNkr3HWFMCq1Wr7Vu7A|;~L>|Wzy8#vOw zz^Zyn9G*-tVW1~?FWS~WgMTJGX^P+Y)BeYY4Y&qB@mq1f0`J%02Dm~|WLnH+uF(7n z#3QHGx-MHqrz+EPJD(bUUnAW{a08jt`bi{Iu From b4e7f9e7ebd3e017b24f6714ecc009c675aa563f Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Jun 2026 16:16:58 -0700 Subject: [PATCH 2/3] CHC: control loglevel via cmdline option --- CodeHawk/CHC/cchcil/cCHXParseFile.ml | 5 +++-- CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml | 3 ++- CodeHawk/CHC/cchlib/cCHVersion.ml | 4 ++-- 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/CodeHawk/CHC/cchcil/cCHXParseFile.ml b/CodeHawk/CHC/cchcil/cCHXParseFile.ml index a6de253ea..b824a60e2 100644 --- a/CodeHawk/CHC/cchcil/cCHXParseFile.ml +++ b/CodeHawk/CHC/cchcil/cCHXParseFile.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny B. Sipma - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-2026 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -72,6 +72,8 @@ let speclist = [ "directory to store the generated xml files"); ("-keep_system_includes", Arg.Unit (fun () -> keep_system_includes := true), "don't filter out functions in files with an absolute path name"); + ("-loglevel", Arg.String set_log_level, + "set level for logging (default: WARNING)"); ("-keepUnused", Arg.Set keepUnused, "keep unused type and function definitions")] @@ -263,7 +265,6 @@ let save_xml_file f = let main () = try let _ = read_args () in - let _ = set_log_level "DEBUG" in let _ = cildeclarations#set_filename !filename in let cilfile = Frontc.parse !filename () in let _ = log_info "Parsed %s [%s:%d]" !filename __FILE__ __LINE__ in diff --git a/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml b/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml index 4dd890f59..6e7e764c6 100644 --- a/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml +++ b/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml @@ -135,6 +135,8 @@ let speclist = [ "disable printing timing log messages"); ("-verbose", Arg.Unit (fun () -> system_settings#set_verbose true), "print status on proof obligations and invariants"); + ("-loglevel", Arg.String set_log_level, + "set level for logging (default: WARNING)"); ("-projectname", Arg.String system_settings#set_projectname, "name of the project (determines name of results directory)"); ("-keep_system_includes", @@ -166,7 +168,6 @@ let save_log_files (contenttype:string) = let main () = try - let _ = set_log_level "WARNING" in let _ = read_args () in let _ = chlog#set_max_entry_size 1000 in let _ = log_info "AIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAI" in diff --git a/CodeHawk/CHC/cchlib/cCHVersion.ml b/CodeHawk/CHC/cchlib/cCHVersion.ml index a2f556dd2..e5e90caae 100644 --- a/CodeHawk/CHC/cchlib/cCHVersion.ml +++ b/CodeHawk/CHC/cchlib/cCHVersion.ml @@ -62,5 +62,5 @@ object (self) end let version = new version_info_t - ~version:"0.3.0_20260604" - ~date:"2026-06-04" + ~version:"0.3.0_20260606" + ~date:"2026-06-06" From 31a03dcfbdca23d09c63dc9b93229b225654a63a Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Jun 2026 22:09:14 -0700 Subject: [PATCH 3/3] CHC: redo usual arithmetic conversions --- CodeHawk/CHC/cchanalyze/cCHPOQuery.ml | 45 +++--- CodeHawk/CHC/cchlib/Makefile | 2 + .../CHC/cchlib/cCHArithmeticConversion.ml | 128 ++++++++++++++++++ .../CHC/cchlib/cCHArithmeticConversion.mli | 113 ++++++++++++++++ CodeHawk/CHC/cchlib/cCHTypesUtil.ml | 84 ------------ CodeHawk/CHC/cchlib/cCHTypesUtil.mli | 2 - .../CHC/cchpre/cCHPrimaryProofObligations.ml | 5 +- 7 files changed, 273 insertions(+), 106 deletions(-) create mode 100644 CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml create mode 100644 CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli diff --git a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml index 6bf70bfdb..f65622ba1 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml @@ -46,6 +46,7 @@ open Xsimplify open XprUtil (* cchlib *) +open CCHArithmeticConversion open CCHBasicTypes open CCHExternalPredicate open CCHFileContract @@ -1685,24 +1686,32 @@ object (self) ~ok:(fun ty1 -> TR.tfold ~ok:(fun ty2 -> - begin - match op with - | XPlus -> - Some (BinOp (PlusA, a1, a2, get_integer_promotion ty1 ty2)) - | XMinus -> - Some (BinOp (MinusA, a1, a2, get_integer_promotion ty1 ty2)) - | XMult -> - Some (BinOp (Mult, a1, a2, get_integer_promotion ty1 ty2)) - | XDiv -> - Some (BinOp (Div, a1, a2, get_integer_promotion ty1 ty2)) - | 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) + 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)) ~error:(fun err -> begin log_diagnostics_result diff --git a/CodeHawk/CHC/cchlib/Makefile b/CodeHawk/CHC/cchlib/Makefile index 1a710a38f..3a00d15b1 100644 --- a/CodeHawk/CHC/cchlib/Makefile +++ b/CodeHawk/CHC/cchlib/Makefile @@ -46,6 +46,7 @@ MLIS := \ cCHCodewalker \ cCHTypesSize \ cCHTypesUtil \ + cCHArithmeticConversion \ cCHBasicTypesXml \ cCHInterfaceDictionary \ cCHExternalPredicate \ @@ -74,6 +75,7 @@ SOURCES := \ cCHCodewalker \ cCHTypesSize \ cCHTypesUtil \ + cCHArithmeticConversion \ cCHBasicTypesXml \ cCHInterfaceDictionary \ cCHExternalPredicate \ diff --git a/CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml b/CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml new file mode 100644 index 000000000..691cfe79d --- /dev/null +++ b/CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml @@ -0,0 +1,128 @@ +(* ============================================================================= + CodeHawk C Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2005-2019 Kestrel Technology LLC + Copyright (c) 2020-2024 Henny B. Sipma + Copyright (c) 2024-2026 Aarno Labs LLC + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + 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 + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chutil *) +open CHLogger +open CHTraceResult + +(* cchlib *) +open CCHBasicTypes +open CCHTypesToPretty +open CCHUtilities + + +let p2s = CHPrettyUtil.pretty_to_string + +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + + +let get_integer_promotion (ty: typ): typ = + let promote_ikind (ik: ikind): ikind = + match ik with + | IChar | ISChar | IUChar | IShort | IBool -> IInt + | IUShort -> IUInt + | _ -> ik in + + match ty with + | TInt (ik, _) -> TInt (promote_ikind ik, []) + | TEnum (ename, _) -> + let einfo = CCHFileEnvironment.file_environment#get_enum ename in + TInt (promote_ikind einfo.ekind, []) + | _ -> + let _ = + log_diagnostics_result + ~tag:"get_integer_promotion: unexpected type" + __FILE__ __LINE__ + [p2s (typ_to_pretty ty)] in + ty + + +let usual_arithmetic_conversion (ty1: typ) (ty2: typ): typ traceresult = + + let convert_float (fk1: fkind) (fk2: fkind): fkind = + let is_complex (fk: fkind) = + match fk with + | FComplexLongDouble | FComplexDouble | FComplexFloat -> true + | _ -> false in + match fk1, fk2 with + | FComplexLongDouble, _ -> FComplexLongDouble + | _, FComplexLongDouble -> FComplexLongDouble + | FComplexDouble, _ -> FComplexDouble + | _, FComplexDouble -> FComplexDouble + | FComplexFloat, _ -> FComplexFloat + | _, FComplexFloat -> FComplexFloat + | FLongDouble, other when is_complex other -> FComplexLongDouble + | other, FLongDouble when is_complex other -> FComplexLongDouble + | FLongDouble, _ | _, FLongDouble -> FLongDouble + | FDouble, other when is_complex other -> FComplexDouble + | other, FDouble when is_complex other -> FComplexDouble + | FDouble, _ | _, FDouble -> FDouble + | FFloat, FFloat -> FFloat in + + let convert_int (ik1: ikind) (ik2: ikind): ikind = + match ik1, ik2 with + | IInt, ILong | ILong, IInt -> ILong + | IInt, ILongLong | ILongLong, IInt -> ILongLong + | ILong, ILongLong | ILongLong, ILong -> ILongLong + | IUInt, IULong | IULong, IUInt -> IULong + | _, IULongLong | IULongLong, _ -> IULongLong + | IInt, IUInt | IUInt, IInt -> IUInt + | ILong, IULong | IULong, ILong -> IULong + | IInt, IULong | IULong, IInt -> IULong + | ILong, IUInt | IUInt, ILong -> ILong + | ILongLong, IUInt | IUInt, ILongLong -> ILongLong + | IUInt128, _ | _, IUInt128 -> IUInt128 + | IInt128, _ | _, IInt128 -> IInt128 + | _ -> + (* this should not happen *) + raise + (CCHFailure + (LBLOCK [ + STR "Missing case in integer promotion: "; + STR (int_type_to_string ik1); + STR " and "; + STR (int_type_to_string ik2)])) in + + match ty1, ty2 with + | TFloat (fk1, _), TFloat (fk2, _) -> Ok (TFloat (convert_float fk1 fk2, [])) + | TFloat _, _ -> Ok ty1 + | _, TFloat _ -> Ok ty2 + | _ -> + let pty1 = get_integer_promotion ty1 in + let pty2 = get_integer_promotion ty2 in + match pty1, pty2 with + | TInt (ik1, _), TInt (ik2, _) when ik1 = ik2 -> Ok (TInt (ik1, [])) + | TInt (ik1, _), TInt (ik2, _) -> Ok (TInt (convert_int ik1 ik2, [])) + | _ -> + Error [(elocm __LINE__) + ^ "not an arithmetic type: " + ^ (p2s (typ_to_pretty ty1)) + ^ " or " + ^ (p2s (typ_to_pretty ty2))] diff --git a/CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli b/CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli new file mode 100644 index 000000000..0334fe53a --- /dev/null +++ b/CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli @@ -0,0 +1,113 @@ +(* ============================================================================= + CodeHawk C Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2005-2019 Kestrel Technology LLC + Copyright (c) 2020-2024 Henny B. Sipma + Copyright (c) 2024-2026 Aarno Labs LLC + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + 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 + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chutil *) +open CHTraceResult + +(* cchlib *) +open CCHBasicTypes + +(** The Usual Arithmetic Conversions (C Standard 6.3.1.8) + + All of the usual arithmetic conversions applied to expressions in the C + source code are supplied by the CIL parser in the form of casts. + + The implementation in this file serves to determine the result type of an + expression constructed to serve as a precondition or side effect to a + function. + *) + + +(** {1 Integer promotion: C Standard 6.3.1.1} + + The following may be used in an expression wherever an int or unsigned + int may be used: + - an object or expression with an integer type whose integer conversion + rank is less than or equal to the rank of int and unsigned int. + - a bit-field of type _Bool, int, signed int, unsigned int. + + If an int can represent all values of the original type, the value is + converted to an int; otherwise it is converted to an unsigned int. These + are called the integer promotions. All other types are unchanged by the + integer promotions. + + The integer promotions preserve value including sign. + *) + +val get_integer_promotion: typ -> typ + + +(** {1 Usual arithmetic conversions: C Standard 6.3.1.8} + + Many operators that expect operands of arithmetic type cause conversions + and yield result types in a similar way. The purpose is to determine a + common real type for the operands and result. For the specified operands, + each operand is converted, without change of type domain, to a type whose + corresponding real type is the common real type. Unless explicitly stated + otherwise, the common real type is also the corresponding real type of + the result, whose type domain is the type domain of the operands if they + are the same, and complex otherwise. This pattern is called 'the usual + arithmetic conversions'. + + First, if the corresponding real type of either operand is long double, + the other operand is converted, without change of type domain, to a type + whose corresponding real type is long double. + + Otherwise, if the corresponding real type of either operand is double, the + other operand is converted, without change of type domain, to a type + whose corresponding real type is double. + + Otherwise, if the corresponding real type of either operand is float, the + other operand is converted, without change of type domain, to a type whose + corresponding type is float. + + Other, the integer promotions are performed on both operands. Then the + following rules are applied to the promoted operands: + + If both operands have the same type, then no further conversion is needed. + + Otherwise, if both operands have signed integer types or both have unsigned + integer types, the operand with the type of lesser integer conversion rank + is converted to the type of the operand with greater rank. + + Otherwise, if the operand that has unsigned integer type has rank greater + or equal to the rank of the type of the other operand, then the operand + with signed integer type is converted to the type of the operand with + unsigned integer type. + + Otherwise, if the type of the operand with signed integer type can represent + all of the values of the type of the operand with unsigned integer type, then + the operand with unsigned integer type is converted to the type of the operand + with signed integer type. + + Otherwise, both operands are converted to the unsigned integer type + corresponding to the type of the operand with signed integer type. + *) + +val usual_arithmetic_conversion: typ -> typ -> typ traceresult diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml index 7f0fde095..d4346feec 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml +++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml @@ -418,90 +418,6 @@ let is_longlong ik = match ik with ILongLong | IULongLong -> true | _ -> false -(** {1 Integer promotion: C Standard 6.3.1.1, 6.3.1.8} - - The following may be used in an expression wherever an int or unsigned - int may be used: - - an object or expression with an integer type whose integer conversion - rank is less than or equal to the rank of int and unsigned int. - - a bit-field of type _Bool, int, signed int, unsigned int. - - If an int can represent all values of the original type, the value is - converted to an int; otherwise it is converted to an unsigned int. These - are called the integer promotions. A - - First, both types are promoted to either signed or unsigned int. - - If both operands have the same type, then no further conversion is needed. - - Otherwise, if both operands have signed integer types or both have unsigned - integer types, the operand with the type of lesser integer conversion rank - is converted to the type of the operand with greater rank. - - Otherwise, if the operand that has unsigned integer type has rank greater - or equal to the rank of the type of the other operand, then the operand - with signed integer type is converted to the type of the operand with - unsigned integer type. - - Otherwise, if the type of the operand with signed integer type can represent - all of the values of the type of the operand with unsigned integer type, then - the operand with unsigned integer type is converted to the type of the operand - with signed integer type. - - Otherwise, both operands are converted to the unsigned integer type - corresponding to the type of the operand with signed integer type. - *) - -let get_integer_promotion (ty1: typ) (ty2: typ): typ = - let promote_ikind (ik: ikind): ikind = - match ik with - | IChar | ISChar | IUChar | IShort | IBool -> IInt - | IUShort -> IUInt - | _ -> ik in - let promote_type (ty: typ): ikind = - match ty with - | TInt (ik, _) -> promote_ikind ik - | TEnum (ename, _) -> - let einfo = CCHFileEnvironment.file_environment#get_enum ename in - promote_ikind einfo.ekind - | _ -> - raise - (CCHFailure - (LBLOCK [ - STR "Unexpected types for integer promotion: "; - typ_to_pretty ty1])) in - let usual_arithmetic_conversion (ik1: ikind) (ik2: ikind): ikind = - match (ik1, ik2) with - | (IInt, ILong) | (ILong, IInt) -> ILong - | (IInt, ILongLong) | (ILongLong, IInt) -> ILongLong - | (ILong, ILongLong) | (ILongLong, ILong) -> ILongLong - | (IUInt, IULong) | (IULong, IUInt) -> IULong - | (_, IULongLong) | (IULongLong, _) -> IULongLong - | (IInt, IUInt) | (IUInt, IInt) -> IUInt - | (ILong, IULong) | (IULong, ILong) -> IULong - | (IInt, IULong) | (IULong, IInt) -> IULong - | (ILong, IUInt) | (IUInt, ILong) -> ILong - | (ILongLong, IUInt) | (IUInt, ILongLong) -> ILongLong - | (IUInt128, _) | (_, IUInt128) -> IUInt128 - | (IInt128, _) | (_, IInt128) -> IInt128 - | _ -> - raise - (CCHFailure - (LBLOCK [ - STR "Missing case in integer promotion: "; - STR (int_type_to_string ik1); - STR " and "; - STR (int_type_to_string ik2)])) in - let ik1 = promote_type ty1 in - let ik2 = promote_type ty2 in - let result_ik = - if ik1 = ik2 then - ik1 - else - usual_arithmetic_conversion ik1 ik2 in - TInt (result_ik, []) - - let rec get_field_offset offset = match offset with | NoOffset -> diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli index 581eeba0e..28eaa363c 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli +++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli @@ -65,8 +65,6 @@ val is_unsigned_type: ikind -> bool val is_character_type: ikind -> bool -val get_integer_promotion: typ -> typ -> typ - val ikind_size_leq : ikind -> ikind -> bool val const_fits_kind: constant -> ikind -> bool diff --git a/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml b/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml index b326deab3..ae2b213dc 100644 --- a/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml +++ b/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml @@ -39,6 +39,7 @@ open CHTraceResult open CHUtil (* cchlib *) +open CCHArithmeticConversion open CCHBasicTypes open CCHContext open CCHDictionary @@ -283,12 +284,12 @@ and create_po_binop | Shiftlt | Shiftrt -> (* result is undefined if second operand is negative or if second operand - is greater than or equal to the width of the first operand, + is greater than or equal to the width of the promoted left operand, ref. C99:6.5.7(3) *) begin match fenv#get_type_unrolled t with | TInt (ik,_) -> - let ty = get_integer_promotion (TInt (ik,[])) (TInt (IInt,[])) in + let ty = get_integer_promotion (TInt (ik, [])) in begin match ty with | TInt (ikp,_) ->