Generating constraints in a target programming language from traces of operations specified in an input

A method, comprising:

• generating a plurality of traces of a plurality of operations specified in an input that access data between a start node and an end node, wherein the plurality of operations comprise one or more put operations using a put index variable to set a value in an entry in an array and one or more get operations using a get index variable to obtain the value from the entry in the array;
• based on the plurality of traces, generating a code template in a target programming language to test the plurality of operations of the plurality of traces, wherein the code template:
• identifying a valid trace in the plurality of traces between the start node and the end node by pairing corresponding ones of the one or more put operations and the one or more get operations and testing for equivalence of index values calculated for the put index variable and the get index variable in respective contexts of the put operations and the get operations, wherein the pairing of the corresponding put operations and the get operations and the respective contexts are determined according to at least a forward pass and a backward pass respectively performed over individual ones of the plurality of traces to construct a set of loops and loop index substitutions that test for equivalence of the index values in the paired corresponding ones of the one or more put operations and the one or more get operations of the valid trace;
• and
• for the identified valid trace, adding a portion of code in the target programming language into the set of loops that prevents execution of further code placed in the code template for additional valid traces.

One or more, non-transitory, computer-readable storage media, storing program instructions that when executed on or across one or more computing devices, cause the one or more computing devices to implement:

• generating a plurality of traces of a plurality of operations specified in an input that access data between a start node and an end node, wherein the plurality of operations comprise one or more put operations using a put index variable to set a value in an entry in an array and one or more get operations using a get index variable to obtain the value from the entry in the array;
• based on the plurality of traces, generating a code template in the target programming language to test the plurality of operations of the plurality of traces, wherein the code template:
• identifying a valid trace in the plurality of traces between the start node and the end node by pairing corresponding ones of the one or more put operations and the one or more get operations and testing for equivalence of index values calculated for the put index variable and the get index variable in respective contexts of the put operations and the get operations, wherein the pairing of the corresponding put operations and the get operations and the respective contexts are determined according to at least a forward pass and a backward pass respectively performed over individual ones of the plurality of traces to construct a set of loops and loop index substitutions that test for equivalence of the index values in the paired corresponding ones of the one or more put operations and the one or more get operations of the valid trace;
• and
• for the identified valid trace, adding a portion of code in the target programming language into the set of loops that prevents execution of further code placed in the code template for additional valid traces.