From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wr1-x433.google.com (mail-wr1-x433.google.com [IPv6:2a00:1450:4864:20::433]) by sourceware.org (Postfix) with ESMTPS id 635243858D33 for ; Tue, 28 Feb 2023 14:46:30 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 635243858D33 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-wr1-x433.google.com with SMTP id r18so10046919wrx.1 for ; Tue, 28 Feb 2023 06:46:30 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:from:to:cc:subject:date:message-id:reply-to; bh=4oePcbsLIWIBJYfFYwf9HQ5nwzvK7nqW9nxuGjH/doE=; b=Zs7M8OZv7WcTL8f73FS2iMlI+jbLjBhvH4vbnHO9ueE5aJE/pEJOGwdM8cu0U7y7KK fQAghMWd+i0FyBzPFQ0QYXSjqkFhYbUQp8klT1jfThrSP1dm+85XaRec6mCQ6yvhIS2D 48D9VOCUJiCpWdLfKEEqdzIM3oXztEtv7LaelBONRKUHVHcPY/h2Ld3cjN85LHvZ1if0 9TLxn/Q92mAIovkgQnNtMBfB5Hx7eAIO/MI4VmnfoiIQa9dDxH0WrbqBKPNhsm67Wi+C lHX/1XMJ2NtWBXU48sykHYwcwrZtjPo/etpAh2dVX99a7WMkj6I+4CAJFXefAEWjXJel G53g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; 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=4oePcbsLIWIBJYfFYwf9HQ5nwzvK7nqW9nxuGjH/doE=; b=CIZ2ru6kV9Y5FBs3AbObFVHAbjdaTQsAPgntb8Q83R1nURs0uKPFOTXyUabcvkUk0x rUJhIQBd3EnF+Xx5XY3Uk1Bx032lsfw7l+L5UobDAPyOxqzJLfcA7r2wZhVpY3SjWAYL Do9CPKk1C0hKtBmxFar0U2HvV8VSL54+9P70Rdoa9LHHgP72krOJLVBYk8VijEm/gxB8 lAxtckZN6L+F0aNQ+Yu/kmWhN/cklkQLr7Vf30c+hZfGCyxz7KAzph9UwbeXPykmPe7b f5De9TuLv/Q77+S6hNWZUPZgpC7ZWrWwqCklx0GTNOejYB916w+1AW6ORuQxxb7igrU3 hR0Q== X-Gm-Message-State: AO0yUKX7tTW2QD+QSog+2WARc8Pg/JJfzqDZnjQ/fKutyEn93esVwYPe VThRWaqZJMD8xAueqJEa+t4= X-Google-Smtp-Source: AK7set9pBNm0aDXF+9TkC0tM6C7bQ1lCe/UbpVREWf/k9IOG5IcLPRJzZRzXTqqkX44jI9WdwR9V9g== X-Received: by 2002:a5d:6e09:0:b0:2c7:5247:e496 with SMTP id h9-20020a5d6e09000000b002c75247e496mr2286642wrz.60.1677595588560; Tue, 28 Feb 2023 06:46:28 -0800 (PST) Received: from smtpclient.apple ([213.55.226.53]) by smtp.gmail.com with ESMTPSA id bi13-20020a05600c3d8d00b003e204fdb160sm16145949wmb.3.2023.02.28.06.46.27 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 28 Feb 2023 06:46:28 -0800 (PST) From: Shengyu Huang Message-Id: Content-Type: multipart/alternative; boundary="Apple-Mail=_E23F7D99-6C67-4DAC-8221-E3439887E60A" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.200.110.1.12\)) Subject: Re: [GSoC][Static Analyzer] Ideas for proposal Date: Tue, 28 Feb 2023 15:46:16 +0100 In-Reply-To: Cc: GCC Development To: David Malcolm References: <960EE623-1B17-4321-B77E-FBCD9496BE1F@gmail.com> <40fbb064f56845908f797400e5d9443b6cf97fe4.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,KAM_SHORT,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=_E23F7D99-6C67-4DAC-8221-E3439887E60A Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Hi Dave, > On 22 Feb 2023, at 15:11, Shengyu Huang wrote: >=20 >> But a better place to look would probably be in our bugzilla; see the >> links on the wiki page: >> https://gcc.gnu.org/wiki/StaticAnalyzer=20 >> The "open bugs" list currently has 41 "RFE" bugs ("request for >> enhancement" i.e. ideas for new features), some of which might make >> suitable GSoC ideas, and/or be of interest to you (ideally both!) >>=20 >> Also, the GSoC wiki page has some project ideas: >> https://gcc.gnu.org/wiki/SummerOfCode#Selected_Project_Ideas >>=20 >=20 > Yeah I was also searching for interesting ideas on the bugzilla, and I wi= ll communicate to you once I have any more concrete ideas. I spent some time searching through Bugzilla this weekend while familiarizi= ng with the analyzer internals, and I found the following things interestin= g, and it=E2=80=99d be great if you can give me some preliminary feedback: 1. I am not sure why we added the class `shift_count_negative_diagnostic` i= n region-model.cc , because there is a similar war= ning issued from c/c-typeck.cc , and when I compiled w= ith -fanalyzer that has the code `b =3D b << -1`, I got two warnings that m= ean the same thing. Maybe interestingly, when I compiled my test case with = -O2, I got the warning from -Wshift-count-negative but not from -Wanalyzer-= shift-count-negative. Would it be considered as a false negative for the an= alyzer?=20 2. Something related to 1. is PR98447 (https://gcc.gnu.org/bugzilla/show_bu= g.cgi?id=3D98447) 3. PR104955 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=3D104955) still t= akes a long without -Wno-analyzer-double-free. I=E2=80=99d be interested in= further investigating the problem (probably as you said sharing one feasib= le_graph can fix the problem). 4. What=E2=80=99s the most interesting to me are PR103533 (https://gcc.gnu.= org/bugzilla/show_bug.cgi?id=3D103533), PR104940 (https://gcc.gnu.org/bugzi= lla/show_bug.cgi?id=3D104940) because I focus on formal methods in my unive= rsity studies, and I=E2=80=99m currently looking into Dafny internals for m= y semester project. 5. PR105891 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=3D105891) seems f= itted to get started during the project phase, or be used as a warm-up befo= re the official project phase. 6. PR106147 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=3D106147) says yo= u are implementing a prototype already, so I guess I=E2=80=99ll leave it ou= t, but I am also quite interested in this analysis. At a glimpse I am not q= uite sure why infinite recursion and infinite loop should be treated differ= ently (maybe it=E2=80=99ll become clearer to me once I am more familiar wit= h the internals). In addition, a simple function that looks like this void re (int c) { if (c > 0) re (c + 1); else re (1); } can also be concluded as infinite recursion because there is no base case i= n all possible paths. 7. Other PRs that interest me: PR106006 (https://gcc.gnu.org/bugzilla/show_= bug.cgi?id=3D106006) and PR107017 (https://gcc.gnu.org/bugzilla/show_bug.cg= i?id=3D107017, already mentioned in the GSoC page). Best, Shengyu --Apple-Mail=_E23F7D99-6C67-4DAC-8221-E3439887E60A--