nsg-ethz / synet-plus Goto Github PK

In the completely non-symbolic sketch that is set in a way that the path R2, R1, R4, R6 is preferred due to it having a lower IGP metric, NetComplete synthesizes a configuration for the requirement that the path R2, R1, R3, R5 should be preferred.

Steps to reproduce:

• replace 1 with 6 in the method test_single_fail_configuration of 'test_bgpver.py'
• run only this test case
• check that the requirements are not met by running python grigori/checking/network.py var/tmp/

The tested random BGP configurations are:

• For the Heanet_simple topology the seeds 3124858447 and 3564130906 were used.
• For the Heanet topology the seeds 1086880043 and 3825078733 were used.
• For the Compuserve topology the seeds 3344070609 and 4034979292 were used.

It is probably best to test in that order as Heanet_simple is the smallest graph and Compuserve the largest.

I will add a section to the readme of Grigori that explains exactly how to reproduce my results. This will include shell scripts to generate those test cases. The topologies can all be found in tests/fixtures in Grigori.

Given only manually generated (semi-symbolic) routemap sketches are provided, update_network_graph still fails with non-concrete variables. Here the non-concrete variable happens to be Var89.

In earlier tries the update failed but there every link got an automatically generated symbolic routemap.

• Test case: test_bgp_limited_routemaps in tests/test_bgpgen.py.

The example two_ibgp_nodes in synet/examples/simple.py currently fails in gns3.write_configs().

This seems to be a bug in the way write_configs handles symbolic values.

Note that you have to first merge the networkx_migration PR in order for this error to pop up.

After the change 59be8164d9 in Tekton var/EBGP_Ver_Simple_1 is missing the network command completely which means no BGP prefix is announced from R3.

In the completely non-symbolic sketch that is set in a way that the path R2, R1, R4, R6 is preferred due to a shorter AS path, NetComplete synthesizes a configuration for the requirement that the path R2, R1, R3, R5 is preferred.

Steps to reproduce:

• replace 1 with 3 in the method test_single_fail_configuration of 'test_bgpver.py'
• run only this test case
• check that the requirements are not met by running python grigori/checking/network.py var/tmp/

With a fully symbolic config where the router ids are in decreasing order (with the requirement precedence in increasing order) and all the other metrics are the same, the solver should return unsat.

• Test-case: test_nothing_fail_multi in tests/test_bgpver.py

Currently check_order returns a non-empty list denoting an error when the bgp configuration would be possible.

• Expected behavior: returning an empty list since the requirement is satisfiable.
• Actual behavior: It returns a non-empty list from compute_dags()
• Test case: test_simplified_possible_bgp in grigori's 'tests/test_bgpgen.py'

I'm opening issues so that I don't loose track of them and that there is finally an unambiguous way of talking about the different ones.

Currently MatchPermitted is not an option in SMTMatch. The problem is that there seems to be no way to match all announcements (to drop all remaining announcements, assuming cisco does not do a drop all by default).

On the other hand I don't know if possibly matching against non-permitted announcements even makes sense. What does it mean to set the permitted announcement attribute to True, False and True again?

By dropping announcements (setting permitted to false) it should not be possible to provide connectivity for requirements that contain multiple paths. Right now permitted is symbolic, but the rest of the sketch is not, therefor the solver should return unsat.

• Test-case: test_announcement_drop in tests/test_bgpver.py

Currently when providing netcomplete with an example that requires routemaps in the sketch in order to implement the constraint and the sketch does not have any routemaps, it doesn't fail to produce the configs.

• Expected behavior: The solver does not say sat or the synthesis fails in some other way before that.
• Actual behavior: The solver says sat.
• Test case: test_simplified_bgp_configuration in grigori's 'tests/test_bgpgen.py'

I'm using my virtual machine, ubutnu20 LTS and player15.

I just download the z3, z3solver, and using my python 2.7 for the 2018's version.

then I download the requirements for synet-plus and the token.

when I run the bgp_peers, the things mostly seemed run well, but after printing the "Constraints adding time : xxxxx
Start Z3 check xxxx
Z3 check time: xxx
Setting the Var: xxx
Reading model time:xxxx
"

then it comes the error:
Traceback (most recent call last):
File "bgp_peers.py", line 212, in
bgp_example(args.outdir)
File "bgp_peers.py", line 203, in bgp_example
netcomplete.synthesize()
File "/home/chris/Downloads/synet-plus-master/synet/netcomplete.py", line 362, in synthesize
self.synthesize_bgp()
File "/home/chris/Downloads/synet-plus-master/synet/netcomplete.py", line 184, in synthesize_bgp
self.bgp_synthesizer.update_network_graph()
File "/home/chris/Downloads/synet-plus-master/synet/synthesis/new_propagation.py", line 435, in update_network_graph
self.ibgp_propagation.node[node]['box'].update_network_graph()
File "/home/chris/Downloads/synet-plus-master/synet/synthesis/new_bgp.py", line 607, in update_network_graph
rmap = smt_rmap.get_config()
File "/home/chris/Downloads/synet-plus-master/synet/utils/fnfree_policy.py", line 1670, in get_config
lines.append(line.get_config())
File "/home/chris/Downloads/synet-plus-master/synet/utils/fnfree_policy.py", line 1572, in get_config
actions = self.smt_actions.get_config()
File "/home/chris/Downloads/synet-plus-master/synet/utils/fnfree_policy.py", line 1448, in get_config
config = _gather_communities(communities, index)
File "/home/chris/Downloads/synet-plus-master/synet/utils/fnfree_policy.py", line 1430, in _gather_communities
assert isinstance(prev_action, ActionSetCommunity), "Found: {}".format(self.actions)
AssertionError: Found: [SetPermitted(EMPTY?Value), SetActions([SetNextHop(EMPTY?V(p(p((((((py(p(p(p((((("

so i don't know what to do , and if there is something caused by the new version nowadays 2020?
thanks for your idea! plz

The local pref values are the only things that are symbolic in the config, therefor they should be used to set the path preference and not be symbolic after running NetComplete.

• Test-case: test_symbolic_local_pref in tests/test_bgpver.py.

In the completely non-symbolic sketch that is set in a way that the path R2, R1, R4, R6 is preferred due to a lower med, NetComplete synthesizes a configuration for the requirement that the path R2, R1, R3, R5 is preferred.

Steps to reproduce:

• replace 1 with 4 in the method test_single_fail_configuration of 'test_bgpver.py'
• run only this test case
• check that the requirements are not met by running python grigori/checking/network.py var/tmp/

Note that in the ideal case, it would never hit this error because #9 would be correct and abort the generation.

• Test case: test_writing_simplified_bgp_configuration in grigori's 'tests/test_bgpgen.py'. Run it and then test the configuration using dynamips and python grigori/checking/network.py var/possible_bgp/.

When creating a virtual iBGP full mesh (by calling add_bgp_neighbor with two nodes that are not directly connected with a link) the synthesis fails in compute_next_hop_map (set_bgp_neighbor_iface)

Not being able to have iBGP full mesh leads to other problems.

Steps to reproduce:

• Run the test case test_negative_constraints in test_bgpver.py

In the completely non-symbolic sketch that is set in a way that the path R2, R1, R6 is preferred due to it being advertised via eBGP instead of iBGP, NetComplete synthesizes a configuration for the requirement that the path R2, R1, R3, R5 should be preferred.

Steps to reproduce:

• replace 1 with 5 in the method test_single_fail_configuration of 'test_bgpver.py'
• run only this test case
• check that the requirements are not met by running python grigori/checking/network.py var/tmp/

If you look at the config of R1 for var/EBGP_Ver_Simple_1 the prefix list should be the destination network (128.0.2.0/24) not the current network (128.0.0.0/24).

The problem seems to lie with Tektons gen_external_announcements (in cisco.py).

Steps to reproduce:

1. Generate the configuration using the test case test_simple_config_gen (and comment out the second half where simple_req_only is called with True, generates var/tmp) in test_bgpver.py or via running python grigori/reqgen/bgp_ver.py (generates var/EBGP_Ver_Simple_1).
2. Run grigori on the input: python grigori/checking/network.py config-directory-from-1 while having dynamips running.

When calling synthesize (use_igp is false) creating the iBGP propagation fails due to create_symbolic_announcements failing at the assertion that next_hop is not in fixed.

This might also be my fault, but currently I don't understand this part of the code.

Steps to reproduce:

1. Replace the 2 in the test_single_fail_configuration (in test_bgpver.py) test case with a 3
2. Run the test case

When giving the solver symbolic values for the ospf weights in an otherwise concrete config, the solver should find a concrete value that satisfies the requirement.

• Test-case: test_symbolic_ospf_weights in tests/test_bgpver.py

When the router ids are assigned in the right order the solver names three conflicting constraints:

[Block_R3_from_R5_104,
 Imp_R3_from_R5_permitted_124,
 Allow_R5_from_R8_30]

This same error also crops up in all other cases that should generate something valid.

The test case is test_router_ids in tests/test_bgpver.py.

Here are a list of test cases generated by bgp_ver.py which currently fail:

• EBGP_Ver_Ordered_2_2
• EBGP_Ver_Ordered_2_3
• EBGP_Ver_Ordered_2_5
• EBGP_Ver_Ordered_3_2
• EBGP_Ver_Ordered_3_3

All the configs for those cases can be generated via python grigori/reqgen/bgp_ver.py. The check can be run via python grigori/checking/network.py var/nameOfDirectory.