From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-ed1-x52c.google.com (mail-ed1-x52c.google.com [IPv6:2a00:1450:4864:20::52c]) by sourceware.org (Postfix) with ESMTPS id 697AA3858CDB for ; Mon, 3 Apr 2023 00:03:03 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 697AA3858CDB 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-x52c.google.com with SMTP id x3so110639801edb.10 for ; Sun, 02 Apr 2023 17:03:03 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; t=1680480180; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:from:to:cc:subject:date:message-id:reply-to; bh=FMLQTRB/aJPsvSsmjDuXjJRGR1l2i9IpmOx0t4taxL0=; b=N0f1OdfE1LH4pk73DKlxTDtH/P867IGYlSUkt7RGkwQu7rCTyzHnthyCA2yDdSPNCQ l5xZbvgvxpB7cMY4t4ITsdUjZ4tVpW8IFMUVfTs7wowoXSypHjD6sF4slf/rMAWzKH7u FMo7JqxOIAmmgBm8/Rxoa785Yy7CWhSFzQ2se1zdE7b7WyB1SFbqPIse45HI+Eb9Jx1G gdQEqyekHNdXTOjLL+ViAbjhW/n5tAA6ywp4Q1+CFMFovbZCNL+hINmQd1C4SVhxuLfU x5Y846sH+clOPPQtjWDsH2rwY4Ge/W0bCccE5jVmzyCEsG0HaNVubo0rLDXR4HgE9psr QugQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1680480180; 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=FMLQTRB/aJPsvSsmjDuXjJRGR1l2i9IpmOx0t4taxL0=; b=Dd7PjZ76/L+Rb/8DXHG8spcQbHAxFzdkR26bvaIyNnVXf7GaxNr2zpjUJpo69Fa65f u1kQkvTWDda7B8N9TcgKbT+RPNpXZQm79wSfsBHs31J/bcid+E7AMmhpIl/fsb7BhiNj TIgekopr/AHvk4VowJeHu9Kb2gw/aBxkFuBz36U8kHL1crwE0+IKudmfrZ+EQkEWMJUi 7T0qDJBw59eobDiFonJTr06KM98WiWkfC1ll1Aph5U4xrMgBL7yPXko14yPxQbVDkjtI vsReb1TFnIOikSF4n8o5xAiIwMexY/NuSAyRbLsD5gnI7+fu3P3gGsAN8TgX+NewDJa9 0/YQ== X-Gm-Message-State: AAQBX9evqOeIMMyZzIB/Orcpwlg6/mF1XSZCIK1R5oo/W6JypRy64y1u PjO4KMSMnDcqNIHvEcgbpe414iCt4v2KNw== X-Google-Smtp-Source: AKy350Z6x34LO2s3i53GefcQ0fHT0WvlPj+cGUifi0Kkl1J/+65p3stW6kYJ2t+io/G8r2Lca19uLA== X-Received: by 2002:a17:907:2063:b0:92e:d6e6:d8a4 with SMTP id qp3-20020a170907206300b0092ed6e6d8a4mr33946689ejb.44.1680480180278; Sun, 02 Apr 2023 17:03:00 -0700 (PDT) Received: from smtpclient.apple ([213.55.224.44]) by smtp.gmail.com with ESMTPSA id qb3-20020a1709077e8300b00947d49ec819sm2885448ejc.22.2023.04.02.17.02.59 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sun, 02 Apr 2023 17:02:59 -0700 (PDT) From: Shengyu Huang Message-Id: Content-Type: multipart/alternative; boundary="Apple-Mail=_790B7407-4127-4009-8F7B-207FC89678CA" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.200.110.1.12\)) Subject: Re: [GSoC][Static Analyzer] First proposal draft and a few more questions/requests Date: Mon, 3 Apr 2023 02:02:48 +0200 In-Reply-To: <8c9a526ae6ce6868d21da887ee5cecd5c5fa28ac.camel@redhat.com> Cc: GCC Development To: David Malcolm References: <960EE623-1B17-4321-B77E-FBCD9496BE1F@gmail.com> <40fbb064f56845908f797400e5d9443b6cf97fe4.camel@redhat.com> <0e6a972dac60ad290d21a82b428cc76c4e8565e9.camel@redhat.com> <4CBE37A2-7D50-4ECC-9B70-951AB7176D9B@gmail.com> <3dfad33dec50c9f8bfb13e42a29cfb41b6aab457.camel@redhat.com> <2344350B-6AD2-46A5-A335-BD3ECBBAA4DF@gmail.com> <0BED8B95-9F1A-4350-A63C-616D31E405C3@gmail.com> <0DEEAED6-46F3-4339-B600-AD35C92929B9@gmail.com> <7B619AA7-C42D-4486-8017-72BB54297005@gmail.com> <8c9a526ae6ce6868d21da887ee5cecd5c5fa28ac.camel@redhat.com> X-Mailer: Apple Mail (2.3731.200.110.1.12) X-Spam-Status: No, score=-1.3 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=_790B7407-4127-4009-8F7B-207FC89678CA Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Hi Dave, > Overall, it looks great. Some notes: > - maybe specify the *GCC* static analyzer you first mention it Done. > - you talk about "timeout" warnings. The analyzer already can emit a > "timeout" warning of sorts, via -Wanalyzer-too-complex, though this is > based on the complexity of the exploded graph (e.g. # of nodes), rather > than actual timings. Is the latter the kind of thing you had in mind, > or where you thinking about ways of making the "too complex" heuristics > smarter? (I confess that you seem much more familiar with the theory > of this than I am!) I was not ware of `-Wanalyzer-too-complex` when I wrote that proposal, and = I forgot to rewrite this part. I planned to ask you why we did not turn on = this flag by default. To avoid state explosion altogether, it is for sure t= hat we need to bear with false positives in some cases. I am not yet sure w= hat is a good approach to balance the soundness and completeness in symboli= c execution, but my intuition (just based on my limited experience with oth= er kinds of formal methods) is that we don=E2=80=99t want to avoid state ex= plosion in all cases because we want to have more precision (that is, we do= n=E2=80=99t want too many false positives). Imagine a dummy static analyzer= that just reports warnings regardless the program. It will not have any st= ate explosion problems, but it will have lots of false positives. Therefore= , I think we should consider turning it on by default. Maybe you have other= considerations that I missed? Another point but irrelevant for this project is that we will surely encoun= ter timeout when we integrate SMT solvers in the future (I don=E2=80=99t kn= ow whether it is the plan for GCC14). It is just unavoidable=E2=80=A6the cu= rrent approach does not sound transferable to the timeout issued by, say, Z= 3. Maybe we want a unified approach at some point? Anyway, this part does not seem too urgent anymore after I know the flag -W= analyzer-too-complex exists=E2=80=A6if you have some working solution in te= rms of how to handle timeout from SMT solvers, I=E2=80=99d be happy to know. > - the numbering of your references seems to have gotten out-of-sync; I > see references to [3] as a paper "Schwartz et al", but that's a link to > one of my blog posts. Thanks for letting me know that. Indeed I forgot to fix the numbering after= adding your blog to the references. > - do you a link to a github account, or somewhere else that > demonstrates code you've written? In particular, how is your C++ ? >=20 My Github account is https://github.com/kumom, but I would not post any cod= e from my course projects there since it will violate honor code and promot= e plagiarism (I will attach a small? lab project to you in another private = email). I have taken courses like systems programming and computer architec= ture, where I wrote plenty of C code and some C++ code. For C++, I=E2=80=99= ve written maybe just a few thousand lines of code. Unfortunately, in all m= y previous jobs as student assistant where I coded mainly in Python and Typ= eScript, my code was neither open source nor owned by me=E2=80=A6Now I am w= orking on a semester project (on formal verification) using Dafny and a cou= rse project (on compiler design) using Scala, but I admit they are a bit fa= r from C++. I have planned to read Effective C++ after the Easter break bef= ore you raised this question, but maybe you can recommend something else th= at you find helpful. Since I am relative familiar with programming language= concepts in general, I believe I will get more fluent at C++ within a shor= t amount of time once I get my hands dirty. > Note that the deadline for submitting proposals to the official GSoC > website is April 4 - 18:00 UTC (i.e. this coming Tuesday) and that > Google are very strict about that deadline; see: > https://developers.google.com/open-source/gsoc/timeline Thanks for the reminder. I have kept this in mind and will submit it before= the deadline. Best, Shengyu --Apple-Mail=_790B7407-4127-4009-8F7B-207FC89678CA--