Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications