From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) by sourceware.org (Postfix) with ESMTPS id 3E7563858433 for ; Wed, 22 Mar 2023 18:34:55 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 3E7563858433 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=redhat.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=redhat.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1679510094; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=mcDXv46PsfkvPuVM7NzIi4P1Qp4Nkw/LUX/6lbRtnDc=; b=gi4AYmc3SEJR4b5TEazwIA/6wR38zJlOq2NK+FS/AXrYgX/vdUzRx03m2d5/ec1GIc58t8 3Ggo8WzclRLrHC0aMO5v0R+k7Wyp+JbaMyGtqX1XNM1A2inVAzCMcymfZ5SP9Mixrw0p3w s85iYzjO/OKrgI/6SyXvx/c6MpVSPD0= Received: from mail-qk1-f198.google.com (mail-qk1-f198.google.com [209.85.222.198]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-70-n7lChVgoMx-SOt59whraqw-1; Wed, 22 Mar 2023 14:34:53 -0400 X-MC-Unique: n7lChVgoMx-SOt59whraqw-1 Received: by mail-qk1-f198.google.com with SMTP id b34-20020a05620a272200b007460c05a463so9165630qkp.1 for ; Wed, 22 Mar 2023 11:34:53 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1679510093; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=mcDXv46PsfkvPuVM7NzIi4P1Qp4Nkw/LUX/6lbRtnDc=; b=6qTm9PHX94Oi6Tcz+Mm0F8mRB9JP2jM54fhCoiEuGU+aGQ+DhATXU8XqKNgDD1UpaL ZfcKq7XSRgAS2Kt8ir+vcMsOaqm4Lu+JAHUfqy+bSqChD7EAFyZFXqUpD3AeuVRoSPKg qD/88YC7e9F+M5DJ1DIgPG9ariozRfveSxUvkjx5UTdpeU+zXgMqZN9zt1/o/Foyy5aW 3X4XFPqbkt6co+xRAmVR+S1+4zn7P6GJ4ZUn4Fa/uss22SRGT6ih0Y91Gw6faLduJEfI QI/KMuS9PkMCR08QDmrwrrxIPrOPxvdL7GPvMBXm2pzy3cP+Uvao125i4yueMvwDnqLE cLqQ== X-Gm-Message-State: AO0yUKVygZfln2m/XxcEes3Xoci8cphomMhqw/5wRqSwnLZ3xYX9w4QY IprVtnXQP8c1+AqsLqJebcN4jLxoM7neLwjcZJgX0onIB0L/Zr6JGh8vqebPUPHj/rsCcfsEGsp JfdXwJns= X-Received: by 2002:a05:622a:408:b0:3e0:5cb5:5152 with SMTP id n8-20020a05622a040800b003e05cb55152mr7687155qtx.49.1679510093226; Wed, 22 Mar 2023 11:34:53 -0700 (PDT) X-Google-Smtp-Source: AK7set/KpFqCA6nr1TQjTWjJuJbukkZBDCyIZ7+1ngU2Fp4rn1nCtk1Ezqu9L7uLFScp9ORGUc2l1w== X-Received: by 2002:a05:622a:408:b0:3e0:5cb5:5152 with SMTP id n8-20020a05622a040800b003e05cb55152mr7687126qtx.49.1679510092946; Wed, 22 Mar 2023 11:34:52 -0700 (PDT) Received: from t14s.localdomain (c-73-69-212-193.hsd1.ma.comcast.net. [73.69.212.193]) by smtp.gmail.com with ESMTPSA id c9-20020ac85189000000b003e36de2c4b8sm4669779qtn.85.2023.03.22.11.34.52 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 22 Mar 2023 11:34:52 -0700 (PDT) Message-ID: <8ee3849b1aa966ad524de8f7817b78597337f431.camel@redhat.com> Subject: Re: [Static Analyzer] Loop handling - False positive for malloc-sm From: David Malcolm To: Shengyu Huang Cc: Pierrick Philippe , gcc@gcc.gnu.org Date: Wed, 22 Mar 2023 14:34:51 -0400 In-Reply-To: <89A3402E-023E-4EEC-A921-E9E31EC9C5B1@gmail.com> References: <34efc6e0-5bd8-879c-0288-154ba28f5f05@irisa.fr> <3b77234afb96947c9694d375b43b3096cbd45467.camel@redhat.com> <89A3402E-023E-4EEC-A921-E9E31EC9C5B1@gmail.com> User-Agent: Evolution 3.44.4 (3.44.4-1.fc36) MIME-Version: 1.0 X-Mimecast-Spam-Score: 0 X-Mimecast-Originator: redhat.com Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Spam-Status: No, score=-5.7 required=5.0 tests=BAYES_00,DKIMWL_WL_HIGH,DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,KAM_SHORT,RCVD_IN_DNSWL_NONE,RCVD_IN_MSPIKE_H2,SPF_HELO_NONE,SPF_NONE,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: On Tue, 2023-03-21 at 11:01 +0100, Shengyu Huang wrote: > Hi Dave, >=20 > > I implemented my own approach, with a "widening_svalue" subclass of > > symbolic value.=C2=A0 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. >=20 > I guess you are using interval domain? I haven=E2=80=99t played with abst= ract > interpretation a lot, but I think the polyhedra domain is the more > popular domain used (but more difficult to implement ofc). In a > course project I did before, I remember switching to polyhedra domain > from the interval domain allowed me to prove the properties I wanted > to prove. Sorry if what I wrote was misleading: I'm not using abstract interpretation per se; the analyzer is doing symbolic execution. It uses a worklist to explore the exploded_graph of (point, state) pairs, but I have quite complicated state objects. What I mean is that the widening_svalue is an abstraction, and the hope is that it will get reused within the program_state object for representing the state of the loop variant the next time through the loop, and thus the program_state is the same as the previous iteration, and thus we effectively have a cache hit within the exploded_graph (and can terminate the analysis). I see this as somewhat analogous to the convergence that happens in an abstract interpretation approach, in that we go from the: - initial value - widened to cover range from initial value up to +infinity and thus (hopefully) terminate in two steps. But it doesn't work very well, alas. As noted in another thread, I've just filed: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=3D109252 with some ideas on better ways of handling loops in the analyzer. >=20 > Also, are you using the same approach maybe to detect nontermination > of loops? Maybe when you find out you have to widen the variable > range to (minus) infinity? For GCC 13 I've added a warning: -Wanalyzer-infinite-recursion implemented in gcc/analyzer/infinite-recursion.cc which attempts to detect infinite *recursions* based on states being too similar when recursing: if nothing can have effectively changed, it's an infinite recursion (for some definition of "effectively). I'd hoped to implement something similar for *loop* detection, but it didn't make feature freeze for GCC 13; see: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=3D106147 The half-finished prototype I have works in a similar way to the recursion detection: find loops such as: for (int i =3D 0; i < 10; i++) for (int j =3D 0; j < 10; i++) { } where due to the copy-and-paste error of reusing "i++", "j" never changes after entering the inner loop, and we never leave it. >=20 > >=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.=C2=A0 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) >=20 > I haven=E2=80=99t thought about how to do this properly in gcc, but maybe= we > can infer loop invariants (or even allow users to annotate loop > invariants=E2=80=A6but I guess it would change a lot of things outside th= e > scope of current analyzer) that can help us do multiple checks for a > loop. I have only 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 bu= t maybe you > will find interesting: https://arxiv.org/pdf/1407.5286.pdf Thanks! Dave