Commit 6437ec67 authored by erwan's avatar erwan
Browse files

Fix: a bug in the rdbg plugin when iterating on arrays on size 1

parent 8552ed35
Pipeline #26981 passed with stages
in 5 minutes and 13 seconds
......@@ -13,15 +13,31 @@ Donnons du Lustre aux leds
* laius FDS :noexport:
Au laboratoire Verimag, les scientifiques cherchent à aider les ingénieurs à prouver automatiquement que leurs programmes sont corrects.
Pour certains programmes, cette question est cruciale, car des vies sont en jeu, notamment quand il s’agit de systèmes embarqués (dans des avions, des trains, des voitures), mais elle est aussi difficile à cause de l'explosion combinatoire.
Une illustration de ce phénomène est donnée par l'échiquier de Sissa, sur lequel le nombre de grains de riz est doublé à chaque case: 1 grain sur la première case 1, 2 grains sur la suivante, puis 4, 8, 16, etc. Un tel échiquier comporte 2^{64}-1$ grains de riz, c'est à dire plus de 18 milliards de milliards de grains, soit l'équivalent de 1000 ans de production mondiale de riz actuellement. Or un programme utilisant 64 cases (ou bits) est un petit programme, et vérifier qu'il est correct dans tous les cas de figure peut nécessiter de considérer des milliards de milliards de cas.
Au laboratoire Verimag, les scientifiques cherchent à aider les
ingénieurs à prouver automatiquement que leurs programmes sont
corrects.
Pour certains programmes, cette question est cruciale, car des vies
sont en jeu, notamment quand il s’agit de systèmes embarqués (dans des
avions, des trains, des voitures), mais elle est aussi difficile à
cause de l'explosion combinatoire.
Une illustration de ce phénomène est donnée par l'échiquier de Sissa,
sur lequel le nombre de grains de riz est doublé à chaque case: 1
grain sur la première case, 2 grains sur la suivante, puis 4, 8, 16,
etc. Un tel échiquier comporte 2^{64}-1$ grains de riz, c'est à dire
plus de 18 milliards de milliards de grains, soit l'équivalent de 1000
ans de production mondiale de riz actuellement. Or un programme
utilisant 64 cases (ou bits) est un petit programme, et vérifier qu'il
est correct dans tous les cas de figure peut nécessiter de considérer
des milliards de milliards de cas.
Au laboratoire Verimag, les axes de recherche visant à vérifier la correction de programmes critiques concernent la conception de langages de programmation, ainsi que des méthodes et des outils de preuve et de test automatisé.
Pour illustrer ces travaux, les chercheurs montreront comment vérifier la correction d'un petit programme embarqué sur une carte Arduino, comportant 2 entrées, actionnées par un bouton rouge et un bouton bleu, et 5 sorties, contrôlant l'allumage de 5 leds.
Pour illustrer ces travaux, les chercheurs montreront comment vérifier
la correction d'un petit programme embarqué sur une carte Arduino
comportant 2 entrées, actionnées par un bouton rouge et un bouton
bleu, et 5 sorties, contrôlant l'allumage de 5 leds.
L'intégrité de ce système embarqué sera considérée comme compromise si une séquence d'entrée permet d'allumer les 5 leds simultanément. Le public pourra essayer de déterminer si différents programmes embarqués sur ce système sont dangereux (bogués), comme autant de petits puzzles.
......
(* Time-stamp: <modified the 10/07/2018 (at 10:41) by Erwan Jahier> *)
(* Time-stamp: <modified the 10/07/2019 (at 13:51) by Erwan Jahier> *)
open Soc
open Data
......@@ -110,7 +110,6 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
let node_soc = SocUtils.find step.lxm node_sk soc_tbl in
let node_step = match node_soc.step with [step] -> step | _ -> assert false in
let iter_inputs,iter_outputs = soc.profile in
let rctx = ref ctx in
let (proc_name,_,_) = node_soc.key in
let inst_name =
match soc.instances with
......@@ -125,12 +124,13 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
List.map (array_index i) iter_outputs)
| "fold" | "red" | "fill"
| "fillred" ->
let a_in = Var (List.hd iter_inputs) in
let a_in = Var (List.hd iter_inputs) in
let a_out = Var (List.hd iter_outputs) in
(
assert(iter_inputs <> []);
assert(iter_outputs <> []);
a_in::(List.map (array_index i) (List.tl iter_inputs)),
a_in::(List.map (array_index i) (List.tl iter_outputs)))
a_out::(List.map (array_index i) (List.tl iter_outputs)))
| _ -> assert false (* should not occur *)
in
let ctx = { ctx with cpath = inst_name.(i)::ctx.cpath } in
......
(* Time-stamp: <modified the 05/04/2019 (at 13:08) by Erwan Jahier> *)
(* Time-stamp: <modified the 10/07/2019 (at 14:14) by Erwan Jahier> *)
open Soc
open Data
open SocExecValue
......@@ -366,6 +366,9 @@ let rec (soc_step : Lxm.t -> Soc.step_method -> Soc.tbl -> Soc.t ->
| "fillred" ->
let a_in = (List.hd iter_inputs) in
let a_in_i, a_in_ip1 =
if n = 1 then (* array of size 1 *)
Var (a_in), Var (List.hd iter_outputs)
else
if i = 0 then
Var (a_in), Var (add_i 1 a_in)
else
......
==> lus2lic0.sum <==
Test run by jahier on Wed May 22 17:16:22
Test run by jahier on Wed Jul 10 14:23:07
Native configuration is x86_64-pc-linux-gnu
=== lus2lic0 tests ===
......@@ -66,7 +66,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
==> lus2lic1.sum <==
Test run by jahier on Wed May 22 17:16:22
Test run by jahier on Wed Jul 10 14:23:07
Native configuration is x86_64-pc-linux-gnu
=== lus2lic1 tests ===
......@@ -409,7 +409,7 @@ PASS: sh multipar.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
==> lus2lic2.sum <==
Test run by jahier on Wed May 22 17:16:45
Test run by jahier on Wed Jul 10 14:23:29
Native configuration is x86_64-pc-linux-gnu
=== lus2lic2 tests ===
......@@ -749,7 +749,7 @@ PASS: sh zzz2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
Test run by jahier on Wed May 22 17:17:11
Test run by jahier on Wed Jul 10 14:23:55
Native configuration is x86_64-pc-linux-gnu
=== lus2lic3 tests ===
......@@ -1259,7 +1259,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
Test run by jahier on Wed May 22 17:17:50
Test run by jahier on Wed Jul 10 14:24:33
Native configuration is x86_64-pc-linux-gnu
=== lus2lic4 tests ===
......@@ -1777,13 +1777,13 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
===============================
# Total number of failures: 15
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 23 seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 22 seconds
lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 26 seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 39 seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 13 seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 38 seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 15 seconds
* Ref time:
51.94user 18.17system 1:41.67elapsed 68%CPU (0avgtext+0avgdata 273712maxresident)k
0inputs+143240outputs (0major+11004706minor)pagefaults 0swaps
52.29user 17.65system 1:40.92elapsed 69%CPU (0avgtext+0avgdata 273612maxresident)k
0inputs+143232outputs (0major+11011148minor)pagefaults 0swaps
* Quick time (-j 4):
58.56user 19.69system 1:07.46elapsed 116%CPU (0avgtext+0avgdata 273796maxresident)k
0inputs+142736outputs (0major+10967172minor)pagefaults 0swaps
62.58user 19.44system 0:55.22elapsed 148%CPU (0avgtext+0avgdata 272896maxresident)k
0inputs+142192outputs (0major+10940912minor)pagefaults 0swaps
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment