avoid loops in the exploded graph?

classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

avoid loops in the exploded graph?

via cfe-dev

Hi,

I read the comment "avoid loops in the exploded graph" in the following snippet of code which is on page 32 of the workbook.

LocationContext *LC = C. getLocationContext ();
ProgramStateRef State = C. getState ();
const Expr *E = /* Obtain an expression value of which is untrusted */;
ProgramStateRef NewState = State -> addTaint (E, LC );
if ( NewState != State ) // avoid loops in the exploded graph
  C. addTransition ( NewState );

My question is why the new tainted state requires the if statement to prevent loops, while other new states in the book do not have the if statement when C.addTransition(State) is used? Do other states which are not tainted not need to prevent loops? For example, on page 30, when a new state is added, it reads:

ProgramStateRef State = C. getState ();
State = modifyState ( State ); // do stuff
C. addTransition ( State );

There is no if state to prevent a loop.

-- 
Love,
Lou


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: avoid loops in the exploded graph?

via cfe-dev
Hi!

According to that, it would seem that a checker-side check should always be there.

Let's see what others think of this -- to me it would make more sense to have this check within addTransition, and I'm unsure myself why that TODO is there.

Lou Wynn via cfe-dev <[hidden email]> ezt írta (időpont: 2018. okt. 9., K, 3:42):

Hi,

I read the comment "avoid loops in the exploded graph" in the following snippet of code which is on page 32 of the workbook.

LocationContext *LC = C. getLocationContext ();
ProgramStateRef State = C. getState ();
const Expr *E = /* Obtain an expression value of which is untrusted */;
ProgramStateRef NewState = State -> addTaint (E, LC );
if ( NewState != State ) // avoid loops in the exploded graph
  C. addTransition ( NewState );

My question is why the new tainted state requires the if statement to prevent loops, while other new states in the book do not have the if statement when C.addTransition(State) is used? Do other states which are not tainted not need to prevent loops? For example, on page 30, when a new state is added, it reads:

ProgramStateRef State = C. getState ();
State = modifyState ( State ); // do stuff
C. addTransition ( State );

There is no if state to prevent a loop.

-- 
Love,
Lou

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: avoid loops in the exploded graph?

via cfe-dev
Hi,

My intuition is that in some situations it is guaranteed that the state will be modified and then the if (NewState!=State) check is unnecessary. In other situations there is a possibility that the state will remain the same (e.g. the expression was already marked as tainted, so nothing changes) and this could theoretically create to a loop edge (an edge from the current node to itself) in the exploded graph.

A loop edge is obviously undesirable, because it could send graph traversal into infinite loops, so wee need to guarantee that they do not appear in the exploded graph.  As Kristóf wrote, the method CheckerContext::addTransitionImpl() always guarantees this with a defensive check (with a TODO to turn it into an assert); but in some checkers it is also tested by the checker itself.

Donát

On k, 2018-10-09 at 11:10 +0200, Kristóf Umann via cfe-dev wrote:
Hi!

According to that, it would seem that a checker-side check should always be there.

Let's see what others think of this -- to me it would make more sense to have this check within addTransition, and I'm unsure myself why that TODO is there.

Lou Wynn via cfe-dev <[hidden email]> ezt írta (időpont: 2018. okt. 9., K, 3:42):

Hi,

I read the comment "avoid loops in the exploded graph" in the following snippet of code which is on page 32 of the workbook.

LocationContext *LC = C. getLocationContext ();
ProgramStateRef State = C. getState ();
const Expr *E = /* Obtain an expression value of which is untrusted */;
ProgramStateRef NewState = State -> addTaint (E, LC );
if ( NewState != State ) // avoid loops in the exploded graph
  C. addTransition ( NewState );

My question is why the new tainted state requires the if statement to prevent loops, while other new states in the book do not have the if statement when C.addTransition(State) is used? Do other states which are not tainted not need to prevent loops? For example, on page 30, when a new state is added, it reads:

ProgramStateRef State = C. getState ();
State = modifyState ( State ); // do stuff
C. addTransition ( State );

There is no if state to prevent a loop.

-- 
Love,
Lou

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: avoid loops in the exploded graph?

via cfe-dev

Use Occam’s razor, there is a very easy explanation for that particular TODO. Namely that no one had the time or effort to fix the checkers mentioned in the comment, and potentially the plethora of others introduced that exploit the early return. 😊

 

From: [hidden email]
Sent: 2018. október 9., kedd 14:03
To: [hidden email]; [hidden email]
Cc: [hidden email]
Subject: Re: [cfe-dev] avoid loops in the exploded graph?

 

Hi,

 

My intuition is that in some situations it is guaranteed that the state will be modified and then the if (NewState!=State) check is unnecessary. In other situations there is a possibility that the state will remain the same (e.g. the expression was already marked as tainted, so nothing changes) and this could theoretically create to a loop edge (an edge from the current node to itself) in the exploded graph.

 

A loop edge is obviously undesirable, because it could send graph traversal into infinite loops, so wee need to guarantee that they do not appear in the exploded graph.  As Kristóf wrote, the method CheckerContext::addTransitionImpl() always guarantees this with a defensive check (with a TODO to turn it into an assert); but in some checkers it is also tested by the checker itself.

 

Donát

 

On k, 2018-10-09 at 11:10 +0200, Kristóf Umann via cfe-dev wrote:

Hi!

According to that, it would seem that a checker-side check should always be there.

Let's see what others think of this -- to me it would make more sense to have this check within addTransition, and I'm unsure myself why that TODO is there.

 

Lou Wynn via cfe-dev <[hidden email]> ezt írta (időpont: 2018. okt. 9., K, 3:42):

Hi,

I read the comment "avoid loops in the exploded graph" in the following snippet of code which is on page 32 of the workbook.

LocationContext *LC = C. getLocationContext ();
ProgramStateRef State = C. getState ();
const Expr *E = /* Obtain an expression value of which is untrusted */;
ProgramStateRef NewState = State -> addTaint (E, LC );
if ( NewState != State ) // avoid loops in the exploded graph
  C. addTransition ( NewState );

My question is why the new tainted state requires the if statement to prevent loops, while other new states in the book do not have the if statement when C.addTransition(State) is used? Do other states which are not tainted not need to prevent loops? For example, on page 30, when a new state is added, it reads:

ProgramStateRef State = C. getState ();
State = modifyState ( State ); // do stuff
C. addTransition ( State );

There is no if state to prevent a loop.

-- 
Love,
Lou
 

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

 


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: avoid loops in the exploded graph?

via cfe-dev
Good point, but I don't think that it should be done -- are checkers modifying the ProgramState so heavily this simple check would be too costly, if avoidable? I personally do not believe so.

On 9 Oct 2018 14:50, "Whisperity" <[hidden email]> wrote:

Use Occam’s razor, there is a very easy explanation for that particular TODO. Namely that no one had the time or effort to fix the checkers mentioned in the comment, and potentially the plethora of others introduced that exploit the early return. 😊

 

From: [hidden email]
Sent: 2018. október 9., kedd 14:03
To: [hidden email]; [hidden email]
Cc: [hidden email]
Subject: Re: [cfe-dev] avoid loops in the exploded graph?

 

Hi,

 

My intuition is that in some situations it is guaranteed that the state will be modified and then the if (NewState!=State) check is unnecessary. In other situations there is a possibility that the state will remain the same (e.g. the expression was already marked as tainted, so nothing changes) and this could theoretically create to a loop edge (an edge from the current node to itself) in the exploded graph.

 

A loop edge is obviously undesirable, because it could send graph traversal into infinite loops, so wee need to guarantee that they do not appear in the exploded graph.  As Kristóf wrote, the method CheckerContext::addTransitionImpl() always guarantees this with a defensive check (with a TODO to turn it into an assert); but in some checkers it is also tested by the checker itself.

 

Donát

 

On k, 2018-10-09 at 11:10 +0200, Kristóf Umann via cfe-dev wrote:

Hi!

According to that, it would seem that a checker-side check should always be there.

Let's see what others think of this -- to me it would make more sense to have this check within addTransition, and I'm unsure myself why that TODO is there.

 

Lou Wynn via cfe-dev <[hidden email]> ezt írta (időpont: 2018. okt. 9., K, 3:42):

Hi,

I read the comment "avoid loops in the exploded graph" in the following snippet of code which is on page 32 of the workbook.

LocationContext *LC = C. getLocationContext ();
ProgramStateRef State = C. getState ();
const Expr *E = /* Obtain an expression value of which is untrusted */;
ProgramStateRef NewState = State -> addTaint (E, LC );
if ( NewState != State ) // avoid loops in the exploded graph
  C. addTransition ( NewState );

My question is why the new tainted state requires the if statement to prevent loops, while other new states in the book do not have the if statement when C.addTransition(State) is used? Do other states which are not tainted not need to prevent loops? For example, on page 30, when a new state is added, it reads:

ProgramStateRef State = C. getState ();
State = modifyState ( State ); // do stuff
C. addTransition ( State );

There is no if state to prevent a loop.

-- 
Love,
Lou
 

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

 


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: avoid loops in the exploded graph?

via cfe-dev
In reply to this post by via cfe-dev
The addTransition() method family is well-defended against accidentally squeezing the current state into it, there's no need to check if the state has changed on the checker side. I don't remember what i was thinking, but this statement in the guide is definitely outdated or incorrect.

I don't think this TODO is anyhow important to address. State comparison is O(1) regardless of how many changes were made. The TODO should probably be removed.

That said, these special cases and default arguments of addTransition(), i.e., passing null state, passing current state, passing null predecessor, passing current predecessor, passing null tag, etc., are too numerous and counter-intuitive to memorize, no wonder i was confused. I believe we should break this up into several methods instead (with different, intuitive names).


On 10/9/18 5:50 AM, Whisperity via cfe-dev wrote:

Use Occam’s razor, there is a very easy explanation for that particular TODO. Namely that no one had the time or effort to fix the checkers mentioned in the comment, and potentially the plethora of others introduced that exploit the early return. 😊

 

From: [hidden email]
Sent: 2018. október 9., kedd 14:03
To: [hidden email]; [hidden email]
Cc: [hidden email]
Subject: Re: [cfe-dev] avoid loops in the exploded graph?

 

Hi,

 

My intuition is that in some situations it is guaranteed that the state will be modified and then the if (NewState!=State) check is unnecessary. In other situations there is a possibility that the state will remain the same (e.g. the expression was already marked as tainted, so nothing changes) and this could theoretically create to a loop edge (an edge from the current node to itself) in the exploded graph.

 

A loop edge is obviously undesirable, because it could send graph traversal into infinite loops, so wee need to guarantee that they do not appear in the exploded graph.  As Kristóf wrote, the method CheckerContext::addTransitionImpl() always guarantees this with a defensive check (with a TODO to turn it into an assert); but in some checkers it is also tested by the checker itself.

 

Donát

 

On k, 2018-10-09 at 11:10 +0200, Kristóf Umann via cfe-dev wrote:

Hi!

According to that, it would seem that a checker-side check should always be there.

Let's see what others think of this -- to me it would make more sense to have this check within addTransition, and I'm unsure myself why that TODO is there.

 

Lou Wynn via cfe-dev <[hidden email]> ezt írta (időpont: 2018. okt. 9., K, 3:42):

Hi,

I read the comment "avoid loops in the exploded graph" in the following snippet of code which is on page 32 of the workbook.

LocationContext *LC = C. getLocationContext ();
ProgramStateRef State = C. getState ();
const Expr *E = /* Obtain an expression value of which is untrusted */;
ProgramStateRef NewState = State -> addTaint (E, LC );
if ( NewState != State ) // avoid loops in the exploded graph
  C. addTransition ( NewState );

My question is why the new tainted state requires the if statement to prevent loops, while other new states in the book do not have the if statement when C.addTransition(State) is used? Do other states which are not tainted not need to prevent loops? For example, on page 30, when a new state is added, it reads:

ProgramStateRef State = C. getState ();
State = modifyState ( State ); // do stuff
C. addTransition ( State );

There is no if state to prevent a loop.

-- 
Love,
Lou
 

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

 


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev