Test on infinite_2.c with fc2068cdedf9560879294b71f009ee780cf3ca86

int main(){
    int X0=1, X1=1;
    while(X1<10){
        X0 = X1*X0;
        X1 = X1+X0;
    }
}

Fail with :

>           assert str(relation.matrix[0][0].list[2]) == 'i.delta(0,0).delta(0,1)'
E           AssertionError: assert 'i.delta(1,0)' == 'i.delta(0,0).delta(0,1)'
E             - i.delta(0,0).delta(0,1)
E             + i.delta(1,0)

Maybe we should check by hand that output values ?

A small comment, but for instance

int main(){
    int y1, y2;
    y2 = y1 + y1;
}

gives

y2    |     +o  +o
y1    |     +o+w.delta(0,0)+p.delta(1,0)+w.delta(2,0)  +m

we could get rid of the +o in the lower-left corner.

The following program:

int main(){
    x2 = x3 + x1;
    x4 = x2;
}

gives

--- Affiche <relation_list.RelationList object at 0x7f54084e7ef0> ---
1:
x2    |     +o  +o  +o
x3    |     +o+w.delta(0,0)+m.delta(1,0)+p.delta(2,0)  +m  +o
x1    |     +o+w.delta(0,0)+p.delta(1,0)+m.delta(2,0)  +o  +m
--- FIN ---
[[0], [1], [2]]

As we can see, x4 is simply not accounted for.

I've started to re-organize the example folder a bit with https://github.com/seiller/pymwp/commit/e261323f5f8d9d1ff50789881d2121810a5b8677

A couple of observations:

• the "readme" at https://github.com/seiller/pymwp/blob/tests-examples/c_files/readme.md is very basics, we will have to expand it more "tutorial" style.
• It would be profitable to have "the usual examples" of non-polynomial programs (typically, exponential computation),
• I was a bit dumb and created this branch before https://github.com/seiller/pymwp/pull/20 was created. As a result, some tests are not correct, but I suspect they have been fixed since.
• I have not changed the https://github.com/seiller/pymwp/tree/tests-examples/tests files, so I probably broke a couple of things.
• We need to discuss the fact that most / some of those programs cannot be compiled.

As of now,

• basics/declaration.c should give an identity matrix of dimension 1.
• basics/assign_value.c should give a matrix containing 0.
• basics/assign_variable.c should returns [m m // 0 0] (x / y).
• basics/if_else.c should returns [m m // m m](x / y) I believe.
• basics/if.c should returns [m m // 0 m](x / y) I believe.
• basics/while_1.c should returns something (not 100% sure what)
• not_infinite/exponent.c results in an empty matrix?

I have not checked the while_if.c, but I believe all the other examples are ok.

The current example we are using in the notes,

int main(){
    int X1;
    int X2;
    X1 + X2;
}

produces:

In compute_rel
uncovered case ! Create empty RelationList (function call) ?
Decl: X1, [], [], []
  TypeDecl: X1, []
    IdentifierType: ['int']
In compute_rel
uncovered case ! Create empty RelationList (function call) ?
Decl: X2, [], [], []
  TypeDecl: X2, []
    IdentifierType: ['int']
In compute_rel
uncovered case ! Create empty RelationList (function call) ?
BinaryOp: +
  ID: X1
  ID: X2
--- Affiche <relation_list.RelationList object at 0x7f3e314adf98> ---
1:

--- FIN ---
[[]]

It seems like valid C code to me and should be analyzed by our program. Am I missing something?

delta_iter branch has custom version of Python standard lib itertools.product that is used to generate choices for eval.

TODO:

• [x] debug delta_iter to make sure it works correctly
• [x] add unit tests to show the above
• [ ] there may be cases where standard lib itertools.product is more optimal, in which case should use it over delta_iter
• [x] update relation.py to use delta_iter implementation

Analyzing simple program like this yields empty result because we skip declaration statements and currently we pick up variables from when they are being used. This issue is to discuss the analysis output for such simple program.

https://github.com/seiller/pymwp/blob/252b5e3f9e159ab17990d0e16f65dd14187a1adc/c_files/basics/assign_value.c#L6-L8

We could display:

   y
y +o

but it requires adding some logic to handle declaration nodes in the AST, so that the presence of the variable is discovered and then to run the analysis to generate the matrix.

-or- we display empty output which is not very user-friendly.

-or- we still skip declaration nodes in the AST, and then if the analysis discovers no variables, we can say some alternative output message to indicate "there was nothing to analyze" (I am putting this in quotes because it needs better wording to be clear in meaning).

Comments?

Please review this changeset and run it on examples to evaluate its impact.

The evaluation procedure is explained with examples in choice.py so I will not repeat it here, but we can discuss it in more.

This approach also changes the representation of choices. Before:

[2,2,2,2,0,0,2], [2,2,2,2,0,1,2], [2,2,2,2,0,2,2], [2,2,2,2,1,0,2], [2,2,2,2,1,1,2], 
[2,2,2,2,1,2,2], [2,2,2,2,2,0,2], [2,2,2,2,2,1,2], [2,2,2,2,2,2,2]

Equivalent, but now more compact:

[[[2], [2], [2], [2], [0, 1, 2], [0, 1, 2], [2]]]

Which is read as: choose a vector (there could be multiple, it is a list of lists), then choose one of the remaining choices at each index; this will give a valid derivation.

This change has some practical implications:

• faster eval+compact representation of choices enables analyzing programs with larger index (more assignments) and also reasonably displaying or writing those results to file
• it enables evaluating programs like long.c, whose index is 13, which is also introduced in this changeset
• it is now possible to evaluate the original dense.c (in tests/test_examples/complex_dense.c) -- it still takes ~1 min to analyze, but the evaluation step is instantaneous
• the analysis phase is now more significant regarding performance
• removes progress bar external dependency

We should discuss the behavior of this method:

https://github.com/seiller/pymwp/blob/4250ab22bab7d7057c4949712ca35b9e76b50fd5/pymwp/relation.py#L130-L136

This is the only place where i may be introduced. It is run on each while loop node during the analysis (after computing fixpoint).

Some open questions:

• What I don't get is that it seems that we are applying that correction to all the coef., and not only to the ones on the diagonal. What am I missing?

• I think that if the coefficient is not m (meaning it is either 0, w, p or i), then we need to change it to i: as of now, I don't think that's what we do.

• this expression is totally different if you change parentheses:

if mon.scalar == "p" or (mon.scalar == "w" and i == j)

to

if (mon.scalar == "p" or mon.scalar == "w") and i == j

the latter checks for diagonal scalars only.

This PR adds a utility for running cProfile on multiple examples. I have added docs to explain how to use it.

When I run on GH server (linux) the dense function hangs, but it should timeout after 30 sec. It terminates correctly for me. Please try it and let me know if it gets stuck on all Linux machines or just the build machine, I'm not sure.

• consider time as relative since it depends on # of cores
• not able to profile dense when it does not terminate (until I figure out how to add some timeout limit)
• for_body.c cannot be parsed and throws
• "before" == master branch, "after" === simpl branch

Some comparisons ordered by internal time:

infinite_8.c

before: 13224063 function calls (10707799 primitive calls) in 5.163 seconds

| ncalls | tottime | percall | cumtime | percall | filename:lineno(function) | | --- | --- | --- | --- | --- | --- | 626833 | 0.623 | 0.000 | 0.927 | 0.000 | polynomial.py:296(compare) 158893/1577 | 0.616 | 0.000 | 1.135 | 0.001 | polynomial.py:352(sort_monomials) 6561 | 0.579 | 0.000 | 1.303 | 0.000 | polynomial.py:237(eval) 1907969/448430 | 0.451 | 0.000 | 0.636 | 0.000 | python3.7/json/encoder.py:277(_iterencode_list) 1607264 | 0.369 | 0.000 | 0.369 | 0.000 | semiring.py:69(sum_mwp) 1597239 | 0.360 | 0.000 | 0.360 | 0.000 | monomial.py:116(eval)

after: 2561855 function calls (2483457 primitive calls) in 1.328 seconds

| ncalls | tottime | percall | cumtime | percall | filename:lineno(function) | | --- | --- | --- | --- | --- | --- | 284672 | 0.238 | 0.000 | 0.534 | 0.000 | monomial.py:95(inclusion) 17709 | 0.206 | 0.000 | 0.760 | 0.000 | polynomial.py:76(inclusion) 565173 | 0.193 | 0.000 | 0.193 | 0.000 | monomial.py:79(contains) 334183 | 0.115 | 0.000 | 0.115 | 0.000 | semiring.py:69(sum_mwp) 56065 | 0.057 | 0.000 | 0.083 | 0.000 | polynomial.py:357(compare) 23335/1577 | 0.054 | 0.000 | 0.098 | 0.000 | polynomial.py:413(sort_monomials)

notinfinite_8.c

before: 15474866 function calls (13029729 primitive calls) in 6.015 seconds

| ncalls | tottime | percall | cumtime | percall | filename:lineno(function) | | --- | --- | --- | --- | --- | --- | 8451 | 1.409 | 0.000 | 3.085 | 0.000 | polynomial.py:237(eval) 3659175 | 0.910 | 0.000 | 0.910 | 0.000 | monomial.py:116(eval) 3662513 | 0.767 | 0.000 | 0.767 | 0.000 | semiring.py:69(sum_mwp) 124347/1987 | 0.503 | 0.000 | 0.918 | 0.000 | polynomial.py:352(sort_monomials) 1880855/440563 | 0.448 | 0.000 | 0.629 | 0.000 | python3.7/json/encoder.py:277(_iterencode_list) 357668 | 0.357 | 0.000 | 0.534 | 0.000 | polynomial.py:296(compare)

after: 2463339 function calls (2391520 primitive calls) in 1.308 seconds

| ncalls | tottime | percall | cumtime | percall | filename:lineno(function) | | --- | --- | --- | --- | --- | --- | 290047 | 0.240 | 0.000 | 0.546 | 0.000 | monomial.py:95(inclusion) 14298 | 0.210 | 0.000 | 0.777 | 0.000 | polynomial.py:76(inclusion) 576027 | 0.201 | 0.000 | 0.201 | 0.000 | monomial.py:79(contains) 363732 | 0.121 | 0.000 | 0.121 | 0.000 | semiring.py:69(sum_mwp) 62967 | 0.064 | 0.000 | 0.094| 0.000 | polynomial.py:357(compare) 21887/1987 | 0.050 | 0.000 | 0.089 | 0.000 | polynomial.py:413(sort_monomials)

To profile individual C file, the command is:

python -m cProfile -s tottime -m pymwp c_files/infinite_2.c

• replace -m pymwp to profile using old Analysis.py (though it pauses for user input so might not work?)
• replace c_files/infinite_2.c with whatever input you want to profile

Analyzing single variable assignment

https://github.com/statycc/pymwp/blob/662f1b9fadfe815e42499d1357d1698467ea29f9/c_files/basics/assign_variable.c#L6-L8

gives the matrix below and choices [0], [1], [2].

| | x | y | |-- | -- | -- | | x | o | o | | y | m | m |

I don't think the choice applies here? This is by rule E1.

The issue on declarations echoed with a more fundamental question that I have, and that is "must values inside the program relates to an input?".

Let me explain: as of now, we are interpreting x = <any value>; as "reset the coefficient for x to 0", because there is now no connection between the inputs and x. However, I'm not sure that this is permitted, for three reasons:

• There is no rule for that case in the original paper, and as far as I can tell it's not even discussed,
• In On Decidable Growth-Rate Properties of Imperative Programs, Ben-Amram "just" works on adding a "reset" instruction to a similar language and shows that it is not easy to do so,
• When discussing constants, they write:

To deal with constants, just replace the program’s constants by variables and regard the replaced constants as input to these variables.

as if (my reading), values had to be linked to the program's input.

All of that being said, they have an example of re-initialization (Example 3.1)

C′′ ≡ X1 := 1; loop X 2 { X1 := X1 +X1 }

as if it was no big deal.

I may simply be confused. Thoughts?

example3_4.c gives an error, probably because there I am mixing two operations in one statement.

Originally posted here

The analysis makes some assumptions about left and right operand structure:

https://github.com/seiller/pymwp/blob/51bc64cfd9b3638de20a2e2671535a4975c2549f/pymwp/analysis.py#L165-L173

which prevents using the original expression X3 = X2 * X2 + X5; Adding some recursive step in binary op might allow analyzing this expression in original form (depending on what the AST looks like for this statement, I have not looked into it)?

If this is not worth fixing at the moment then we can add a note in the features table that binary op is for two operands and support for multiple is in progress.

During analysis of a for loop, the implementation call a non-existent method rels.conditionRel.

This was, at some point, a method of RelationList class, but going back as far as old_dfg_mwp_python I have not found the implementation.

Trying to resolve this:

1. what does this method do?
2. (independent of previous) is it necessary to call this method?

Current implementation with added comments:

        # create empty relation list
        rels = RelationList([])

        # recursively analyze children of current AST node, update index value
        for child in node.stmt.block_items:
            index, rel_list = compute_rel(index, child)
            
            # add to relation list (will resize matrix as needed)
            rels = rels.composition(rel_list)

        # run fixpoint    
        rels = rels.fixpoint()
        
        # ?????
        rels = rels.conditionRel(list_var(node.cond))

        # return updated index, relation list
        return index, rels

(actual source without comments)

list_var extends c_ast.NodeVisitor and returns node names, implementation: [1], [2]