Virtually all real-valued computations are carried out using floating-point data types and operations. The precision of these data types must be set with the goals of reducing the overall round-off error, but also emphasizing reduced data movement and cache occupancy costs. Often, a mixed precision allocation achieves this optimum; unfortunately, there are no techniques available to compute such allocations and conservatively meet a given error target across all program inputs. In this work, we present a rigorous approach to precision allocation based on formal analysis via Symbolic Taylor Expansions, and error analysis based on interval functions. This approach is implemented in an automated tool called FPTUNER that generates and solves a quadratically constrained quadratic program to obtain a precision-annotated version of the given expression. FPTUNER automatically introduces all the requisite precision up/down casting operations. It also allows users to flexibly control precision allocation through constraints, including capping the number of high precision operators, grouping a collection of operators to allocate the same precision for them (to facilitate vectorization), etc. Our evaluation, including real energy measurements on an ARM (Jetson) hardware platform, demonstrate the degree to which precision choices can be exercised, especially controlling compiler optimizations, and the energy impacts of these allocations.