More comprehensively check whether a GEP edge can induce a GEP object by mbarbar · Pull Request #1870 · SVF-tools/SVF

mbarbar · 2026-07-11T06:27:18Z

No description provided.

yuleisui · 2026-07-11T06:31:14Z

+        // If we aren't treating the first field as equivalent to the base, no matter the
+        // offset, we may induce a GEP object. If the field index isn't 0, no matter how we
+        // treat the first field (0), we may induce a GEP object.
+        return !Options::FirstFieldEqBase() || 0 != normalGepCGEdge->getConstantFieldIdx();


Could we do the opposite way for the condition to make it intuitive?

If(Options::FirstFieldEqBase() && 0==normalGepCGEdge->getConstantFieldIdx())

Return false

Done, if you could take a look again.

yuleisui · 2026-07-11T06:56:37Z

Would be good to also include your test case (rational for this pr) in https://github.com/SVF-tools/Test-Suite/tree/master/src/basic_c_tests

mbarbar · 2026-07-11T08:13:08Z

Would be good to also include your test case (rational for this pr) in https://github.com/SVF-tools/Test-Suite/tree/master/src/basic_c_tests

I'm looking at the 0 AP offset and believe the test has far larger issues. I think we can add the test after that is sorted. I believe it to be a coincidence that this issue showed up from that test case in the sense that if we didn't have the AP offset problem, this ff-eq-base stuff wouldn't have happened.

mbarbar · 2026-07-19T09:28:48Z

I was able to reduce the failing stack program to

%"class.std::stack" = type { %"class.std::deque" }
%"class.std::deque" = type { %"class.std::_Deque_base" }
%"class.std::_Deque_base" = type { %"struct.std::_Deque_base<A, std::allocator<A>>::_Deque_impl" }
%"struct.std::_Deque_base<A, std::allocator<A>>::_Deque_impl" = type { %"struct.std::_Deque_base<A, std::allocator<A>>::_Deque_impl_data" }
%"struct.std::_Deque_base<A, std::allocator<A>>::_Deque_impl_data" = type { ptr, i64, %"struct.std::_Deque_iterator", %"struct.std::_Deque_iterator" }
%"struct.std::_Deque_iterator" = type { ptr, ptr, ptr, ptr }
%"class.std::allocator.0" = type { i8 }

define dso_local noundef i32 @main()  {
  %6 = alloca ptr, align 8
  %13 = getelementptr inbounds %"class.std::stack", ptr %6, i32 0, i32 0
  %18 = getelementptr inbounds %"class.std::_Deque_base", ptr %13, i32 0, i32 0
  %21 = load ptr, ptr %18, align 8
  %n = call noalias noundef nonnull ptr @_Znwm(i64 noundef 19)
  store ptr %n, ptr %21, align 8
  call void @baz(ptr noundef nonnull align 8 dereferenceable(32) %18, ptr noundef %21)

  %99 = alloca %"class.std::allocator.0", align 1
  %105 = getelementptr inbounds ptr, ptr %99, i64 104
  call void @baz(ptr noundef nonnull align 8 dereferenceable(32) %105, ptr noundef %105)

  ret i32 2
}

define linkonce_odr dso_local void @baz(ptr noundef nonnull align 8 dereferenceable(32) %0, ptr noundef %1) {
  %7 = getelementptr inbounds %"struct.std::_Deque_iterator", ptr %0, i32 0, i32 3
  %19 = load ptr, ptr %1, align 8
  store ptr %1, ptr %7, align 8
  ret void
}

declare noundef nonnull ptr @_Znwm(i64 noundef)

nander initial and final constraint graph:

ander initial and final constraint graph:

The diff for nander and ander top-level points-to sets is

30c30
< NodeID 35 		PointsTo: { 15 1024 }
---
> NodeID 35 		PointsTo: { 1024 }

Everything run with -node-alloc-strat=debug.

I guess the main thing is that in ander, the cycle 13->32->1008 is collapsed. I'm not fully sure why there is an edge 14:n->1024 in nander but not in ander.

mbarbar · 2026-07-21T02:23:46Z

nander:

----------------------------------------------
##<> Source Loc: { constant data }
Ptr 0 		PointsTo: {empty}

----------------------------------------------

Ptr 1 		PointsTo: {empty}

----------------------------------------------
##<Dummy Obj > id:2
Ptr 2 		PointsTo: {empty}

----------------------------------------------
##<Dummy Obj > id:3
Ptr 3 		PointsTo: {empty}

----------------------------------------------
##<main> Source Loc: 
Ptr 4 		PointsTo: { 5 }

!!Target NodeID 5	 [<main> Source Loc: ] 
----------------------------------------------
##<main> Source Loc: 
Ptr 5 		PointsTo: {empty}

----------------------------------------------
##<main> Source Loc: 
Ptr 6 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 7 		PointsTo: { 8 }

!!Target NodeID 8	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 8 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { constant data }
Ptr 9 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<> Source Loc: 
Ptr 10 		PointsTo: { 1008 }

!!Target NodeID 1008	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: { constant data }
Ptr 11 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<> Source Loc: 
Ptr 12 		PointsTo: { 1008 }

!!Target NodeID 1008	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 13 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<n> Source Loc: 
Ptr 14 		PointsTo: { 15 }

!!Target NodeID 15	 [<n> Source Loc: ] 
----------------------------------------------
##<n> Source Loc: 
Ptr 15 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { constant data }
Ptr 16 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<_Znwm> Source Loc: 
Ptr 17 		PointsTo: { 18 }

!!Target NodeID 18	 [<_Znwm> Source Loc: ] 
----------------------------------------------
##<_Znwm> Source Loc: 
Ptr 18 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 19 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 20 		PointsTo: {empty}

----------------------------------------------
##<baz> Source Loc: 
Ptr 21 		PointsTo: { 22 }

!!Target NodeID 22	 [<baz> Source Loc: ] 
----------------------------------------------
##<baz> Source Loc: 
Ptr 22 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 23 		PointsTo: { 24 }

!!Target NodeID 24	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 24 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 25 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: { constant data }
Ptr 26 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<> Source Loc: 
Ptr 27 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 28 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { constant data }
Ptr 29 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<baz> Source Loc: 
Ptr 30 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { 0th arg baz  }
Ptr 31 		PointsTo: { 1008 1024 }

!!Target NodeID 1008	 [<> Source Loc: ] 
!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: { 1st arg baz  }
Ptr 32 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 33 		PointsTo: { 1008 1024 }

!!Target NodeID 1008	 [<> Source Loc: ] 
!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: { constant data }
Ptr 34 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<> Source Loc: 
Ptr 35 		PointsTo: { 15 1024 }

!!Target NodeID 15	 [<n> Source Loc: ] 
!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 36 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 37 		PointsTo: {empty}

----------------------------------------------
##<_Znwm> Source Loc: 
Ptr 38 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { 0th arg _Znwm  }
Ptr 39 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 1008 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 1024 		PointsTo: { 15 1024 }

!!Target NodeID 15	 [<n> Source Loc: ] 
!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------

ander:

----------------------------------------------
##<> Source Loc: { constant data }
Ptr 0 		PointsTo: {empty}

----------------------------------------------

Ptr 1 		PointsTo: {empty}

----------------------------------------------
##<Dummy Obj > id:2
Ptr 2 		PointsTo: {empty}

----------------------------------------------
##<Dummy Obj > id:3
Ptr 3 		PointsTo: {empty}

----------------------------------------------
##<main> Source Loc: 
Ptr 4 		PointsTo: { 5 }

!!Target NodeID 5	 [<main> Source Loc: ] 
----------------------------------------------
##<main> Source Loc: 
Ptr 5 		PointsTo: {empty}

----------------------------------------------
##<main> Source Loc: 
Ptr 6 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 7 		PointsTo: { 8 }

!!Target NodeID 8	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 8 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { constant data }
Ptr 9 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<> Source Loc: 
Ptr 10 		PointsTo: { 1008 }

!!Target NodeID 1008	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: { constant data }
Ptr 11 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<> Source Loc: 
Ptr 12 		PointsTo: { 1008 }

!!Target NodeID 1008	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 13 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<n> Source Loc: 
Ptr 14 		PointsTo: { 15 }

!!Target NodeID 15	 [<n> Source Loc: ] 
----------------------------------------------
##<n> Source Loc: 
Ptr 15 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { constant data }
Ptr 16 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<_Znwm> Source Loc: 
Ptr 17 		PointsTo: { 18 }

!!Target NodeID 18	 [<_Znwm> Source Loc: ] 
----------------------------------------------
##<_Znwm> Source Loc: 
Ptr 18 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 19 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 20 		PointsTo: {empty}

----------------------------------------------
##<baz> Source Loc: 
Ptr 21 		PointsTo: { 22 }

!!Target NodeID 22	 [<baz> Source Loc: ] 
----------------------------------------------
##<baz> Source Loc: 
Ptr 22 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 23 		PointsTo: { 24 }

!!Target NodeID 24	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 24 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 25 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: { constant data }
Ptr 26 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<> Source Loc: 
Ptr 27 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 28 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { constant data }
Ptr 29 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<baz> Source Loc: 
Ptr 30 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { 0th arg baz  }
Ptr 31 		PointsTo: { 1008 1024 }

!!Target NodeID 1008	 [<> Source Loc: ] 
!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: { 1st arg baz  }
Ptr 32 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 33 		PointsTo: { 1008 1024 }

!!Target NodeID 1008	 [<> Source Loc: ] 
!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: { constant data }
Ptr 34 		PointsTo: { 3 }

!!Target NodeID 3	 [Dummy Obj id: 3]
----------------------------------------------
##<> Source Loc: 
Ptr 35 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 36 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 37 		PointsTo: {empty}

----------------------------------------------
##<_Znwm> Source Loc: 
Ptr 38 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: { 0th arg _Znwm  }
Ptr 39 		PointsTo: {empty}

----------------------------------------------
##<> Source Loc: 
Ptr 1008 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------
##<> Source Loc: 
Ptr 1024 		PointsTo: { 1024 }

!!Target NodeID 1024	 [<> Source Loc: ] 
----------------------------------------------

Diff:

164c164
< Ptr 35 		PointsTo: { 15 1024 }
---
> Ptr 35 		PointsTo: { 1024 }
166d165
< !!Target NodeID 15	 [<n> Source Loc: ] 
191c190
< Ptr 1024 		PointsTo: { 15 1024 }
---
> Ptr 1024 		PointsTo: { 1024 }
193d191
< !!Target NodeID 15	 [<n> Source Loc: ]

mbarbar added 2 commits July 11, 2026 16:26

More comprehensively check whether a GEP edge can induce a field object.

3c538dc

Doc

bad82dd

yuleisui reviewed Jul 11, 2026

View reviewed changes

Flip conditon.

a12e1f1

mbarbar mentioned this pull request Jul 12, 2026

Assertion failed if -cluster-fs is enabled #1518

Open

mbarbar added 2 commits July 21, 2026 15:52

Process rep nodes when collapsing an SCC.

a465851

Merge branch 'rep-scc' into induce-gep

dc7463f

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

More comprehensively check whether a GEP edge can induce a GEP object#1870

More comprehensively check whether a GEP edge can induce a GEP object#1870
mbarbar wants to merge 5 commits into
SVF-tools:masterfrom
mbarbar:induce-gep

mbarbar commented Jul 11, 2026

Uh oh!

yuleisui Jul 11, 2026

Uh oh!

mbarbar Jul 11, 2026

Uh oh!

yuleisui commented Jul 11, 2026 •

edited

Loading

Uh oh!

mbarbar commented Jul 11, 2026

Uh oh!

mbarbar commented Jul 19, 2026

Uh oh!

mbarbar commented Jul 21, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

mbarbar commented Jul 11, 2026

Uh oh!

yuleisui Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

mbarbar Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

yuleisui commented Jul 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mbarbar commented Jul 11, 2026

Uh oh!

mbarbar commented Jul 19, 2026

Uh oh!

mbarbar commented Jul 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

yuleisui commented Jul 11, 2026 •

edited

Loading

mbarbar commented Jul 21, 2026 •

edited

Loading