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 4FBCB3858D37 for ; Sun, 26 Mar 2023 21:46:16 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 4FBCB3858D37 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 j24so6789586wrd.0 for ; Sun, 26 Mar 2023 14:46:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; t=1679867175; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:from:to:cc:subject:date:message-id:reply-to; bh=r4XPqIP890ruQruyc+LOkhBSLlrpe0UPsrNdSZl5SkA=; b=EBrZ361ShzLaYl7KQC/6ROdKsN2sczERpwBnQA4zRArNdXrEl3ovXWx54zCEiw5YWR Jph04XxCXy5GdVqLujn9uBaGnwKlZTyx0xYf+G595WIK2SX1FlcgE5k/9hRxRqkqNzEH VE3UcL766sWMQ/ZlQFFnZ8FUOzY9VG7XbGb9WqEhDxD0ohkOZEut0TEG5eaQbescwYjH e0B8x+FFcjM2EdNw7Sruhxr+kVB7M8AtD38LPVKoxwdEocvQM34CHRXMVG6g/zmGd5h5 q1UDkeqGaDCMuMre5VHxHG4JAJlHw8dt4XGgRqTf0GkEJPMbi+JK3JjyBMmzwMWbApKr AcrA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1679867175; 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=r4XPqIP890ruQruyc+LOkhBSLlrpe0UPsrNdSZl5SkA=; b=PWUABE+XUeIm8FlUdf0UV68iYC+pizQ3a3/ceRVhrbKvLt5+qRLchpR6tIZPFgkI1A CkH+Ex1+3Zbp53wV62RxMdN9+7rVogyuo8Q/8IObzhaC1PGFpXZSM1GgYqEDEE/R03A0 0DXotlNFsSQxvnQx1rZMCI76uCawYJC5yQWPDr7ppAHsymNLtnHPkjyz/pZNp65k/AqZ x+0Vy+JT4pVm+FWKQMv5LCIRJNihWQ4egsUvzZqagkV7Q4Hhmb5W6y1qVbPvdcytr4GN 4IG4vK3Xdu6xAibF05kYUc9+kEC/VmNDSXMr5Oswf1xjDAM0XzKeKCByV0ro4v/53LyC DpFg== X-Gm-Message-State: AAQBX9cjD9MLu60K7ax69h9jHDBiavVv01SM9KCDdqOnD3Wm3LgKsTJg VnCiGFKB8T9wODnyrfcoL+0= X-Google-Smtp-Source: AKy350acuE1sgtOUjCeUrvg1ArjXjJdb1zIEk6cxvH9vGuvnboZd4C+FvDGhjmjMD2q75X/nqJd16g== X-Received: by 2002:adf:e8cb:0:b0:2cf:efad:9c1f with SMTP id k11-20020adfe8cb000000b002cfefad9c1fmr7825630wrn.46.1679867174787; Sun, 26 Mar 2023 14:46:14 -0700 (PDT) Received: from smtpclient.apple ([213.55.222.111]) by smtp.gmail.com with ESMTPSA id d5-20020adfef85000000b002cfed482e9asm23450441wro.61.2023.03.26.14.46.14 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sun, 26 Mar 2023 14:46:14 -0700 (PDT) From: Shengyu Huang Message-Id: <0DEEAED6-46F3-4339-B600-AD35C92929B9@gmail.com> Content-Type: multipart/alternative; boundary="Apple-Mail=_E8B6D231-3B16-4E89-9986-092AC297A0FB" 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: Sun, 26 Mar 2023 23:46:02 +0200 In-Reply-To: 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> 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=_E8B6D231-3B16-4E89-9986-092AC297A0FB Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Hi Dave, > On 26 Mar 2023, at 19:14, David Malcolm wrote: >=20 > I has looked into compiling those files with the patch some time ago; > looking at my notes, one issue was with this on-stack buffer: > char extra[1024]; > declared outside the loop. Inside the loop, it gets modified in > various ways: > extra[0] =3D '\0'; > and > if (fread(extra, 1, extsize, fpZip) =3D=3D extsize) { > where the latter means "extra" becomes tainted. >=20 > However "extra" is barely used, and is effectively reset each time > through the loop - but the analyzer doesn't figure that out. So the > loop analysis explodes, as it tries to keep track of the possibility > that "extra" is still tainted from previous iteration(s), despite the > fact that it's going to be clobbered before it ever gets used. >=20 > So one fix might be to extend the state-purging code so that it somehow > "sees" that "extra" gets clobbered before it gets used, and thus we can > purge the tainted state from it. Thanks for your notes. I think we may be talking about the same thing? If y= ou look at the updated proposal (I have changed it quite a lot since I firs= t sent it out), you=E2=80=99ll see there is one relevant paper for state me= rging (although it is slightly different from state purging, I think the go= al and general methodology is similar): https://dslab.epfl.ch/pubs/stateMer= ging.pdf=20 I was trying to say if some similar situation happened for other types of c= heckers, I expected state explosion would also happen. I tried to construct= a similar example (with the same kind of reset and nested conditionals + a= loop) but for double-free, so far no success yet. I=E2=80=99ll pick it up = afterwards, at latest by next Saturday, because I need to prepare for a com= ing midterm on Friday. I will also put this test case to the proposal becau= se it seems like a very good starting point for the project. Best, Shengyu= --Apple-Mail=_E8B6D231-3B16-4E89-9986-092AC297A0FB--