Propagate bounds across untouched memory when dealing with inline assembly

[plotchy]

Bounds can be propagated when memory is untouched and variables are stored and loaded at the same positions.

contract Bound {
    function mask(uint256 a) public payable returns (uint) {
        uint256 b = a & 0xff;
        uint256 c;
        assembly {
            // store b and load into c
            let free_mem := mload(0x40)
            mstore(free_mem, b)
            c := mload(free_mem)
        }
        // range context is lost
        return c;
    }
}

Would expect c to share bounds with b

  4 │ ╭─▶     function mask(uint256 a) public payable returns (uint) {
  5 │ │           uint256 b = a & 0xff;
    │ │           ──────────┬─────────  
    │ │                     ╰─────────── "b" ∈ [ 0, 255 ]
    ┆ ┆   
 14 │ │           return c;
    │ │           ────┬───  
    │ │               ╰───── returns: "c" ∈ [ 0, 2**256 - 1 ]
 15 │ ├─▶     }
    │ │           
    │ ╰─────────── Entry function call

Seems difficult to track untouched memory with operations in between that touch memory (ie: codecopy, calldatacopy, etc). Are dest, offset of those tracked?

[brockelmore]

This should be possible but not on the short term roadmap. This is a pretty easy case but memory analysis is going to be a pretty big lift, so I want to have a bit more of a plan before attacking this