From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-ed1-x529.google.com (mail-ed1-x529.google.com [IPv6:2a00:1450:4864:20::529]) by sourceware.org (Postfix) with ESMTPS id E46C73857829; Thu, 18 Mar 2021 12:27:19 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.3.2 sourceware.org E46C73857829 Received: by mail-ed1-x529.google.com with SMTP id u4so6380760edv.9; Thu, 18 Mar 2021 05:27:19 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=fqsxWTc7JDPC4FDkjLBSto9Am8TFWsdIxQS2s7cW0OQ=; b=bjtkGebzWvIQCFMNB1nXTxp1C/KCU+vosqS1JN/wiL7ksTFn1nind9RXXDIFkbGbhK WMucxqBgiy6NfqYXtgPlZjdovH+X5BlTqfJbPghyHtOiutvngCBzpWjU+bL2av8zxEtx Yt6hVZt1xoc64N0hls24ilOzuT3fDcek6EzQjQd+AOus56T8gQ1gTYbzGfoGng6rOWSl JQtr631u+EbEuoL/wuWSx3fUArzhAprcQBCOOpBThoEDCS6E6U4zbzYf8VDdGKMuEvff EtFAezM1Dg6ph64urwjT8UiGfaowJh14RGm3ptHuCHiiilPKw2lzLNq4WS37XylCfL79 HXoQ== X-Gm-Message-State: AOAM531fitAjxHcBqYrOcEIJjeKgTuFsHmiR3Ni5pAuD/p8zb0LlUaBs 0bXKLBkAvyE/RS8taMUYfUe4VSPo/Unob0Ew5i6gq5ue X-Google-Smtp-Source: ABdhPJz077EMfuvC8sW2OQ3kmYXZc4IzAVJKOT+91TLGXZFfJg7dbl1iYQi42lekWp42v/jFj1CBLLG8iIq5S93ot9I= X-Received: by 2002:a05:6402:3075:: with SMTP id bs21mr3345560edb.274.1616070438639; Thu, 18 Mar 2021 05:27:18 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Richard Biener Date: Thu, 18 Mar 2021 13:27:07 +0100 Message-ID: Subject: Re: More questions on points-to analysis To: Erick Ochoa Cc: GCC Development Content-Type: text/plain; charset="UTF-8" X-Spam-Status: No, score=-3.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, FREEMAIL_FROM, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.2 X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on server2.sourceware.org X-BeenThere: gcc@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 18 Mar 2021 12:27:21 -0000 On Wed, Mar 17, 2021 at 4:17 PM Erick Ochoa wrote: > > Hi Richard, I think I misunderstood yesterday's answer and deviated a > little bit. But now I want to focus on this: > > > > * the process in GCC that generates the constraints for NULL works > > > fine (i.e., feeding the constraints generated by GCC to an external > > > solver should yield a conservatively correct answer) but the process > > > that solves the constraints relaxes the solutions for the NULL > > > constraint variable (i.e., GCC has deviated from the constraint > > > solving algorithm somehow) > > > > No, that part should work OK. > > > > So, let's ignore the other solver for now and instead focus on the > concrete example I presented on the previous email. If GCC is solving > these constraints: > > ``` > ANYTHING = &ANYTHING > ESCAPED = *ESCAPED > ESCAPED = ESCAPED + UNKNOWN > *ESCAPED = NONLOCAL > NONLOCAL = &NONLOCAL > NONLOCAL = &ESCAPED > INTEGER = &ANYTHING > ISRA.4 = &NONLOCAL > derefaddrtmp(9) = &NULL > *ISRA.4 = derefaddrtmp(9) > i = NONLOCAL > i = &NONLOCAL > ESCAPED = &NONLOCAL > _2 = *ISRA.4 > ``` > > What would a hand calculated solution gives us vs what was the > solution given by GCC? > > I am following the algorithm stated on Section 3.3 of Structure > Aliasing in GCC, and I will be ignoring the ESCAPED = ESCAPED + > UNKNOWN constraint since there isn't any other field offset that needs > to be calculated. > > First, I want to make some adjustments. I am going to be using "=" to > signify the \supseteq symbol and I will be adding curly braces to > specify the element in a set as opposed to the whole set. Therefore > the constraints will now become (ordered slightly differently): > > ``` > ====direct contraints======== > ANYTHING = { ANYTHING } > ESCAPED = { NONLOCAL } > NONLOCAL = { NONLOCAL } > NONLOCAL = { ESCAPED } > INTEGER = { ANYTHING } > ISRA.4 = { NONLOCAL } > derefaddrtmp(9) = { NULL } > i = { NONLOCAL } > > ====complex constraints====== > ESCAPED = *ESCAPED > *ESCAPED = NONLOCAL > *ISRA.4 = derefaddrtmp(9) > _2 = *ISRA.4 > > ===== copy-constraints====== > ESCAPED = ESCAPED // again ignoring the + UNKNOWN since I don't think > it will matter... > i = NONLOCAL > ``` > > Solution sets are basically the direct constraints at the moment. > > Let's now create the graph > > 1. node ESCAPED has an edge going to itself (due to the copy constraint) > 2. node ISRA.4 has no outgoing copy edges > 3. node derefaddrtmp(9) has no outgoing edges > 4. node _2 has no outgoing edges > 5. node i has an outgoing edge to NONLOCAL (due to the copy constraint) > 6. node NONLOCAL has no outgoing edge > > Now, we can iterate over this set of nodes > > 1. Walking over node ESCAPED. Sol(ESCAPED) = {NONLOCAL}. There are no > edges, but it has complex-constraints. Let's modify the graph. > 1. Looking at ESCAPED = *ESCAPED we note that we need to add a copy > edge from ESCAPED to NONLOCAL. > 2. Looking at *ESCAPED = NONLOCAL we note that we need to add a copy > edge from NONLOCAL to NONLOCAL > > The graph is now transformed to > > 1. node ESCAPED has an edge going to ESCAPED and NONLOCAL > 2. node ISRA.4 has no outgoing copy edges > 3. node derefaddrtmp(9) has no outgoing edges > 4. node _2 has no outgoing edges > 5. node i has an outgoing edge to NONLOCAL (due to the copy constraint) > 6. node NONLOCAL has an edge going to NONLOCAL > > The solution set of escaped is now Sol(ESCAPED) = Sol(ESCAPED) U > Sol(NONLOCAL) = {NONLOCAL, ESCAPED} > > Now we continue walking > > 2. Walking over node ISRA.4. It has the solution set { NONLOCAL }. > There are no edges, but it has complex-constraints. Let's modify the > graph. > 1. Looking at *ISRA.4 = derefaddrtmp(9), we note that we need to add > a copy edge from NONLOCAL to derefaddrtmp(9). > > The graph is now transformed to > > 1. node ESCAPED has an edge going to ESCAPED and NONLOCAL > 2. node ISRA.4 has no outgoing copy edges > 3. node derefaddrtmp(9) has no outgoing edges > 4. node _2 has no outgoing edges > 5. node i has an outgoing edge to NONLOCAL (due to the copy constraint) > 6. node NONLOCAL has an edge going to NONLOCAL, derefaddrtmp(9) > > The Sol(NONLOCAL) = Sol(NONLOCAL) U Sol(derefaddrtmp(9)) = {NONLOCAL, > ESCAPED, NULL}. > > Now I could continue, but here is already something that is not shown > in the points-to sets in the dump. It shows that > > NONLOCAL = {NONLOCAL, ESCAPED, NULL} > > Looking at the data that I showed yesterday: > > ``` > NONLOCAL = { ESCAPED NONLOCAL } same as i > ``` > > we see that NULL is not in the solution set of NONLOCAL. > > Now, yesterday you said that NULL is not conservatively correctly > represented in the constraints. You also said today the points-to > analysis should be solving the constraints fine. What I now understand > from this is that while NULL may be pointed to by some constraints, it > doesn't mean that not being on the set means that a pointer will not > point to NULL. However, it should still be shown in the dumps where > the points-to sets are shown for the constraint variables since it is > solved using the same analysis? Is this correct? Am I doing the points > to analysis by hand wrong somehow? Why would NULL not be in > Sol(NONLOCAL) if it is solving the same constraints that I am solving > by hand? Because NONLOCAL is a special var and those do not get "solved". Their points-to set is fixed. NONLOCAL is the set of "global" variables _at function entry_ (otherwise it would be the same as ESCAPED). Richard.