From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-ed1-x533.google.com (mail-ed1-x533.google.com [IPv6:2a00:1450:4864:20::533]) by sourceware.org (Postfix) with ESMTPS id 588B43858D37 for ; Tue, 21 Mar 2023 10:01:55 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 588B43858D37 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=gmail.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=gmail.com Received: by mail-ed1-x533.google.com with SMTP id x3so57300249edb.10 for ; Tue, 21 Mar 2023 03:01:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; t=1679392914; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:from:to:cc:subject:date:message-id:reply-to; bh=0OPCE3/j/kWLkBanL5VwvjF+LXBMAX3iUNV5EAMIkig=; b=JNMjHVCTxUb2z8XKCJZtAEwH+41jWxKebmp5uCA9GbsZ72jNvHkWpU7W7ODFOkNqw7 E+1+DM1XoYza/qh0AlEQBGA1SNkT7+cueec3Oq5zDm6dsHWe45885A2T/QCsAfe9erNx ktCONIr8qX32WxpFTbdvWmhQxaSMkWTtji62lrs+QYmIs4kmfzrMN0btTVq1hf5znVu/ mSB1+G9VBMVOc1mC4CFqOO5QvKu3co1Bn7mKiy/HDGQ9uHgNRtvgol6GR1FDR0VfddfY P+qFebLjuKfFsdruSJuCBmJfJRGwvSf0SGRHeOHCok3NDt+j4MrJsRY0T2t8XIlmDhJp 2cxw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1679392914; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=0OPCE3/j/kWLkBanL5VwvjF+LXBMAX3iUNV5EAMIkig=; b=6PrWeZZqiYiddBQFAYRfkQRHHoDcOMhQRRw2yYILu3suBFCop1WXSfOECl1Sn200Ke GwJpWJDCeBWeSGQLyLOC/9KlTCpP0YkB9bNWZ50KPY0HKaCTPSrnXya5TcbPUrEgXo/r 20td6u6UGWOl7XkoAO2+13BrJGBSQgbM6bH2iyClXV9Uhg08l1m++ync0RKdzG5bgkaJ Nn+z9lMGEoI31tcdnh/JLokgnAU78hBCecCH1SFk4mUnWEW3g2wAeBgIslC8/lsuvMjf +IN/T6JUAI6vS5JDCUKEQFe6kNITW0Dlblhpoaamaf4Umi+83mjK87P2pvuevmD6VoV1 S0wg== X-Gm-Message-State: AO0yUKVFVsTmkc9pdS7yNPZGc66EuTUBd2dI/LEwh0/B7409r5Dt91Uh D6TPpmpsu4sTFk1qGDe6C0g= X-Google-Smtp-Source: AK7set/DLIPVKJbEb3A8FVkEZh4NJym9XlFrt4UyeBdM5LMXBMjWbwU1mdC7ljc0Z/ehOT098bS7YA== X-Received: by 2002:aa7:cc09:0:b0:4fd:8333:e29f with SMTP id q9-20020aa7cc09000000b004fd8333e29fmr2429442edt.41.1679392913713; Tue, 21 Mar 2023 03:01:53 -0700 (PDT) Received: from smtpclient.apple ([2001:620:618:5c8:2:80b3:0:6d8]) by smtp.gmail.com with ESMTPSA id m23-20020a509317000000b004fb95f51f54sm5984087eda.12.2023.03.21.03.01.53 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 21 Mar 2023 03:01:53 -0700 (PDT) From: Shengyu Huang Message-Id: <89A3402E-023E-4EEC-A921-E9E31EC9C5B1@gmail.com> Content-Type: multipart/alternative; boundary="Apple-Mail=_CCF07093-B453-4A3A-B3CE-6DC42599913E" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.200.110.1.12\)) Subject: Re: [Static Analyzer] Loop handling - False positive for malloc-sm Date: Tue, 21 Mar 2023 11:01:41 +0100 In-Reply-To: <3b77234afb96947c9694d375b43b3096cbd45467.camel@redhat.com> Cc: Pierrick Philippe , gcc@gcc.gnu.org To: David Malcolm References: <34efc6e0-5bd8-879c-0288-154ba28f5f05@irisa.fr> <3b77234afb96947c9694d375b43b3096cbd45467.camel@redhat.com> X-Mailer: Apple Mail (2.3731.200.110.1.12) X-Spam-Status: No, score=-1.2 required=5.0 tests=BAYES_00,DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FROM,HTML_MESSAGE,RCVD_IN_DNSWL_NONE,SPF_HELO_NONE,SPF_PASS,TXREP autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org List-Id: --Apple-Mail=_CCF07093-B453-4A3A-B3CE-6DC42599913E Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Hi Dave, > I implemented my own approach, with a "widening_svalue" subclass of > symbolic value. This is widening in the Abstract Interpretation sense, > (as opposed to the bitwise operations sense): if I see multiple values > on successive iterations, the widening_svalue tries to simulate that we > know the start value and the direction the variable is moving in. I guess you are using interval domain? I haven=E2=80=99t played with abstra= ct interpretation a lot, but I think the polyhedra domain is the more popul= ar domain used (but more difficult to implement ofc). In a course project I= did before, I remember switching to polyhedra domain from the interval dom= ain allowed me to prove the properties I wanted to prove. Also, are you using the same approach maybe to detect nontermination of loo= ps? Maybe when you find out you have to widen the variable range to (minus)= infinity? >=20 > This doesn't work well; arguably I should rewrite it, perhaps with an > iterator_svalue, though I'm not sure how it ought to work. Some ideas: >=20 > * reuse gcc's existing SSA-based loop analysis, which I believe can > identify SSA names that are iterator variables, figure out their > bounds, and their per-iteration increments, etc. >=20 > * rework the program_point or supergraph code to have a notion of "1st > iteration of loop", "2nd iteration of loop", "subsequent iterations", > or similar, so that the analyzer can explore those cases differently > (on the assumption that such iterations hopefully catch the most > interesting bugs) I haven=E2=80=99t thought about how to do this properly in gcc, but maybe w= e can infer loop invariants (or even allow users to annotate loop invariant= s=E2=80=A6but I guess it would change a lot of things outside the scope of = current analyzer) that can help us do multiple checks for a loop. I have on= ly seen this strategy used on the source level before, and I don=E2=80=99t = know how difficult it will be to implement it on gimple=E2=80=A6There is a = paper I haven=E2=80=99t had the time to read but maybe you will find intere= sting: https://arxiv.org/pdf/1407.5286.pdf Best, Shengyu= --Apple-Mail=_CCF07093-B453-4A3A-B3CE-6DC42599913E--