Narrowing with bottom does not produce bottom

[Red-Panda64]

Below is a slightly reformatted (removed indentation and added line breaks to make this more readable) traced message which shows an
a value being narrowed with bot and remaining unchanged.

%%% narrow: narrow HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
base:({
Parameter {
i ->   (Unknown int([-31,31]),[0,2147483647])
}
}, {}, {}, (P:{}, Protected Changes:{
})),
threadid:(wrapper call:varinfo * node * chain option:(varinfo:f, node:node 21 "pthread_create((pthread_t * __restrict  )(& id), (pthread_attr_t const   * __restrict  )((void *)0), & f, (void * __restrict  )((void *)0));", chain option:no index), Thread:[main, f@tests/regression/95-dividedsides/19-dead-side-effect3.c:26:3-26:36], created:(current function:bot, callees:bot)),
threadflag:Multithreaded (other),
threadreturn:False,
escape:{},
mutexEvents:(),
access:(),
mutex:(lockset:{}, multiplicity:{}),
race:(),
mhp:(),
assert:()], map:{})}

with bot to

HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
base:({
Parameter {
i ->   (Unknown int([-31,31]),[0,2147483647])
}
}, {}, {}, (P:{}, Protected Changes:{
})),
threadid:(wrapper call:varinfo * node * chain option:(varinfo:f, node:node 21 "pthread_create((pthread_t * __restrict  )(& id), (pthread_attr_t const   * __restrict  )((void *)0), & f, (void * __restrict  )((void *)0));", chain option:no index), Thread:[main, f@tests/regression/95-dividedsides/19-dead-side-effect3.c:26:3-26:36], created:(current function:bot, callees:bot)),
threadflag:Multithreaded (other),
threadreturn:False,
escape:{},
mutexEvents:(),
access:(),
mutex:(lockset:{}, multiplicity:{}),
race:(),
mhp:(),
assert:()], map:{})}

There are some domains (e.g. DefExc) that do not narrow to bottom. The interval should be narrowed to bottom, however. It seems this is prevented by some lifter further up.

[Red-Panda64]

I have discovered this snippet in src/domain/lattice.ml:

  let widen x y =
    match (x,y) with
    | (`Lifted x, `Lifted y) -> `Lifted (Base.widen x y)
    | _ -> y

  let narrow x y =
    match (x,y) with
    | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
    | _ -> x

These are part of the LiftConf module, which also has constructors `Top and `Bot. Not only does this mean, that narrowing with bottom is a nop instead of returning bottom, it also means that widen (`Top, `Lifted y) returns `Lifted y, which is less than `Top.

[michael-schwarz]

Oops!

[Red-Panda64]

Same applies to LiftPO, Lift2Conf, LiftBot and LiftTop. Maybe I am missing something here, but that seems wrong to me.

[michael-schwarz]

The correctness argument is that our solvers ensure that for widen the second argument is larger and for narrow the second argument is smaller. But I'm not sure whether all lifters maintain this, so making it more explicit may be a good idea.

[sim642]

For widen that is documented and guaranteed last time I checked.

For narrow, I'm hearing that assumption for the first time. TD3 doesn't guarantee this (#490 (comment)) and this was considered expected when we discussed it (to remove the assert). Our properties for narrow have matched the textbook definitions:

analyzer/src/domains/domainProperties.ml

Lines 182 to 183 in b8a5bb9

	let narrow_meet = make ~name:"narrow meet" (pair arb arb) (fun (a, b) -> D.leq (D.meet a b) (D.narrow a b))
	let narrow_fst = make ~name:"narrow fst" (pair arb arb) (fun (a, b) -> D.leq (D.narrow a b) a)

.

[Red-Panda64]

I see. In terms of correctness, the narrowing implementation is not an issue. The widening is an oversight on my part. Still, as discussed with @michael-schwarz, it would be nice for narrowing with bottom to produce bottom for a mechanism we are working on. Is it acceptable to change the narrowing operators to produce bottom whenever possible? If not, it is not a big issue, as I already have a work-around.

[sim642]

Is it acceptable to change the narrowing operators to produce bottom whenever possible?

I think it makes sense to change the various Lift/Flat/... lattice functors to do that. It's consistent with the two properties.