Merging States

When you’re learning programming, they teach about branch statements like if(), but in Smatch how paths merge back together is much more interesting than branching. That’s where the history is saved, so a lot of internal magic happens here.

if (x == 1) { // <-- branch
	y = 1;
	kfree(p);
} else {
	y = 3;
} // <-- merge is invisible

Smatch states are saved in a group called a stree. The current states are
call the cur stree. When we merge two strees, the rule is that if there is a
state on one side then there must be a matching state on the other side.

In the above code, we free “p” if x == 1 and not on the other side. So the state of “p” is &freed on one side, but not set on the other side. What happens by default is that we will set the state to &undefined for the false path. Then when we merge &freed + &undefined it gives us &merged. The &freed state will still be listed in the ->possible list.

Smatch provides a number of hooks to manipulate how merging happens.

add_unmatched_state(): This lets you specify something instead of &undefined. For example, lets say we want to record if a function frees a parameter. If a parameter is freed on one side and it’s NULL on the other side then let’s set the unmatched state to &freed.

if (param)
	kfree(param);
// <-- we want the state to be freed here

ad_merge_hook: This allows you set a different state instead of &merged. The
sm_state will still have a ->merged = true, so Smatch still tracks merges.

add_pre_merge_hook: This is for if you want to look up other information during a merge. So for example, in check_uninitialized.c if a variable is
&uninitialized but the path is impossible then set the state to &initialized. Uninitialized variables and impossible paths are tracked separately but we want to use the information from both during a merge.