Re: [Paparazzi-devel] Source code analysis of paparazzi

[Matthieu Lemerre]

Hi Karoly,

OK. I used the "x86_32" settings of Frama-C, which may not correspond
when endianness is important (may happen in some places), but at least
does for integer sizes (which is really important). So the analysis may
be unsound, but this is sufficient as a preliminary study

Regards,
Matthieu

Karoly Molnar <address@hidden> writes:

> Hi Mathieu,
>
> in compiler settings I meant that you typically have to provide settings how 
> a given compiler would theoretically compile the code that you want to 
> analyze. I have worked with PCLint, Klocwork and QAC to mention a few and 
> each of these are using some sort of target and compiler specific 
> configuration to tell the static analysis tool e.g. the endianness, the size 
> of an int on the target, if the enum is char or int etc... When I have 
> referred to compiler settings, I thought something similar exists for FramaC 
> as well. 
>
> Regards
> Karoly
>
>> From: address@hidden
>> To: address@hidden
>> Date: Wed, 3 Dec 2014 11:43:18 +0100
>> CC: address@hidden
>> Subject: Re: [Paparazzi-devel] Source code analysis of paparazzi
>> 
>> 
>> Hi Felix and Karoly,
>> 
>> Yes, this was a configuration error from my side, the code is
>> correct. The long that appear is in the source code after being parsed
>> by Frama-C; the problem I had here is that I forgot to configure the
>> Frama-C libc emulation correctly, and it translated int64_t to long
>> instead of long long.
>> 
>> @Karoly: Keep in mind that this is source code analysis, so there is no
>> compiler settings outside of configuration of Frama-C itself... 
>> 
>> Best regards,
>> Matthieu
>> 
>> Felix Ruess <address@hidden> writes:
>> 
>> > Hi Matthieu,
>> >
>> > I can't reproduce the issue.
>> >
>> > Seems like your parser adds the (long) casts as that is nowhere in our 
>> > code:
>> > #define INT32_RAD_OF_DEG(_deg) (int32_t)(((int64_t)(_deg) *
>> > 14964008)/857374503)
>> >
>> > So this looks good to me as you should be able to pass up to 61637 degrees
>> > to that function...
>> > Maximum you can pass before intermediate multiplication overflows:
>> > pow(2,63) / 14964008 = 616370429423 in deg*1e7= 61637 in deg
>> >
>> > Cheers, Felix
>> >
>> > On Wed, Nov 26, 2014 at 4:53 PM, Matthieu Lemerre <address@hidden>
>> > wrote:
>> >
>> >>
>> >> Hi Felix,
>> >>
>> >> Thanks for the list of configurations. I have began the analysis of the
>> >> Quad_LisaM_2 target, and I found the following bug: in ins_int.c, the
>> >> ins_init function does:
>> >>
>> >> llh_nav0.lat = INT32_RAD_OF_DEG(NAV_LAT0);
>> >>
>> >> The macro expansion of which gives (If I configured things correctly):
>> >>
>> >> llh_nav0.lat = (int)(((long)435641194 * (long)14964008) / 
>> >> (long)857374503);
>> >>
>> >> The intermediate calculation (long) 435641194 * (long)14964008 causes an
>> >> overflow, and may not be compiled correctly.
>> >>
>> >> A work-around is to produce this code instead:
>> >>
>> >> int j = ((435641194ULL * 14964008ULL) / 857374503ULL);
>> >>
>> >> The intermediary computation fits in 64bit, and this solve the problem
>> >> here. However, I don't know a general solution to this problem if you
>> >> had a constant expression which required an intermediate computation
>> >> that does not fit in 64bit, I would be interested to know if you could
>> >> find one.
>> >>
>> >> Cheers,
>> >> Matthieu
>> >>
>> >> Felix Ruess <address@hidden> writes:
>> >>
>> >> > Hi Matthieu,
>> >> >
>> >> > If you want only two examples, I would suggest the following aircrafts
>> >> from
>> >> > the example conf:
>> >> > - rotorcraft, stm32f1: Quad_LisaM_2
>> >> > - fixedwing, lpc21: Microjet
>> >> >
>> >> > Of course these only represent a small subset of Paprazzi...
>> >> >
>> >> > Cheers, Felix
>> >> >
>> >> > On Fri, Nov 21, 2014 at 4:48 PM, Matthieu Lemerre <
>> >> address@hidden>
>> >> > wrote:
>> >> >
>> >> >>
>> >> >> Hi Michal,
>> >> >>
>> >> >> Thanks. Actually, a single-threaded mainloop is simpler to analyze, so
>> >> >> I'll stick with that for the moment.
>> >> >>
>> >> >> However, I would still be interested if you could give me the name of 2
>> >> >> configurations that are different in both dimensions {fixedwing,
>> >> >> rotorcraft} and {lpc2148,stm32}.
>> >> >>
>> >> >> Thanks,
>> >> >> Matthieu
>> >> >>
>> >> >>
>> >> >> Michal Podhradsky <address@hidden> writes:
>> >> >>
>> >> >> > Hi Matthieu,
>> >> >> >
>> >> >> > I am really glad that you are analysing Paparazzi code. There is an
>> >> >> > experimental branch based on RTOS ChibiOS, current version can be
>> >> found
>> >> >> > here: https://github.com/paparazzi/paparazzi/tree/rt_paparazzi
>> >> >> > It  contains working configuration for Rotorcraft & Lisa M/MX. There
>> >> are
>> >> >> > around 13 threads running for various subsystems, plus mutexes etc. 
>> >> >> > so
>> >> >> you
>> >> >> > might find it interesting to analyse multi-threaded version of
>> >> Paparazzi.
>> >> >> >
>> >> >> > Regards
>> >> >> > Michal
>> >> >> >
>> >> >> > On Thu, Nov 6, 2014 at 1:59 AM, Alexandre Bustico <
>> >> >> > address@hidden> wrote:
>> >> >> >
>> >> >> >> Le 06/11/2014 10:38, Matthieu Lemerre a écrit :
>> >> >> >>
>> >> >> >>> it seems that the generated source code is single-threaded, but
>> >> >> >>> are there other threads?
>> >> >> >>>
>> >> >> >>
>> >> >> >> In the master branch, there  is single-threaded mainloop, but many
>> >> >> >> callbacks are interrupt driven,
>> >> >> >> from hardware timer, and all the peripherals (i2c, spi, dma, uart,
>> >> etc
>> >> >> >> etc).
>> >> >> >>
>> >> >> >> there is also in another branch an experimental rtos (chibios)
>> >> version
>> >> >> >> which use threads.
>> >> >> >>
>> >> >> >> --
>> >> >> >> Alexandre
>> >> >> >>
>> >> >> >>
>> >> >> >>
>> >> >> >> _______________________________________________
>> >> >> >> Paparazzi-devel mailing list
>> >> >> >> address@hidden
>> >> >> >> https://lists.nongnu.org/mailman/listinfo/paparazzi-devel
>> >> >> >>
>> >> >> > _______________________________________________
>> >> >> > Paparazzi-devel mailing list
>> >> >> > address@hidden
>> >> >> > https://lists.nongnu.org/mailman/listinfo/paparazzi-devel
>> >> >>
>> >> >> _______________________________________________
>> >> >> Paparazzi-devel mailing list
>> >> >> address@hidden
>> >> >> https://lists.nongnu.org/mailman/listinfo/paparazzi-devel
>> >> >>
>> >> > _______________________________________________
>> >> > Paparazzi-devel mailing list
>> >> > address@hidden
>> >> > https://lists.nongnu.org/mailman/listinfo/paparazzi-devel
>> >>
>> 
>> _______________________________________________
>> Paparazzi-devel mailing list
>> address@hidden
>> https://lists.nongnu.org/mailman/listinfo/paparazzi-devel
>                                         
> _______________________________________________
> Paparazzi-devel mailing list
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/paparazzi-devel